let E, F, G be RealLinearSpace; :: thesis: [: the carrier of E, the carrier of F:] --> (0. G) is Bilinear
set f = [: the carrier of E, the carrier of F:] --> (0. G);
A2: for x being Point of E holds (curry ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of F,G

proof

let x be Point of E; :: thesis: (curry ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of F,G
reconsider L = (curry ([: the carrier of E, the carrier of F:] --> (0. G))) . x as Function of F,G ;
A5: for y1, y2 being Point of F holds L . (y1 + y2) = (L . y1) + (L . y2)

proof

let y1, y2 be Point of F; :: thesis: L . (y1 + y2) = (L . y1) + (L . y2)
A11: L . (y1 + y2) = ([: the carrier of E, the carrier of F:] --> (0. G)) . (x,(y1 + y2)) by LM4
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
A12: L . y1 = ([: the carrier of E, the carrier of F:] --> (0. G)) . (x,y1) by LM4
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
L . y2 = ([: the carrier of E, the carrier of F:] --> (0. G)) . (x,y2) by LM4
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
hence L . (y1 + y2) = (L . y1) + (L . y2) by A11, A12, RLVECT_1:4; :: thesis: verum

end;

for y being Point of F
for a being Real holds L . (a * y) = a * (L . y)

proof

let y be Point of F; :: thesis: for a being Real holds L . (a * y) = a * (L . y)
let a be Real; :: thesis: L . (a * y) = a * (L . y)
A18: L . (a * y) = ([: the carrier of E, the carrier of F:] --> (0. G)) . (x,(a * y)) by LM4
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
L . y = ([: the carrier of E, the carrier of F:] --> (0. G)) . (x,y) by LM4
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
hence L . (a * y) = a * (L . y) by A18, RLVECT_1:10; :: thesis: verum

end;

hence (curry ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of F,G by A5, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

for x being Point of F st x in dom (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) holds
(curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G

proof

let x be Point of F; :: thesis: ( x in dom (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) implies (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G )
assume x in dom (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) ; :: thesis: (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G
reconsider L = (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x as Function of E,G ;
A22: for y1, y2 being Point of E holds L . (y1 + y2) = (L . y1) + (L . y2)

proof

let y1, y2 be Point of E; :: thesis: L . (y1 + y2) = (L . y1) + (L . y2)
A28: L . (y1 + y2) = ([: the carrier of E, the carrier of F:] --> (0. G)) . ((y1 + y2),x) by LM5
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
A29: L . y1 = ([: the carrier of E, the carrier of F:] --> (0. G)) . (y1,x) by LM5
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
L . y2 = ([: the carrier of E, the carrier of F:] --> (0. G)) . (y2,x) by LM5
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
hence L . (y1 + y2) = (L . y1) + (L . y2) by A28, A29, RLVECT_1:4; :: thesis: verum

end;

for y being Point of E
for a being Real holds L . (a * y) = a * (L . y)

proof

let y be Point of E; :: thesis: for a being Real holds L . (a * y) = a * (L . y)
let a be Real; :: thesis: L . (a * y) = a * (L . y)
A35: L . (a * y) = ([: the carrier of E, the carrier of F:] --> (0. G)) . ((a * y),x) by LM5
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
L . y = ([: the carrier of E, the carrier of F:] --> (0. G)) . (y,x) by LM5
.= 0. G by ZFMISC_1:87, FUNCOP_1:7 ;
hence L . (a * y) = a * (L . y) by A35, RLVECT_1:10; :: thesis: verum

end;

hence (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G by A22, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

hence [: the carrier of E, the carrier of F:] --> (0. G) is Bilinear by A2; :: thesis: verum