let E, F be RealNormSpace; :: thesis: for Z being Subset of E
for g being PartFunc of E,F
for f being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) st (g | Z) `| Z = f | Z holds
for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z)
let Z be Subset of E; :: thesis: for g being PartFunc of E,F
for f being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) st (g | Z) `| Z = f | Z holds
for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z)
let g be PartFunc of E,F; :: thesis: for f being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) st (g | Z) `| Z = f | Z holds
for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z)
let f be PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: ( (g | Z) `| Z = f | Z implies for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z) )
assume A1: (g | Z) `| Z = f | Z ; :: thesis: for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z)
defpred S<sub>1</sub>[ Nat] means diff (g,($1 + 1),Z) = diff (f,$1,Z);
diff (g,(0 + 1),Z) = (g | Z) `| Z by NDIFF_6:11
.= diff (f,0,Z) by A1, NDIFF_6:11 ;
then A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
thus diff (g,((i + 1) + 1),Z) = (diff (g,(i + 1),Z)) `| Z by NDIFF_6:13
.= (diff (f,i,Z)) `| Z by A4, Th30
.= diff (f,(i + 1),Z) by NDIFF_6:13 ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z) ; :: thesis: verum