let E, F, G be RealNormSpace; :: thesis: for f being BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G )
let f be BilinearOperator of E,F,G; :: thesis: for z being Point of [:E,F:] holds
( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G )
let z be Point of [:E,F:]; :: thesis: ( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G )
reconsider L1 = f * (reproj1 z) as Function of E,G ;
for x, y being Element of E holds L1 . (x + y) = (L1 . x) + (L1 . y)

proof

let x, y be Element of E; :: thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
A1: L1 . (x + y) = f . ((reproj1 z) . (x + y)) by FUNCT_2:15
.= f . ((x + y),(z `2)) by NDIFF_7:def 1
.= (f . (x,(z `2))) + (f . (y,(z `2))) by LOPBAN_8:12 ;
A2: f . (x,(z `2)) = f . ((reproj1 z) . x) by NDIFF_7:def 1
.= L1 . x by FUNCT_2:15 ;
f . (y,(z `2)) = f . ((reproj1 z) . y) by NDIFF_7:def 1
.= L1 . y by FUNCT_2:15 ;
hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A2; :: thesis: verum

end;

then A3: L1 is additive ;
A4: for x being VECTOR of E
for a being Real holds L1 . (a * x) = a * (L1 . x)

proof

let x be VECTOR of E; :: thesis: for a being Real holds L1 . (a * x) = a * (L1 . x)
let a be Real; :: thesis: L1 . (a * x) = a * (L1 . x)
A5: L1 . (a * x) = f . ((reproj1 z) . (a * x)) by FUNCT_2:15
.= f . ((a * x),(z `2)) by NDIFF_7:def 1
.= a * (f . (x,(z `2))) by LOPBAN_8:12 ;
f . (x,(z `2)) = f . ((reproj1 z) . x) by NDIFF_7:def 1
.= L1 . x by FUNCT_2:15 ;
hence L1 . (a * x) = a * (L1 . x) by A5; :: thesis: verum

end;

reconsider L2 = f * (reproj2 z) as Function of F,G ;
for x, y being Element of F holds L2 . (x + y) = (L2 . x) + (L2 . y)

proof

let x, y be Element of F; :: thesis: L2 . (x + y) = (L2 . x) + (L2 . y)
A6: L2 . (x + y) = f . ((reproj2 z) . (x + y)) by FUNCT_2:15
.= f . ((z `1),(x + y)) by NDIFF_7:def 2
.= (f . ((z `1),x)) + (f . ((z `1),y)) by LOPBAN_8:12 ;
A7: f . ((z `1),x) = f . ((reproj2 z) . x) by NDIFF_7:def 2
.= L2 . x by FUNCT_2:15 ;
f . ((z `1),y) = f . ((reproj2 z) . y) by NDIFF_7:def 2
.= L2 . y by FUNCT_2:15 ;
hence L2 . (x + y) = (L2 . x) + (L2 . y) by A6, A7; :: thesis: verum

end;

then A8: L2 is additive ;
for x being VECTOR of F
for a being Real holds L2 . (a * x) = a * (L2 . x)

proof

let x be VECTOR of F; :: thesis: for a being Real holds L2 . (a * x) = a * (L2 . x)
let a be Real; :: thesis: L2 . (a * x) = a * (L2 . x)
A9: L2 . (a * x) = f . ((reproj2 z) . (a * x)) by FUNCT_2:15
.= f . ((z `1),(a * x)) by NDIFF_7:def 2
.= a * (f . ((z `1),x)) by LOPBAN_8:12 ;
f . ((z `1),x) = f . ((reproj2 z) . x) by NDIFF_7:def 2
.= L2 . x by FUNCT_2:15 ;
hence L2 . (a * x) = a * (L2 . x) by A9; :: thesis: verum

end;

hence ( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G ) by A3, A4, LOPBAN_1:def 5, A8; :: thesis: verum