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;

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

(curry' L) . y is additive homogeneous Function of E,G

( 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 that 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)) ) )

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

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

for y being Point of F

for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) :: thesis: verum

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

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

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

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

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

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

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

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

for y being Point of F st y in dom (curry' L) holds
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)

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

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

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

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

proof

hence
(curry L) . x is additive homogeneous Function of F,G
by A16, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum
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;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

(curry' L) . y is additive homogeneous Function of E,G

proof

hence
L is Bilinear
by A15; :: thesis: verum
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)

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

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

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

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

proof

hence
(curry' L) . y is additive homogeneous Function of E,G
by A22, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum
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;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