let E, F, G be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:]
for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: for z being Point of [:E,F:]
for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)
let z be Point of [:E,F:]; :: thesis: for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)
consider K being Real such that
A1: ( 0 <= K & ( for z being Point of [:E,F:] holds
( f is_differentiable_in z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ||.(diff (f,z)).|| <= K * ||.z.|| ) ) ) by Th11;
let dx be Point of E; :: thesis: for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)
let dy be Point of F; :: thesis: (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)
A2: (partdiff`1 (f,z)) . dx = (f * (reproj1 z)) . dx by Th4
.= f . ((reproj1 z) . dx) by FUNCT_2:15
.= f . (dx,(z `2)) by NDIFF_7:def 1 ;
(partdiff`2 (f,z)) . dy = (f * (reproj2 z)) . dy by Th4
.= f . ((reproj2 z) . dy) by FUNCT_2:15
.= f . ((z `1),dy) by NDIFF_7:def 2 ;
hence (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) by A1, A2; :: thesis: verum