let ps be non empty FinSequence of REAL ; :: thesis: for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds
ps . i > x ) holds
Product ps > x

let x be Real; :: thesis: ( x >= 1 & ( for i being Element of NAT st i in dom ps holds
ps . i > x ) implies Product ps > x )

assume that
A1: x >= 1 and
A2: for j being Element of NAT st j in dom ps holds
ps . j > x ; :: thesis: Product ps > x
consider ps1 being FinSequence, y being object such that
A3: ps = ps1 ^ <*y*> by FINSEQ_1:46;
<*y*> is FinSequence of REAL by ;
then rng <*y*> c= REAL by FINSEQ_1:def 4;
then {y} c= REAL by FINSEQ_1:38;
then reconsider y2 = y as Element of REAL by ZFMISC_1:31;
defpred S1[ Nat] means for f being FinSequence of REAL st len f = \$1 & ( for j being Element of NAT st j in dom f holds
f . j > x ) holds
() * y2 > x;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let f be FinSequence of REAL ; :: thesis: ( len f = k + 1 & ( for j being Element of NAT st j in dom f holds
f . j > x ) implies () * y2 > x )

assume that
A6: len f = k + 1 and
A7: for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: () * y2 > x
f <> {} by A6;
then consider v being FinSequence, w being object such that
A8: f = v ^ <*w*> by FINSEQ_1:46;
reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by ;
rng f2 c= REAL ;
then {w} c= REAL by FINSEQ_1:38;
then reconsider m = w as Element of REAL by ZFMISC_1:31;
k + 1 = (len f1) + (len f2) by ;
then A9: k + 1 = (len f1) + 1 by FINSEQ_1:39;
then A10: f . (len f) = m by ;
len f in Seg (len f) by ;
then A11: len f in dom f by FINSEQ_1:def 3;
then m > 1 by ;
then A12: x * m > x by ;
A13: for j being Element of NAT st j in dom f1 holds
f1 . j > x
proof
A14: dom f1 c= dom f by ;
let j be Element of NAT ; :: thesis: ( j in dom f1 implies f1 . j > x )
assume A15: j in dom f1 ; :: thesis: f1 . j > x
f . j = f1 . j by ;
hence f1 . j > x by A7, A15, A14; :: thesis: verum
end;
Product f = (Product f1) * m by ;
then A16: (Product f) * y2 = ((Product f1) * y2) * m ;
m > x by A7, A10, A11;
then (Product f) * y2 > x * m by ;
hence (Product f) * y2 > x by ; :: thesis: verum
end;
len ps in Seg (len ps) by FINSEQ_1:3;
then A17: len ps in dom ps by FINSEQ_1:def 3;
reconsider q = ps1 as FinSequence of REAL by ;
A18: for j being Element of NAT st j in dom q holds
q . j > x
proof
A19: dom q c= dom ps by ;
let j be Element of NAT ; :: thesis: ( j in dom q implies q . j > x )
assume A20: j in dom q ; :: thesis: q . j > x
ps . j = q . j by ;
hence q . j > x by A2, A20, A19; :: thesis: verum
end;
A21: len q = len q ;
len ps = (len ps1) + () by ;
then len ps = (len ps1) + 1 by FINSEQ_1:39;
then A22: ps . (len ps) = y2 by ;
A23: S1[ 0 ]
proof
let f be FinSequence of REAL ; :: thesis: ( len f = 0 & ( for j being Element of NAT st j in dom f holds
f . j > x ) implies () * y2 > x )

assume that
A24: len f = 0 and
for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: () * y2 > x
f = <*> REAL by A24;
then Product f = 1 by RVSUM_1:94;
hence (Product f) * y2 > x by A2, A22, A17; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A23, A4);
then (Product q) * y2 > x by ;
hence Product ps > x by ; :: thesis: verum