defpred S1[ FinSequence of INT ] means Product fr is Integer;
A1: now :: thesis: for s being FinSequence of INT
for m being Element of INT st S1[s] holds
S1[s ^ <*m*>]
let s be FinSequence of INT ; :: thesis: for m being Element of INT st S1[s] holds
S1[s ^ <*m*>]
let m be Element of INT ; :: thesis: ( S1[s] implies S1[s ^ <*m*>] )
reconsider k = m as Integer ;
assume S1[s] ; :: thesis: S1[s ^ <*m*>]
then reconsider pis = Product s as Integer ;
Product (s ^ <*m*>) = pis * k by RVSUM_1:96;
hence S1[s ^ <*m*>] ; :: thesis: verum
end;
A2: S1[ <*> INT] by RVSUM_1:94;
for fr1 being FinSequence of INT holds S1[fr1] from FINSEQ_2:sch 2(A2, A1);
 hence Product fr is integer ; :: thesis: verum