let n be Nat; :: thesis: for f being real-valued with_values_greater_or_equal_one FinSequence holds Product (f | n) <= Product f
let f be real-valued with_values_greater_or_equal_one FinSequence; :: thesis: Product (f | n) <= Product f

per cases ( n <= len f or n > len f ) ;

suppose A1: n <= len f ; :: thesis: Product (f | n) <= Product f

defpred S₁[ FinSequence of REAL ] means for g being real-valued with_values_greater_or_equal_one FinSequence st g = $1 & n <= len g holds
Product (g | n) <= Product g;
A2: S₁[ <*> REAL] ;
A3: 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 A4: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
let g be real-valued with_values_greater_or_equal_one FinSequence; :: thesis: ( g = p ^ <*x*> & n <= len g implies Product (g | n) <= Product g )
assume that
A5: g = p ^ <*x*> and
A6: n <= len g ; :: thesis: Product (g | n) <= Product g
A7: len g = (len p) + (len <*x*>) by A5, FINSEQ_1:22;
A8: len <*x*> = 1 by FINSEQ_1:39;

per cases then ( n < (len p) + 1 or n = (len p) + 1 ) by A6, A7, XXREAL_0:1;

suppose A9: n < (len p) + 1 ; :: thesis: Product (g | n) <= Product g

then n <= len p by NAT_1:13;
then A10: (p ^ <*x*>) | n = p | n by FINSEQ_5:22;
A11: Product g = (Product p) * x by A5, RVSUM_1:96;
A12: ( p is with_values_greater_or_equal_one & p is real-valued ) by A5, Th19;
then A13: Product (p | n) <= Product p by A4, A9, NAT_1:13;
( <*x*> is with_values_greater_or_equal_one & <*x*> is real-valued ) by A5, Th19;
then (Product p) * 1 <= (Product p) * x by A12, XREAL_1:64, Th20;
hence Product (g | n) <= Product g by A5, A10, A11, A13, XXREAL_0:2; :: thesis: verum

end;

suppose n = (len p) + 1 ; :: thesis: Product (g | n) <= Product g

hence Product (g | n) <= Product g by A7, A8; :: thesis: verum

end;

end;

end;

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

end;

suppose n > len f ; :: thesis: Product (f | n) <= Product f

hence Product (f | n) <= Product f by FINSEQ_1:58; :: thesis: verum

end;

end;