:: BILINEAR semantic presentation

definition
let c1 be 1-sorted ;
let c2, c3 be VectSpStr of c1;
mode Form is Function of [:the carrier of a2,the carrier of a3:],the carrier of a1;
end;

definition
let c1 be non empty ZeroStr ;
let c2, c3 be VectSpStr of c1;
canceled;
func NulForm a2,a3 -> Form of a2,a3 equals :: BILINEAR:def 2
[:the carrier of a2,the carrier of a3:] --> (0. a1);
coherence
[:the carrier of c2,the carrier of c3:] --> (0. c1) is Form of c2,c3 ;
end;

:: deftheorem BILINEAR:def 1 :
canceled;

:: deftheorem defines NulForm BILINEAR:def 2 :
for b1 being non empty ZeroStr
for b2, b3 being VectSpStr of b1 holds NulForm b2,b3 = [:the carrier of b2,the carrier of b3:] --> (0. b1);

definition
let c1 be non empty LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Form of c2,c3;
func a4 + a5 -> Form of a2,a3 means :E1: :: BILINEAR:def 3
for b1 being Vector of a2
for b2 being Vector of a3 holds a6 . [b1,b2] = (a4 . [b1,b2]) + (a5 . [b1,b2]);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . [b2,b3] = (c4 . [b2,b3]) + (c5 . [b2,b3])
proof
set c6 = the carrier of c2;
set c7 = the carrier of c3;
set c8 = the carrier of c1;
deffunc H1( Element of the carrier of c2, Element of the carrier of c3) -> Element of the carrier of c1 = (c4 . [a1,a2]) + (c5 . [a1,a2]);
consider c9 being Function of [:the carrier of c2,the carrier of c3:],the carrier of c1 such that
E1: for b1 being Element of the carrier of c2
for b2 being Element of the carrier of c3 holds c9 . [b1,b2] = H1(b1,b2) from FUNCT_2:sch 8();
 reconsider c10 = c9 as Form of c2,c3 ;
take c10 ;
thus for b1 being Vector of c2
for b2 being Vector of c3 holds c10 . [b1,b2] = (c4 . [b1,b2]) + (c5 . [b1,b2]) by E1;
end;
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . [b3,b4] = (c4 . [b3,b4]) + (c5 . [b3,b4]) & for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . [b3,b4] = (c4 . [b3,b4]) + (c5 . [b3,b4]) ) implies ( b1 = b2 ) )
proof
let c6, c7 be Form of c2,c3;
assume that E1: for b1 being Vector of c2
for b2 being Vector of c3 holds c6 . [b1,b2] = (c4 . [b1,b2]) + (c5 . [b1,b2])
and E2: for b1 being Vector of c2
for b2 being Vector of c3 holds c7 . [b1,b2] = (c4 . [b1,b2]) + (c5 . [b1,b2]) ;
now
let c8 be Vector of c2;
let c9 be Vector of c3;
thus c6 . [c8,c9] = (c4 . [c8,c9]) + (c5 . [c8,c9]) by E1
.= c7 . [c8,c9] by E2 ;
end;
hence c6 = c7 by FUNCT_2:120;
end;
end;

:: deftheorem E1 defines + BILINEAR:def 3 :
for b1 being non empty LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5, b6 being Form of b2,b3 holds
( b6 = b4 + b5 iff for b7 being Vector of b2
for b8 being Vector of b3 holds b6 . [b7,b8] = (b4 . [b7,b8]) + (b5 . [b7,b8]) );

definition
let c1 be non empty HGrStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Element of c1;
func a5 * a4 -> Form of a2,a3 means :E2: :: BILINEAR:def 4
for b1 being Vector of a2
for b2 being Vector of a3 holds a6 . [b1,b2] = a5 * (a4 . [b1,b2]);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . [b2,b3] = c5 * (c4 . [b2,b3])
proof
set c6 = the carrier of c2;
set c7 = the carrier of c3;
set c8 = the carrier of c1;
deffunc H1( Element of the carrier of c2, Element of the carrier of c3) -> Element of the carrier of c1 = c5 * (c4 . [a1,a2]);
consider c9 being Function of [:the carrier of c2,the carrier of c3:],the carrier of c1 such that
E2: for b1 being Element of the carrier of c2
for b2 being Element of the carrier of c3 holds c9 . [b1,b2] = H1(b1,b2) from FUNCT_2:sch 8();
 reconsider c10 = c9 as Form of c2,c3 ;
