A0: fr is FinSequence of INT by FINSEQ_1:102;
defpred S₁[ FinSequence of INT ] means Product fr is Integer;

A1: now :: thesis: for s being FinSequence of INT
for m being Element of INT st S₁[s] holds
S₁[s ^ <*m*>]

let s be FinSequence of INT ; :: thesis: for m being Element of INT st S₁[s] holds
S₁[s ^ <*m*>]
let m be Element of INT ; :: thesis: ( S₁[s] implies S₁[s ^ <*m*>] )
reconsider k = m as Integer ;
assume S₁[s] ; :: thesis: S₁[s ^ <*m*>]
then reconsider pis = Product s as Integer ;
Product (s ^ <*m*>) = pis * k by RVSUM_1:96;
hence S₁[s ^ <*m*>] ; :: thesis: verum

end;

A2: S₁[ <*> INT] by RVSUM_1:94;
for fr1 being FinSequence of INT holds S₁[fr1] from FINSEQ_2:sch 2(A2, A1);
hence Product fr is integer by A0; :: thesis: verum