let E, F, G be RealNormSpace; :: thesis: for B being Lipschitzian BilinearOperator of E,F,G
for i being Nat holds
( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )
let B be Lipschitzian BilinearOperator of E,F,G; :: thesis: for i being Nat holds
( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )
reconsider L = B `| ([#] [:E,F:]) as Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) by Th15;
set G1 = R_NormSpace_of_BoundedLinearOperators ([:E,F:],G);
defpred S₁[ Nat] means ( diff (B,($1 + 1),([#] [:E,F:])) = diff (L,$1,([#] [:E,F:])) & diff_SP (($1 + 1),[:E,F:],G) = diff_SP ($1,[:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))) );
A1: S₁[ 0 ]

proof

thus diff (B,(0 + 1),([#] [:E,F:])) = (B | ([#] [:E,F:])) `| ([#] [:E,F:]) by NDIFF_6:11
.= L | ([#] [:E,F:])
.= diff (L,0,([#] [:E,F:])) by NDIFF_6:11 ; :: thesis: diff_SP ((0 + 1),[:E,F:],G) = diff_SP (0,[:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)))
thus diff_SP ((0 + 1),[:E,F:],G) = R_NormSpace_of_BoundedLinearOperators ([:E,F:],G) by NDIFF_6:7
.= diff_SP (0,[:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))) by NDIFF_6:7 ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
A4: diff_SP (((n + 1) + 1),[:E,F:],G) = R_NormSpace_of_BoundedLinearOperators ([:E,F:],(diff_SP ((n + 1),[:E,F:],G))) by NDIFF_6:10
.= diff_SP ((n + 1),[:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))) by A3, NDIFF_6:10 ;
diff (B,((n + 1) + 1),([#] [:E,F:])) = (diff (B,(n + 1),([#] [:E,F:]))) `| ([#] [:E,F:]) by NDIFF_6:13
.= diff (L,(n + 1),([#] [:E,F:])) by A3, NDIFF_6:13 ;
hence S₁[n + 1] by A4; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let i be Nat; :: thesis: ( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )

per cases ( i = 0 or i <> 0 ) ;

suppose A6: i = 0 ; :: thesis: ( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )

then A7: diff_SP (i,[:E,F:],G) = G by NDIFF_6:def 2;
B | ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] by Th14;
hence diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] by A6, A7, NDIFF_6:def 5; :: thesis: (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:]
(B | ([#] [:E,F:])) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] by Th14;
hence (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] by A6, A7, NDIFF_6:def 5; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )

then consider j being Nat such that
A8: i = j + 1 by NAT_1:6;
A9: diff (L,j,([#] [:E,F:])) = diff (B,i,([#] [:E,F:])) by A5, A8;
A10: diff_SP (j,[:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))) = diff_SP (i,[:E,F:],G) by A5, A8;
thus ( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] ) by A9, A10, Th20; :: thesis: verum

end;

end;