let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for i being Nat holds diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z
let Z be Subset of S; :: thesis: for i being Nat holds diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z
let i be Nat; :: thesis: diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z
A1: (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) by Th12;
A2: modetrans ((diff_SP (S,T)) . i) = (diff_SP (S,T)) . i by Def1, Th8;
then modetrans (((diff (f,Z)) . i),S,(modetrans ((diff_SP (S,T)) . i))) = (diff (f,Z)) . i by A1, Def4;
hence diff (f,(i + 1),Z) = (diff (f,i,Z)) `| Z by A2, Def5; :: thesis: verum