take c10 ;
thus for b1 being Vector of c2
for b2 being Vector of c3 holds c10 . [b1,b2] = c5 * (c4 . [b1,b2]) by E2;
end;
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . [b3,b4] = c5 * (c4 . [b3,b4]) & for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . [b3,b4] = c5 * (c4 . [b3,b4]) ) implies ( b1 = b2 ) )
proof
let c6, c7 be Form of c2,c3;
assume that E2: for b1 being Vector of c2
for b2 being Vector of c3 holds c6 . [b1,b2] = c5 * (c4 . [b1,b2])
and E3: for b1 being Vector of c2
for b2 being Vector of c3 holds c7 . [b1,b2] = c5 * (c4 . [b1,b2]) ;
now
let c8 be Vector of c2;
let c9 be Vector of c3;
thus c6 . [c8,c9] = c5 * (c4 . [c8,c9]) by E2
.= c7 . [c8,c9] by E3 ;
end;
hence c6 = c7 by FUNCT_2:120;
end;
end;

:: deftheorem E2 defines * BILINEAR:def 4 :
for b1 being non empty HGrStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3
for b5 being Element of b1
for b6 being Form of b2,b3 holds
( b6 = b5 * b4 iff for b7 being Vector of b2
for b8 being Vector of b3 holds b6 . [b7,b8] = b5 * (b4 . [b7,b8]) );

definition
let c1 be non empty LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
func - a4 -> Form of a2,a3 means :E3: :: BILINEAR:def 5
for b1 being Vector of a2
for b2 being Vector of a3 holds a5 . [b1,b2] = - (a4 . [b1,b2]);
existence
ex b1 being Form of c2,c3 st
for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . [b2,b3] = - (c4 . [b2,b3])
proof
set c5 = the carrier of c2;
set c6 = the carrier of c3;
set c7 = the carrier of c1;
deffunc H1( Element of the carrier of c2, Element of the carrier of c3) -> Element of the carrier of c1 = - (c4 . [a1,a2]);
consider c8 being Function of [:the carrier of c2,the carrier of c3:],the carrier of c1 such that
E3: for b1 being Element of the carrier of c2
for b2 being Element of the carrier of c3 holds c8 . [b1,b2] = H1(b1,b2) from FUNCT_2:sch 8();
 reconsider c9 = c8 as Form of c2,c3 ;
take c9 ;
thus for b1 being Vector of c2
for b2 being Vector of c3 holds c9 . [b1,b2] = - (c4 . [b1,b2]) by E3;
end;
uniqueness
for b1, b2 being Form of c2,c3 holds
( ( for b3 being Vector of c2
for b4 being Vector of c3 holds b1 . [b3,b4] = - (c4 . [b3,b4]) & for b3 being Vector of c2
for b4 being Vector of c3 holds b2 . [b3,b4] = - (c4 . [b3,b4]) ) implies ( b1 = b2 ) )
proof
let c5, c6 be Form of c2,c3;
assume that E3: for b1 being Vector of c2
for b2 being Vector of c3 holds c5 . [b1,b2] = - (c4 . [b1,b2])
and E4: for b1 being Vector of c2
for b2 being Vector of c3 holds c6 . [b1,b2] = - (c4 . [b1,b2]) ;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus c5 . [c7,c8] = - (c4 . [c7,c8]) by E3
.= c6 . [c7,c8] by E4 ;
end;
hence c5 = c6 by FUNCT_2:120;
end;
end;

:: deftheorem E3 defines - BILINEAR:def 5 :
for b1 being non empty LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5 being Form of b2,b3 holds
( b5 = - b4 iff for b6 being Vector of b2
for b7 being Vector of b3 holds b5 . [b6,b7] = - (b4 . [b6,b7]) );

