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

(curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G

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

for x being Point of F st x in dom (curry' ([: the carrier of E, the carrier of F:] --> (0. G))) holds
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)

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

end;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

for y being Point of F
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;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

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

proof

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
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;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

(curry' ([: the carrier of E, the carrier of F:] --> (0. G))) . x is additive homogeneous Function of E,G

proof

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

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

end;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

for y being Point of E
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;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

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

proof

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
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;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