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_{1}[ 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_{1}[ 0 ]
by XBOOLE_0:def 1;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[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

X . i <= Product X

defpred S

for i being Nat st len X = $1 & i in dom X holds

X . i <= Product X;

A1: S

A2: for n being Nat st S

S

proof

A12:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set n1 = n + 1;

assume A3: S_{1}[n]
; :: thesis: S_{1}[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;

end;set n1 = n + 1;

assume A3: S

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;

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;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

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