definition
let c1 be non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
redefine func - as - a4 -> Form of a2,a3 equals :: BILINEAR:def 6
(- (1. a1)) * a4;
coherence
- c4 is Form of c2,c3 ;
compatibility
for b1 being Form of c2,c3 holds
( b1 = - c4 iff b1 = (- (1. c1)) * c4 )
proof
let c5 be Form of c2,c3;
thus ( c5 = - c4 implies c5 = (- (1. c1)) * c4 )
proof
assume E4: c5 = - c4 ;
now
let c6 be Vector of c2;
let c7 be Vector of c3;
thus c5 . [c6,c7] = - (c4 . [c6,c7]) by E4, E3
.= (- (1. c1)) * (c4 . [c6,c7]) by MOD_1:14
.= ((- (1. c1)) * c4) . [c6,c7] by E2 ;
end;
hence c5 = (- (1. c1)) * c4 by FUNCT_2:120;
end;
assume E4: c5 = (- (1. c1)) * c4 ;
now
let c6 be Vector of c2;
let c7 be Vector of c3;
thus c5 . [c6,c7] = (- (1. c1)) * (c4 . [c6,c7]) by E4, E2
.= - (c4 . [c6,c7]) by MOD_1:14
.= (- c4) . [c6,c7] by E3 ;
end;
hence c5 = - c4 by FUNCT_2:120;
end;
end;

:: deftheorem defines - BILINEAR:def 6 :
for b1 being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3 holds - b4 = (- (1. b1)) * b4;

definition
let c1 be non empty LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Form of c2,c3;
func a4 - a5 -> Form of a2,a3 equals :: BILINEAR:def 7
a4 + (- a5);
correctness
coherence
c4 + (- c5) is Form of c2,c3;
;
end;

:: deftheorem defines - BILINEAR:def 7 :
for b1 being non empty LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5 being Form of b2,b3 holds b4 - b5 = b4 + (- b5);

definition
let c1 be non empty LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Form of c2,c3;
redefine func - as a4 - a5 -> Form of a2,a3 means :E4: :: BILINEAR:def 8
for b1 being Vector of a2
for b2 being Vector of a3 holds a6 . [b1,b2] = (a4 . [b1,b2]) - (a5 . [b1,b2]);
coherence
c4 - c5 is Form of c2,c3 ;
compatibility
for b1 being Form of c2,c3 holds
( b1 = c4 - c5 iff for b2 being Vector of c2
for b3 being Vector of c3 holds b1 . [b2,b3] = (c4 . [b2,b3]) - (c5 . [b2,b3]) )
proof
let c6 be Form of c2,c3;
thus ( c6 = c4 - c5 implies for b1 being Vector of c2
for b2 being Vector of c3 holds c6 . [b1,b2] = (c4 . [b1,b2]) - (c5 . [b1,b2]) )
proof
assume E4: c6 = c4 - c5 ;
let c7 be Vector of c2;
let c8 be Vector of c3;
thus c6 . [c7,c8] = (c4 + (- c5)) . [c7,c8] by E4
.= (c4 . [c7,c8]) + ((- c5) . [c7,c8]) by E1
.= (c4 . [c7,c8]) + (- (c5 . [c7,c8])) by E3
.= (c4 . [c7,c8]) - (c5 . [c7,c8]) by RLVECT_1:def 11 ;
end;
assume E4: for b1 being Vector of c2
for b2 being Vector of c3 holds c6 . [b1,b2] = (c4 . [b1,b2]) - (c5 . [b1,b2]) ;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus c6 . [c7,c8] = (c4 . [c7,c8]) - (c5 . [c7,c8]) by E4
.= (c4 . [c7,c8]) + (- (c5 . [c7,c8])) by RLVECT_1:def 11
.= (c4 . [c7,c8]) + ((- c5) . [c7,c8]) by E3
.= (c4 + (- c5)) . [c7,c8] by E1
.= (c4 - c5) . [c7,c8] ;
end;
hence c6 = c4 - c5 by FUNCT_2:120;
end;
end;

:: deftheorem E4 defines - BILINEAR:def 8 :
for b1 being non empty LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5, b6 being Form of b2,b3 holds
( b6 = b4 - b5 iff for b7 being Vector of b2
for b8 being Vector of b3 holds b6 . [b7,b8] = (b4 . [b7,b8]) - (b5 . [b7,b8]) );

E5: now
let c1 be non empty Abelian LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Form of c2,c3;
now
let c6 be Vector of c2;
let c7 be Vector of c3;
thus (c4 + c5) . [c6,c7] = (c4 . [c6,c7]) + (c5 . [c6,c7]) by E1
.= (c5 + c4) . [c6,c7] by E1 ;
end;
hence c4 + c5 = c5 + c4 by FUNCT_2:120;
end;

