defpred S_{1}[ Nat] means for X1, X2 being natural-valued XFinSequence st len X1 = $1 & $1 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) holds

Product X1 <= Product X2;

A1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

hence for X1, X2 being natural-valued XFinSequence st len X1 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) holds

Product X1 <= Product X2 ; :: thesis: verum

X1 . n <= X2 . n ) holds

Product X1 <= Product X2;

A1: S

proof

A2:
for n being Nat st S
let X1, X2 be natural-valued XFinSequence; :: thesis: ( len X1 = 0 & 0 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) implies Product X1 <= Product X2 )

assume ( len X1 = 0 & 0 = len X2 ) ; :: thesis: ( ex n being Nat st

( n in dom X1 & not X1 . n <= X2 . n ) or Product X1 <= Product X2 )

then ( X1 = {} & {} = X2 ) ;

hence ( ex n being Nat st

( n in dom X1 & not X1 . n <= X2 . n ) or Product X1 <= Product X2 ) ; :: thesis: verum

end;X1 . n <= X2 . n ) implies Product X1 <= Product X2 )

assume ( len X1 = 0 & 0 = len X2 ) ; :: thesis: ( ex n being Nat st

( n in dom X1 & not X1 . n <= X2 . n ) or Product X1 <= Product X2 )

then ( X1 = {} & {} = X2 ) ;

hence ( ex n being Nat st

( n in dom X1 & not X1 . n <= X2 . n ) or Product X1 <= Product X2 ) ; :: thesis: verum

S

proof

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 X1, X2 be natural-valued XFinSequence; :: thesis: ( len X1 = n + 1 & n + 1 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) implies Product X1 <= Product X2 )

assume that

A4: ( len X1 = n + 1 & n + 1 = len X2 ) and

A5: for i being Nat st i in dom X1 holds

X1 . i <= X2 . i ; :: thesis: Product X1 <= Product X2

X1 = (X1 | n) ^ <%(X1 . n)%> by A4, AFINSQ_1:56;

then A6: Product X1 = (Product (X1 | n)) * (Product <%(X1 . n)%>) by Th7

.= (Product (X1 | n)) * (X1 . n) by Th5 ;

X2 = (X2 | n) ^ <%(X2 . n)%> by A4, AFINSQ_1:56;

then A7: Product X2 = (Product (X2 | n)) * (Product <%(X2 . n)%>) by Th7

.= (Product (X2 | n)) * (X2 . n) by Th5 ;

A8: n < n + 1 by NAT_1:13;

then A9: ( n in dom X1 & len (X1 | n) = n & n = len (X2 | n) ) by A4, AFINSQ_1:54, AFINSQ_1:66;

A10: X1 . n <= X2 . n by A5, A8, A4, AFINSQ_1:66;

for i being Nat st i in dom (X1 | n) holds

(X1 | n) . i <= (X2 | n) . i

hence Product X1 <= Product X2 by A6, A7, A10, XREAL_1:66; :: thesis: verum

end;set n1 = n + 1;

assume A3: S

let X1, X2 be natural-valued XFinSequence; :: thesis: ( len X1 = n + 1 & n + 1 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) implies Product X1 <= Product X2 )

assume that

A4: ( len X1 = n + 1 & n + 1 = len X2 ) and

A5: for i being Nat st i in dom X1 holds

X1 . i <= X2 . i ; :: thesis: Product X1 <= Product X2

X1 = (X1 | n) ^ <%(X1 . n)%> by A4, AFINSQ_1:56;

then A6: Product X1 = (Product (X1 | n)) * (Product <%(X1 . n)%>) by Th7

.= (Product (X1 | n)) * (X1 . n) by Th5 ;

X2 = (X2 | n) ^ <%(X2 . n)%> by A4, AFINSQ_1:56;

then A7: Product X2 = (Product (X2 | n)) * (Product <%(X2 . n)%>) by Th7

.= (Product (X2 | n)) * (X2 . n) by Th5 ;

A8: n < n + 1 by NAT_1:13;

then A9: ( n in dom X1 & len (X1 | n) = n & n = len (X2 | n) ) by A4, AFINSQ_1:54, AFINSQ_1:66;

A10: X1 . n <= X2 . n by A5, A8, A4, AFINSQ_1:66;

for i being Nat st i in dom (X1 | n) holds

(X1 | n) . i <= (X2 | n) . i

proof

then
Product (X1 | n) <= Product (X2 | n)
by A3, A9;
let i be Nat; :: thesis: ( i in dom (X1 | n) implies (X1 | n) . i <= (X2 | n) . i )

assume i in dom (X1 | n) ; :: thesis: (X1 | n) . i <= (X2 | n) . i

then ( (X1 | n) . i = X1 . i & (X2 | n) . i = X2 . i & i in dom X1 ) by A8, A4, A9, AFINSQ_1:53;

hence (X1 | n) . i <= (X2 | n) . i by A5; :: thesis: verum

end;assume i in dom (X1 | n) ; :: thesis: (X1 | n) . i <= (X2 | n) . i

then ( (X1 | n) . i = X1 . i & (X2 | n) . i = X2 . i & i in dom X1 ) by A8, A4, A9, AFINSQ_1:53;

hence (X1 | n) . i <= (X2 | n) . i by A5; :: thesis: verum

hence Product X1 <= Product X2 by A6, A7, A10, XREAL_1:66; :: thesis: verum

hence for X1, X2 being natural-valued XFinSequence st len X1 = len X2 & ( for n being Nat st n in dom X1 holds

X1 . n <= X2 . n ) holds

Product X1 <= Product X2 ; :: thesis: verum