defpred S₁[ 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₁[ 0 ]

proof

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;

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

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;

then Product (X1 | n) <= Product (X2 | n) by A3, A9;
hence Product X1 <= Product X2 by A6, A7, A10, XREAL_1:66; :: thesis: verum

end;

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