definition
let c1 be non empty Abelian LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Form of c2,c3;
redefine func + as a4 + a5 -> Form of a2,a3;
commutativity
for b1, b2 being Form of c2,c3 holds b1 + b2 = b2 + b1 by E5;
end;

theorem E6: :: BILINEAR:1
for b1 being non empty ZeroStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Vector of b2
for b5 being Vector of b3 holds (NulForm b2,b3) . [b4,b5] = 0. b1
proof
let c1 be non empty ZeroStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Vector of c2;
let c5 be Vector of c3;
set c6 = NulForm c2,c3;
thus (NulForm c2,c3) . [c4,c5] = ([:the carrier of c2,the carrier of c3:] --> (0. c1)) . [c4,c5]
.= 0. c1 by FUNCOP_1:13 ;
end;

theorem :: BILINEAR:2
for b1 being non empty right_zeroed LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3 holds b4 + (NulForm b2,b3) = b4
proof
let c1 be non empty right_zeroed LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
set c5 = NulForm c2,c3;
now
let c6 be Vector of c2;
let c7 be Vector of c3;
thus (c4 + (NulForm c2,c3)) . [c6,c7] = (c4 . [c6,c7]) + ((NulForm c2,c3) . [c6,c7]) by E1
.= (c4 . [c6,c7]) + (0. c1) by E6
.= c4 . [c6,c7] by RLVECT_1:def 7 ;
end;
hence c4 + (NulForm c2,c3) = c4 by FUNCT_2:120;
end;

theorem :: BILINEAR:3
for b1 being non empty add-associative LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5, b6 being Form of b2,b3 holds (b4 + b5) + b6 = b4 + (b5 + b6)
proof
let c1 be non empty add-associative LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5, c6 be Form of c2,c3;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus ((c4 + c5) + c6) . [c7,c8] = ((c4 + c5) . [c7,c8]) + (c6 . [c7,c8]) by E1
.= ((c4 . [c7,c8]) + (c5 . [c7,c8])) + (c6 . [c7,c8]) by E1
.= (c4 . [c7,c8]) + ((c5 . [c7,c8]) + (c6 . [c7,c8])) by RLVECT_1:def 6
.= (c4 . [c7,c8]) + ((c5 + c6) . [c7,c8]) by E1
.= (c4 + (c5 + c6)) . [c7,c8] by E1 ;
end;
hence (c4 + c5) + c6 = c4 + (c5 + c6) by FUNCT_2:120;
end;

theorem :: BILINEAR:4
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3 holds b4 - b4 = NulForm b2,b3
proof
let c1 be non empty add-associative right_zeroed right_complementable LoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
now
let c5 be Vector of c2;
let c6 be Vector of c3;
thus (c4 - c4) . [c5,c6] = (c4 . [c5,c6]) - (c4 . [c5,c6]) by E4
.= 0. c1 by RLVECT_1:28
.= (NulForm c2,c3) . [c5,c6] by E6 ;
end;
hence c4 - c4 = NulForm c2,c3 by FUNCT_2:120;
end;

theorem :: BILINEAR:5
for b1 being non empty right-distributive doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Element of b1
for b5, b6 being Form of b2,b3 holds b4 * (b5 + b6) = (b4 * b5) + (b4 * b6)
proof
let c1 be non empty right-distributive doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Element of c1;
let c5, c6 be Form of c2,c3;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus (c4 * (c5 + c6)) . [c7,c8] = c4 * ((c5 + c6) . [c7,c8]) by E2
.= c4 * ((c5 . [c7,c8]) + (c6 . [c7,c8])) by E1
.= (c4 * (c5 . [c7,c8])) + (c4 * (c6 . [c7,c8])) by VECTSP_1:def 11
.= ((c4 * c5) . [c7,c8]) + (c4 * (c6 . [c7,c8])) by E2
.= ((c4 * c5) . [c7,c8]) + ((c4 * c6) . [c7,c8]) by E2
.= ((c4 * c5) + (c4 * c6)) . [c7,c8] by E1 ;
end;
hence c4 * (c5 + c6) = (c4 * c5) + (c4 * c6) by FUNCT_2:120;
end;

