let i be Nat; :: thesis: for X being natural-valued positive-yielding XFinSequence st i in dom X holds
X . i <= Product X
defpred S₁[ 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: S₁[ 0 ] by XBOOLE_0:def 1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A3: S₁[n] ; :: thesis: S₁[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 A4, AFINSQ_1:54, AFINSQ_1:66;
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 PARTFUN3:def 1, NAT_1:14;
then A9: X . n >= 1 by NAT_1:14;
i < len X by A4, AFINSQ_1:66;
then i <= n by A4, NAT_1:13;

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 A5, A8, XREAL_1:66;
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 A7, AFINSQ_1:66;
Product (X | n) >= (X | n) . i by A3, A7, AFINSQ_1:66, A10;
then ( Product X >= ((X | n) . i) * 1 & (X | n) . i = X . i ) by A6, A4, AFINSQ_1:53, A11, A7, A5, A9, XREAL_1:66;
hence X . i <= Product X ; :: thesis: verum

end;

end;

end;

A12: for n being Nat holds S₁[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