let E, F, G be RealLinearSpace; :: thesis: for L being Function of [: the carrier of E, the carrier of F:], the carrier of G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) )
let L be Function of [: the carrier of E, the carrier of F:], the carrier of G; :: thesis: ( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) )
A1: ( dom (curry L) = the carrier of E & dom (curry' L) = the carrier of F ) by FUNCT_2:def 1;

hereby :: thesis: ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) implies L is Bilinear )

assume A2: L is Bilinear ; :: thesis: ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) )
thus for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) :: thesis: ( ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) )

proof

let x1, x2 be Point of E; :: thesis: for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
let y be Point of F; :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
reconsider Ly = (curry' L) . y as additive homogeneous Function of E,G by A1, A2;
A5: Ly . x1 = L . (x1,y) by LM5;
A6: Ly . x2 = L . (x2,y) by LM5;
thus L . ((x1 + x2),y) = Ly . (x1 + x2) by LM5
.= (L . (x1,y)) + (L . (x2,y)) by A5, A6, VECTSP_1:def 20 ; :: thesis: verum

end;

thus for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) :: thesis: ( ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) )

proof

let x be Point of E; :: thesis: for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let y be Point of F; :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))
reconsider Ly = (curry' L) . y as additive homogeneous Function of E,G by A1, A2;
thus L . ((a * x),y) = Ly . (a * x) by LM5
.= a * (Ly . x) by LOPBAN_1:def 5
.= a * (L . (x,y)) by LM5 ; :: thesis: verum

end;

thus for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) :: thesis: for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

let x be Point of E; :: thesis: for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
let y1, y2 be Point of F; :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
reconsider Lx = (curry L) . x as additive homogeneous Function of F,G by A1, A2;
A8: Lx . y1 = L . (x,y1) by LM4;
A9: Lx . y2 = L . (x,y2) by LM4;
thus L . (x,(y1 + y2)) = Lx . (y1 + y2) by LM4
.= (L . (x,y1)) + (L . (x,y2)) by A8, A9, VECTSP_1:def 20 ; :: thesis: verum

end;

thus for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) :: thesis: verum

proof

let x be Point of E; :: thesis: for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let y be Point of F; :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))
reconsider Lx = (curry L) . x as additive homogeneous Function of F,G by A1, A2;
A10: Lx . y = L . (x,y) by LM4;
thus L . (x,(a * y)) = Lx . (a * y) by LM4
.= a * (L . (x,y)) by A10, LOPBAN_1:def 5 ; :: thesis: verum

end;

end;

assume that
A11: for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) and
A12: for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) and
A13: for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) and
A14: for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ; :: thesis: L is Bilinear
A15: for x being Point of E st x in dom (curry L) holds
(curry L) . x is additive homogeneous Function of F,G

proof

let x be Point of E; :: thesis: ( x in dom (curry L) implies (curry L) . x is additive homogeneous Function of F,G )
assume x in dom (curry L) ; :: thesis: (curry L) . x is additive homogeneous Function of F,G
reconsider Lx = (curry L) . x as Function of F,G ;
A16: for y1, y2 being Point of F holds Lx . (y1 + y2) = (Lx . y1) + (Lx . y2)

proof

let y1, y2 be Point of F; :: thesis: Lx . (y1 + y2) = (Lx . y1) + (Lx . y2)
A17: L . (x,y1) = Lx . y1 by LM4;
thus Lx . (y1 + y2) = L . (x,(y1 + y2)) by LM4
.= (L . (x,y1)) + (L . (x,y2)) by A13
.= (Lx . y1) + (Lx . y2) by A17, LM4 ; :: thesis: verum

end;

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

proof

let y be Point of F; :: thesis: for a being Real holds Lx . (a * y) = a * (Lx . y)
let a be Real; :: thesis: Lx . (a * y) = a * (Lx . y)
thus Lx . (a * y) = L . (x,(a * y)) by LM4
.= a * (L . (x,y)) by A14
.= a * (Lx . y) by LM4 ; :: thesis: verum

end;

hence (curry L) . x is additive homogeneous Function of F,G by A16, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

for y being Point of F st y in dom (curry' L) holds
(curry' L) . y is additive homogeneous Function of E,G

proof

let y be Point of F; :: thesis: ( y in dom (curry' L) implies (curry' L) . y is additive homogeneous Function of E,G )
assume y in dom (curry' L) ; :: thesis: (curry' L) . y is additive homogeneous Function of E,G
reconsider Ly = (curry' L) . y as Function of E,G ;
A22: for x1, x2 being Point of E holds Ly . (x1 + x2) = (Ly . x1) + (Ly . x2)

proof

let x1, x2 be Point of E; :: thesis: Ly . (x1 + x2) = (Ly . x1) + (Ly . x2)
A23: L . (x1,y) = Ly . x1 by LM5;
thus Ly . (x1 + x2) = L . ((x1 + x2),y) by LM5
.= (L . (x1,y)) + (L . (x2,y)) by A11
.= (Ly . x1) + (Ly . x2) by A23, LM5 ; :: thesis: verum

end;

for x being Point of E
for a being Real holds Ly . (a * x) = a * (Ly . x)

proof

let x be Point of E; :: thesis: for a being Real holds Ly . (a * x) = a * (Ly . x)
let a be Real; :: thesis: Ly . (a * x) = a * (Ly . x)
thus Ly . (a * x) = L . ((a * x),y) by LM5
.= a * (L . (x,y)) by A12
.= a * (Ly . x) by LM5 ; :: thesis: verum

end;

hence (curry' L) . y is additive homogeneous Function of E,G by A22, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

hence L is Bilinear by A15; :: thesis: verum