theorem :: BILINEAR:6
for b1 being non empty left-distributive doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5 being Element of b1
for b6 being Form of b2,b3 holds (b4 + b5) * b6 = (b4 * b6) + (b5 * b6)
proof
let c1 be non empty left-distributive doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Element of c1;
let c6 be Form of c2,c3;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus ((c4 + c5) * c6) . [c7,c8] = (c4 + c5) * (c6 . [c7,c8]) by E2
.= (c4 * (c6 . [c7,c8])) + (c5 * (c6 . [c7,c8])) by VECTSP_1:def 12
.= ((c4 * c6) . [c7,c8]) + (c5 * (c6 . [c7,c8])) by E2
.= ((c4 * c6) . [c7,c8]) + ((c5 * c6) . [c7,c8]) by E2
.= ((c4 * c6) + (c5 * c6)) . [c7,c8] by E1 ;
end;
hence (c4 + c5) * c6 = (c4 * c6) + (c5 * c6) by FUNCT_2:120;
end;

theorem :: BILINEAR:7
for b1 being non empty associative doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4, b5 being Element of b1
for b6 being Form of b2,b3 holds (b4 * b5) * b6 = b4 * (b5 * b6)
proof
let c1 be non empty associative doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4, c5 be Element of c1;
let c6 be Form of c2,c3;
now
let c7 be Vector of c2;
let c8 be Vector of c3;
thus ((c4 * c5) * c6) . [c7,c8] = (c4 * c5) * (c6 . [c7,c8]) by E2
.= c4 * (c5 * (c6 . [c7,c8])) by GROUP_1:def 4
.= c4 * ((c5 * c6) . [c7,c8]) by E2
.= (c4 * (c5 * c6)) . [c7,c8] by E2 ;
end;
hence (c4 * c5) * c6 = c4 * (c5 * c6) by FUNCT_2:120;
end;

theorem :: BILINEAR:8
for b1 being non empty left_unital doubleLoopStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3 holds (1. b1) * b4 = b4
proof
let c1 be non empty left_unital doubleLoopStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
now
let c5 be Vector of c2;
let c6 be Vector of c3;
thus ((1. c1) * c4) . [c5,c6] = (1. c1) * (c4 . [c5,c6]) by E2
.= c4 . [c5,c6] by VECTSP_1:def 19 ;
end;
hence (1. c1) * c4 = c4 by FUNCT_2:120;
end;

