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

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

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

proof

let x be VECTOR of [:E,F:]; :: thesis: (diff (f,(z1 + z2))) . x = ((diff (f,z1)) . x) + ((diff (f,z2)) . x)
consider dx being Point of E, dy being Point of F such that
A2: x = [dx,dy] by PRVECT_3:18;
A3: (diff (f,(z1 + z2))) . x = (diff (f,(z1 + z2))) . (dx,dy) by A2
.= ((partdiff`1 (f,(z1 + z2))) . dx) + ((partdiff`2 (f,(z1 + z2))) . dy) by Th12
.= (((partdiff`1 (f,z1)) + (partdiff`1 (f,z2))) . dx) + ((partdiff`2 (f,(z1 + z2))) . dy) by Th7
.= (((partdiff`1 (f,z1)) + (partdiff`1 (f,z2))) . dx) + (((partdiff`2 (f,z1)) + (partdiff`2 (f,z2))) . dy) by Th8
.= (((partdiff`1 (f,z1)) . dx) + ((partdiff`1 (f,z2)) . dx)) + (((partdiff`2 (f,z1)) + (partdiff`2 (f,z2))) . dy) by LOPBAN_1:35
.= (((partdiff`1 (f,z1)) . dx) + ((partdiff`1 (f,z2)) . dx)) + (((partdiff`2 (f,z1)) . dy) + ((partdiff`2 (f,z2)) . dy)) by LOPBAN_1:35
.= ((((partdiff`1 (f,z1)) . dx) + ((partdiff`1 (f,z2)) . dx)) + ((partdiff`2 (f,z1)) . dy)) + ((partdiff`2 (f,z2)) . dy) by RLVECT_1:def 3
.= ((((partdiff`1 (f,z1)) . dx) + ((partdiff`2 (f,z1)) . dy)) + ((partdiff`1 (f,z2)) . dx)) + ((partdiff`2 (f,z2)) . dy) by RLVECT_1:def 3
.= (((partdiff`1 (f,z1)) . dx) + ((partdiff`2 (f,z1)) . dy)) + (((partdiff`1 (f,z2)) . dx) + ((partdiff`2 (f,z2)) . dy)) by RLVECT_1:def 3 ;
A4: ((partdiff`1 (f,z1)) . dx) + ((partdiff`2 (f,z1)) . dy) = (diff (f,z1)) . (dx,dy) by Th12
.= (diff (f,z1)) . x by A2 ;
((partdiff`1 (f,z2)) . dx) + ((partdiff`2 (f,z2)) . dy) = (diff (f,z2)) . (dx,dy) by Th12
.= (diff (f,z2)) . x by A2 ;
hence (diff (f,(z1 + z2))) . x = ((diff (f,z1)) . x) + ((diff (f,z2)) . x) by A3, A4; :: thesis: verum

end;

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

end;

A5: now :: thesis: for z1 being Point of [:E,F:]
for a being Real holds diff (f,(a * z1)) = a * (diff (f,z1))

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

proof

let x be VECTOR of [:E,F:]; :: thesis: (diff (f,(a * z1))) . x = a * ((diff (f,z1)) . x)
consider dx being Point of E, dy being Point of F such that
A6: x = [dx,dy] by PRVECT_3:18;
A7: ((partdiff`1 (f,z1)) . dx) + ((partdiff`2 (f,z1)) . dy) = (diff (f,z1)) . (dx,dy) by Th12
.= (diff (f,z1)) . x by A6 ;
thus (diff (f,(a * z1))) . x = (diff (f,(a * z1))) . (dx,dy) by A6
.= ((partdiff`1 (f,(a * z1))) . dx) + ((partdiff`2 (f,(a * z1))) . dy) by Th12
.= ((a * (partdiff`1 (f,z1))) . dx) + ((partdiff`2 (f,(a * z1))) . dy) by Th7
.= ((a * (partdiff`1 (f,z1))) . dx) + ((a * (partdiff`2 (f,z1))) . dy) by Th8
.= (a * ((partdiff`1 (f,z1)) . dx)) + ((a * (partdiff`2 (f,z1))) . dy) by LOPBAN_1:36
.= (a * ((partdiff`1 (f,z1)) . dx)) + (a * ((partdiff`2 (f,z1)) . dy)) by LOPBAN_1:36
.= a * ((diff (f,z1)) . x) by A7, RLVECT_1:def 5 ; :: thesis: verum

end;

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

end;

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

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

end;

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