let S, T be RealNormSpace; :: thesis: for i being Nat holds (diff_SP (S,T)) . i is RealNormSpace
defpred S₁[ Nat] means (diff_SP (S,T)) . $1 is RealNormSpace;
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]
then reconsider H = (diff_SP (S,T)) . i as RealNormSpace ;
modetrans ((diff_SP (S,T)) . i) = H by Def1;
then (diff_SP (S,T)) . (i + 1) = R_NormSpace_of_BoundedLinearOperators (S,H) by Def2;
hence S₁[i + 1] ; :: thesis: verum

end;

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