E7: now
let c1 be non empty 1-sorted ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Element of the carrier of c2;
let c6 be Element of c3;
E8: dom c4 = [:the carrier of c2,the carrier of c3:] by FUNCT_2:def 1;
then consider c7 being Function such that
E9: ( (curry c4) . c5 = c7 & dom c7 = the carrier of c3 & rng c7 c= rng c4 )
and for b1 being set holds
( b1 in the carrier of c3 implies c7 . b1 = c4 . [c5,b1] ) by FUNCT_5:36;
rng c7 c= the carrier of c1 by E9, XBOOLE_1:1;
then reconsider c8 = c7 as Function of the carrier of c3,the carrier of c1 by E9, FUNCT_2:4;
c8 = (curry c4) . c5 by E9;
hence (curry c4) . c5 is Functional of c3 ;
consider c9 being Function such that
E10: ( (curry' c4) . c6 = c9 & dom c9 = the carrier of c2 & rng c9 c= rng c4 )
and for b1 being set holds
( b1 in the carrier of c2 implies c9 . b1 = c4 . [b1,c6] ) by E8, FUNCT_5:39;
rng c9 c= the carrier of c1 by E10, XBOOLE_1:1;
then reconsider c10 = c9 as Function of the carrier of c2,the carrier of c1 by E10, FUNCT_2:4;
c10 = (curry' c4) . c6 by E10;
hence (curry' c4) . c6 is Functional of c2 ;
end;

definition
let c1 be non empty 1-sorted ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Vector of c2;
func FunctionalFAF a4,a5 -> Functional of a3 equals :: BILINEAR:def 9
(curry a4) . a5;
correctness
coherence
(curry c4) . c5 is Functional of c3;
by E7;
end;

:: deftheorem defines FunctionalFAF BILINEAR:def 9 :
for b1 being non empty 1-sorted
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3
for b5 being Vector of b2 holds FunctionalFAF b4,b5 = (curry b4) . b5;

definition
let c1 be non empty 1-sorted ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Vector of c3;
func FunctionalSAF a4,a5 -> Functional of a2 equals :: BILINEAR:def 10
(curry' a4) . a5;
correctness
coherence
(curry' c4) . c5 is Functional of c2;
by E7;
end;

:: deftheorem defines FunctionalSAF BILINEAR:def 10 :
for b1 being non empty 1-sorted
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3
for b5 being Vector of b3 holds FunctionalSAF b4,b5 = (curry' b4) . b5;

theorem E8: :: BILINEAR:9
for b1 being non empty 1-sorted
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3
for b5 being Vector of b2 holds
( dom (FunctionalFAF b4,b5) = the carrier of b3 & rng (FunctionalFAF b4,b5) c= the carrier of b1 & for b6 being Vector of b3 holds (FunctionalFAF b4,b5) . b6 = b4 . [b5,b6] )
proof
let c1 be non empty 1-sorted ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Vector of c2;
set c6 = FunctionalFAF c4,c5;
E9: ( dom c4 = [:the carrier of c2,the carrier of c3:] & rng c4 c= the carrier of c1 ) by FUNCT_2:def 1;
consider c7 being Function such that
E10: ( (curry c4) . c5 = c7 & dom c7 = the carrier of c3 & rng c7 c= rng c4 )
and E11: for b1 being set holds
( b1 in the carrier of c3 implies c7 . b1 = c4 . [c5,b1] ) by E9, FUNCT_5:36;
thus ( dom (FunctionalFAF c4,c5) = the carrier of c3 & rng (FunctionalFAF c4,c5) c= the carrier of c1 ) by E10;
let c8 be Vector of c3;
thus (FunctionalFAF c4,c5) . c8 = c4 . [c5,c8] by E10, E11;
end;

theorem E9: :: BILINEAR:10
for b1 being non empty 1-sorted
for b2, b3 being non empty VectSpStr of b1
for b4 being Form of b2,b3
for b5 being Vector of b3 holds
( dom (FunctionalSAF b4,b5) = the carrier of b2 & rng (FunctionalSAF b4,b5) c= the carrier of b1 & for b6 being Vector of b2 holds (FunctionalSAF b4,b5) . b6 = b4 . [b6,b5] )
proof
let c1 be non empty 1-sorted ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Form of c2,c3;
let c5 be Vector of c3;
set c6 = FunctionalSAF c4,c5;
E10: ( dom c4 = [:the carrier of c2,the carrier of c3:] & rng c4 c= the carrier of c1 ) by FUNCT_2:def 1;
consider c7 being Function such that
E11: ( (curry' c4) . c5 = c7 & dom c7 = the carrier of c2 & rng c7 c= rng c4 )
and E12: for b1 being set holds
( b1 in the carrier of c2 implies c7 . b1 = c4 . [b1,c5] ) by E10, FUNCT_5:39;
thus ( dom (FunctionalSAF c4,c5) = the carrier of c2 & rng (FunctionalSAF c4,c5) c= the carrier of c1 ) by E11;
let c8 be Vector of c2;
thus (FunctionalSAF c4,c5) . c8 = c4 . [c8,c5] by E11, E12;
end;

theorem E10: :: BILINEAR:11
for b1 being non empty ZeroStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Vector of b2 holds FunctionalFAF (NulForm b2,b3),b4 = 0Functional b3
proof
let c1 be non empty ZeroStr ;
let c2, c3 be non empty VectSpStr of c1;
let c4 be Vector of c2;
set c5 = NulForm c2,c3;
now
let c6 be Vector of c3;
thus (FunctionalFAF (NulForm c2,c3),c4) . c6 = (NulForm c2,c3) . [c4,c6] by E8
.= 0. c1 by E6
.= (0Functional c3) . c6 by HAHNBAN1:22 ;
end;
hence FunctionalFAF (NulForm c2,c3),c4 = 0Functional c3 by FUNCT_2:113;
end;

theorem E11: :: BILINEAR:12
for b1 being non empty ZeroStr
for b2, b3 being non empty VectSpStr of b1
for b4 being Vector of b3 holds FunctionalSAF (NulForm b2,b3),b4