let f be integer-valued positive-yielding FinSequence; :: thesis: Product f >= 1
defpred S₁[ set ] means for F being integer-valued positive-yielding FinSequence st F = $1 holds
Product F >= 1;
A1: S₁[ <*> INT] by RVSUM_1:94;
A2: for p being FinSequence of INT
for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of INT ; :: thesis: for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of INT ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
let F be integer-valued positive-yielding FinSequence; :: thesis: ( F = p ^ <*x*> implies Product F >= 1 )
assume A4: F = p ^ <*x*> ; :: thesis: Product F >= 1
p is positive-yielding by A4, NUMBER08:37;
then A5: Product p >= 1 by A3;
A6: <*x*> is positive-yielding by A4, NUMBER08:37;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by FINSEQ_1:38;
then A7: x >= 0 + 1 by A6, INT_1:7;
Product F = (Product p) * x by A4, RVSUM_1:96;
then Product F >= 1 * 1 by A5, A7, XREAL_1:66;
hence Product F >= 1 ; :: thesis: verum

end;

A8: for p being FinSequence of INT holds S₁[p] from FINSEQ_2:sch 2(A1, A2);
f is FinSequence of INT by FINSEQ_1:104;
hence Product f >= 1 by A8; :: thesis: verum