let E, F, G be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f is_partial_differentiable_in`1 z & partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: for z being Point of [:E,F:] holds
( f is_partial_differentiable_in`1 z & partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )
let z be Point of [:E,F:]; :: thesis: ( f is_partial_differentiable_in`1 z & partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )
reconsider L1 = f * (reproj1 z) as Lipschitzian LinearOperator of E,G by Th2;
reconsider L2 = f * (reproj2 z) as Lipschitzian LinearOperator of F,G by Th2;
A1: ( L1 is_differentiable_in z `1 & diff (L1,(z `1)) = L1 ) by NDIFF_7:26;
hence f is_partial_differentiable_in`1 z by NDIFF_7:def 4; :: thesis: ( partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )
thus partdiff`1 (f,z) = f * (reproj1 z) by A1, NDIFF_7:def 6; :: thesis: ( f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )
A2: ( L2 is_differentiable_in z `2 & diff (L2,(z `2)) = L2 ) by NDIFF_7:26;
hence f is_partial_differentiable_in`2 z by NDIFF_7:def 5; :: thesis: partdiff`2 (f,z) = f * (reproj2 z)
thus partdiff`2 (f,z) = f * (reproj2 z) by A2, NDIFF_7:def 7; :: thesis: verum