let E, F, G be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of E,F,G holds
( ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`1 (f,(a * z)) = a * (partdiff`1 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) ) )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: ( ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`1 (f,(a * z)) = a * (partdiff`1 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) ) )

A1: now :: thesis: for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2))

let z1, z2 be Point of [:E,F:]; :: thesis: partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2))
for x being VECTOR of E holds (partdiff`1 (f,(z1 + z2))) . x = ((partdiff`1 (f,z1)) . x) + ((partdiff`1 (f,z2)) . x)

proof

let x be VECTOR of E; :: thesis: (partdiff`1 (f,(z1 + z2))) . x = ((partdiff`1 (f,z1)) . x) + ((partdiff`1 (f,z2)) . x)
A2: (partdiff`1 (f,z1)) . x = (f * (reproj1 z1)) . x by Th4
.= f . ((reproj1 z1) . x) by FUNCT_2:15
.= f . (x,(z1 `2)) by NDIFF_7:def 1 ;
A3: (partdiff`1 (f,z2)) . x = (f * (reproj1 z2)) . x by Th4
.= f . ((reproj1 z2) . x) by FUNCT_2:15
.= f . (x,(z2 `2)) by NDIFF_7:def 1 ;
thus (partdiff`1 (f,(z1 + z2))) . x = (f * (reproj1 (z1 + z2))) . x by Th4
.= f . ((reproj1 (z1 + z2)) . x) by FUNCT_2:15
.= f . [x,((z1 + z2) `2)] by NDIFF_7:def 1
.= f . (x,((z1 `2) + (z2 `2))) by Th5
.= ((partdiff`1 (f,z1)) . x) + ((partdiff`1 (f,z2)) . x) by A2, A3, LOPBAN_8:12 ; :: thesis: verum

end;

hence partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) by LOPBAN_1:35; :: thesis: verum

end;

A4: now :: thesis: for z1 being Point of [:E,F:]
for a being Real holds partdiff`1 (f,(a * z1)) = a * (partdiff`1 (f,z1))

let z1 be Point of [:E,F:]; :: thesis: for a being Real holds partdiff`1 (f,(a * z1)) = a * (partdiff`1 (f,z1))
let a be Real; :: thesis: partdiff`1 (f,(a * z1)) = a * (partdiff`1 (f,z1))
for x being VECTOR of E holds (partdiff`1 (f,(a * z1))) . x = a * ((partdiff`1 (f,z1)) . x)

proof

let x be VECTOR of E; :: thesis: (partdiff`1 (f,(a * z1))) . x = a * ((partdiff`1 (f,z1)) . x)
A5: (partdiff`1 (f,z1)) . x = (f * (reproj1 z1)) . x by Th4
.= f . ((reproj1 z1) . x) by FUNCT_2:15
.= f . (x,(z1 `2)) by NDIFF_7:def 1 ;
thus (partdiff`1 (f,(a * z1))) . x = (f * (reproj1 (a * z1))) . x by Th4
.= f . ((reproj1 (a * z1)) . x) by FUNCT_2:15
.= f . [x,((a * z1) `2)] by NDIFF_7:def 1
.= f . (x,(a * (z1 `2))) by Th5
.= a * ((partdiff`1 (f,z1)) . x) by A5, LOPBAN_8:12 ; :: thesis: verum

end;

hence partdiff`1 (f,(a * z1)) = a * (partdiff`1 (f,z1)) by LOPBAN_1:36; :: thesis: verum

end;

now :: thesis: for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2))

let z1, z2 be Point of [:E,F:]; :: thesis: partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2))
thus partdiff`1 (f,(z1 - z2)) = partdiff`1 (f,(z1 + ((- 1) * z2))) by RLVECT_1:16
.= (partdiff`1 (f,z1)) + (partdiff`1 (f,((- 1) * z2))) by A1
.= (partdiff`1 (f,z1)) + ((- 1) * (partdiff`1 (f,z2))) by A4
.= (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) by RLVECT_1:16 ; :: thesis: verum

end;

hence ( ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`1 (f,(a * z)) = a * (partdiff`1 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) ) ) by A1, A4; :: thesis: verum