let f be real-valued with_values_greater_or_equal_one FinSequence; :: thesis: Product f >= 1
defpred S₁[ FinSequence of REAL ] means for g being real-valued with_values_greater_or_equal_one FinSequence st g = $1 holds
Product $1 >= 1;
A1: S₁[ <*> REAL] by RVSUM_1:94;
A2: for p being FinSequence of REAL
for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
let g be real-valued with_values_greater_or_equal_one FinSequence; :: thesis: ( g = p ^ <*x*> implies Product (p ^ <*x*>) >= 1 )
assume A4: g = p ^ <*x*> ; :: thesis: Product (p ^ <*x*>) >= 1
<*x*> is with_values_greater_or_equal_one by A4, Th19;
then A5: x >= 1 by Th20;
p is with_values_greater_or_equal_one by A4, Th19;
then A6: Product p >= 1 by A3;
Product (p ^ <*x*>) = x * (Product p) by RVSUM_1:96;
then Product (p ^ <*x*>) >= 1 * 1 by A5, A6, XREAL_1:66;
hence Product (p ^ <*x*>) >= 1 ; :: thesis: verum

end;

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