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 () = the carrier of E & dom () = 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 = () . 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 ; :: 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 = () . 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 = () . 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 ; :: 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 = () . 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 ; :: 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 () holds
() . x is additive homogeneous Function of F,G
proof
let x be Point of E; :: thesis: ( x in dom () implies () . x is additive homogeneous Function of F,G )
assume x in dom () ; :: thesis: () . x is additive homogeneous Function of F,G
reconsider Lx = () . 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 ; :: 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 ; :: thesis: verum
end;
for y being Point of F st y in dom () holds
() . y is additive homogeneous Function of E,G
proof
let y be Point of F; :: thesis: ( y in dom () implies () . y is additive homogeneous Function of E,G )
assume y in dom () ; :: thesis: () . y is additive homogeneous Function of E,G
reconsider Ly = () . 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 ; :: 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 ; :: thesis: verum
end;
hence L is Bilinear by A15; :: thesis: verum