let E, F be RealNormSpace; :: thesis: for i being Nat holds diff_SP ((i + 1),E,F) = diff_SP (i,E,(R_NormSpace_of_BoundedLinearOperators (E,F)))
defpred S₁[ Nat] means diff_SP (($1 + 1),E,F) = diff_SP ($1,E,(R_NormSpace_of_BoundedLinearOperators (E,F)));
diff_SP ((0 + 1),E,F) = R_NormSpace_of_BoundedLinearOperators (E,F) by NDIFF_6:7
.= diff_SP (0,E,(R_NormSpace_of_BoundedLinearOperators (E,F))) by NDIFF_6:7 ;
then A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
thus diff_SP (((i + 1) + 1),E,F) = R_NormSpace_of_BoundedLinearOperators (E,(diff_SP ((i + 1),E,F))) by NDIFF_6:10
.= diff_SP ((i + 1),E,(R_NormSpace_of_BoundedLinearOperators (E,F))) by A3, NDIFF_6:10 ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence for i being Nat holds diff_SP ((i + 1),E,F) = diff_SP (i,E,(R_NormSpace_of_BoundedLinearOperators (E,F))) ; :: thesis: verum