defpred S1[ 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 S1[fp] holds
S1[fp ^ <*a*>]
let fp be FinSequence of NAT ; :: thesis: for a being Element of NAT st S1[fp] holds
S1[fp ^ <*a*>]
let a be Element of NAT ; :: thesis: ( S1[fp] implies S1[fp ^ <*a*>] )
assume S1[fp] ; :: thesis: S1[fp ^ <*a*>]
then reconsider sp = Product fp as Element of NAT ;
Product (fp ^ <*a*>) = sp * a by RVSUM_1:96;
hence S1[fp ^ <*a*>] ; :: thesis: verum
end;
A2: S1[ <*> NAT] by RVSUM_1:94;
for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch 2(A2, A1);
 hence Product fp is Element of NAT ; :: thesis: verum