let i be Nat; :: thesis: for X being natural-valued positive-yielding XFinSequence st i in dom X holds
X . i <= Product X

defpred S1[ Nat] means for X being natural-valued positive-yielding XFinSequence
for i being Nat st len X = \$1 & i in dom X holds
X . i <= Product X;
A1: S1[ 0 ] by XBOOLE_0:def 1;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A3: S1[n] ; :: thesis: S1[n + 1]
let X be natural-valued positive-yielding XFinSequence; :: thesis: for i being Nat st len X = n + 1 & i in dom X holds
X . i <= Product X

let i be Nat; :: thesis: ( len X = n + 1 & i in dom X implies X . i <= Product X )
assume A4: ( len X = n + 1 & i in dom X ) ; :: thesis: X . i <= Product X
then X = (X | n) ^ <%(X . n)%> by AFINSQ_1:56;
then A5: Product X = (Product (X | n)) * (Product <%(X . n)%>) by Th7
.= (Product (X | n)) * (X . n) by Th5 ;
A6: n < n + 1 by NAT_1:13;
then A7: ( n in dom X & len (X | n) = n ) by ;
then ( Product (X | n) > 0 & X . n in rng X ) by FUNCT_1:def 3;
then A8: ( X . n > 0 & Product (X | n) >= 1 ) by ;
then A9: X . n >= 1 by NAT_1:14;
i < len X by ;
then i <= n by ;
per cases then ( i = n or i < n ) by XXREAL_0:1;
suppose i = n ; :: thesis: X . i <= Product X
then Product X >= (X . i) * 1 by ;
hence X . i <= Product X ; :: thesis: verum
end;
suppose A10: i < n ; :: thesis: X . i <= Product X
then A11: i in dom (X | n) by ;
Product (X | n) >= (X | n) . i by ;
then ( Product X >= ((X | n) . i) * 1 & (X | n) . i = X . i ) by ;
hence X . i <= Product X ; :: thesis: verum
end;
end;
end;
A12: for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
let X be natural-valued positive-yielding XFinSequence; :: thesis: ( i in dom X implies X . i <= Product X )
thus ( i in dom X implies X . i <= Product X ) by A12; :: thesis: verum