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`2 (f,(z1 + z2)) = (partdiff`2 (f,z1)) + (partdiff`2 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`2 (f,(a * z)) = a * (partdiff`2 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`2 (f,(z1 - z2)) = (partdiff`2 (f,z1)) - (partdiff`2 (f,z2)) ) )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: ( ( for z1, z2 being Point of [:E,F:] holds partdiff`2 (f,(z1 + z2)) = (partdiff`2 (f,z1)) + (partdiff`2 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`2 (f,(a * z)) = a * (partdiff`2 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`2 (f,(z1 - z2)) = (partdiff`2 (f,z1)) - (partdiff`2 (f,z2)) ) )

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

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

proof

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

end;

hence partdiff`2 (f,(z1 + z2)) = (partdiff`2 (f,z1)) + (partdiff`2 (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`2 (f,(a * z1)) = a * (partdiff`2 (f,z1))

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

proof

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

end;

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

end;

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

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

end;

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