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,Z)) . i is PartFunc of S,(diff_SP (i,S,T))
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for i being Nat holds (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T))
let Z be Subset of S; :: thesis: for i being Nat holds (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T))
defpred S₁[ Nat] means (diff (f,Z)) . $1 is PartFunc of S,(diff_SP ($1,S,T));
(diff (f,Z)) . 0 = f | Z by Def5;
then A1: S₁[ 0 ] by Th7;

A2: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
A3: (diff (f,Z)) . (i + 1) = (modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T)))) `| Z by Def5;
diff_SP ((i + 1),S,T) = R_NormSpace_of_BoundedLinearOperators (S,(modetrans ((diff_SP (S,T)) . i))) by Def2
.= R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,T))) by Def1 ;
hence S₁[i + 1] by A3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for i being Nat holds (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) ; :: thesis: verum