defpred S₁[ non empty Nat] means for p being RelStr-yielding ManySortedSet of st ( for i being Element of $1 holds
( p . i is Dickson & p . i is quasi_ordered ) ) holds
( product p is quasi_ordered & product p is Dickson );
A1: S₁[1]

proof

let p be RelStr-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of 1 holds
( p . i is Dickson & p . i is quasi_ordered ) ) implies ( product p is quasi_ordered & product p is Dickson ) )
assume A2: for i being Element of 1 holds
( p . i is Dickson & p . i is quasi_ordered ) ; :: thesis: ( product p is quasi_ordered & product p is Dickson )
reconsider z = 0 as Element of 1 by CARD_1:87, TARSKI:def 1;
A3: p . z is Dickson by A2;
A4: p . z is quasi_ordered by A2;
p . z, product p are_isomorphic by Th40;
hence ( product p is quasi_ordered & product p is Dickson ) by A3, A4, Th39; :: thesis: verum

end;

A5: now

let n be non empty Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let p be RelStr-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of n + 1 holds
( p . i is Dickson & p . i is quasi_ordered ) ) implies ( product p is quasi_ordered & product p is Dickson ) )
assume A7: for i being Element of n + 1 holds
( p . i is Dickson & p . i is quasi_ordered ) ; :: thesis: ( product p is quasi_ordered & product p is Dickson )
n <= n + 1 by NAT_1:11;
then reconsider ns = n as Subset of (n + 1) by NAT_1:40;
A8: n + 1 = { k where k is Element of NAT : k < n + 1 } by AXIOMS:30;
X: n in NAT by ORDINAL1:def 13;
n < n + 1 by NAT_1:13;
then n in n + 1 by A8, X;
then reconsider ne = n as Element of n + 1 ;
reconsider pns = p | ns as RelStr-yielding ManySortedSet of ;
for i being Element of n holds
( pns . i is Dickson & pns . i is quasi_ordered )

proof

let i be Element of n; :: thesis: ( pns . i is Dickson & pns . i is quasi_ordered )
A9: pns . i = p . i by FUNCT_1:72;
A10: n = { k where k is Element of NAT : k < n } by AXIOMS:30;
i in n ;
then consider k being Element of NAT such that
A11: ( k = i & k < n ) by A10;
k < n + 1 by A11, NAT_1:13;
then i in n + 1 by A8, A11;
then reconsider i' = i as Element of n + 1 ;
i' = i ;
hence ( pns . i is Dickson & pns . i is quasi_ordered ) by A7, A9; :: thesis: verum

end;

then A12: ( product pns is Dickson & product pns is quasi_ordered ) by A6;
( p . ne is Dickson & p . ne is quasi_ordered ) by A7;
then A13: ( [:(product (p | ns)),(p . ne):] is Dickson & [:(product (p | ns)),(p . ne):] is quasi_ordered ) by A12, Th38;
[:(product (p | ns)),(p . ne):], product p are_isomorphic by Th42;
hence ( product p is quasi_ordered & product p is Dickson ) by A13, Th39; :: thesis: verum

end;

end;

thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A1, A5); :: thesis: verum