defpred S₁[ FinSequence of NAT ] means Product $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 = Product fp as Element of NAT ;
Product (fp ^ <*a*>) = sp * a by RVSUM_1:96;
hence S₁[fp ^ <*a*>] ; :: thesis: verum

end;

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