defpred S₁[ FinSequence of NAT ] means Sum $1 is Element of NAT ;

A1: now :: thesis: for fp being FinSequence of NAT
for a being Element of NAT st S₁[fp] holds
S₁[fp ^ <*a*>]

let fp be FinSequence of NAT ; :: thesis: for a being Element of NAT st S₁[fp] holds
S₁[fp ^ <*a*>]
let a be Element of NAT ; :: thesis: ( S₁[fp] implies S₁[fp ^ <*a*>] )
assume S₁[fp] ; :: thesis: S₁[fp ^ <*a*>]
then reconsider sp = Sum fp as Element of NAT ;
Sum (fp ^ <*a*>) = sp + a by RVSUM_1:74;
hence S₁[fp ^ <*a*>] ; :: thesis: verum

end;

A2: S₁[ <*> NAT] by RVSUM_1:72;
for fp being FinSequence of NAT holds S₁[fp] from FINSEQ_2:sch 2(A2, A1);
hence Sum fp is Element of NAT ; :: thesis: verum