defpred S₁[ non empty Nat] means for p being RelStr-yielding ManySortedSet of $1 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 1; :: 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 n + 1; :: 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;
A9: n in NAT by ORDINAL1:def 13;
n < n + 1 by NAT_1:13;
then n in n + 1 by A8, A9;
then reconsider ne = n as Element of n + 1 ;
reconsider pns = p | ns as RelStr-yielding ManySortedSet of n ;
A10: 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 )
A11: pns . i = p . i by FUNCT_1:72;
A12: 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
A13: k = i and
A14: k < n by A12;
k < n + 1 by A14, NAT_1:13;
then i in n + 1 by A8, A13;
then reconsider i9 = i as Element of n + 1 ;
i9 = i ;
hence ( pns . i is Dickson & pns . i is quasi_ordered ) by A7, A11; :: thesis: verum

end;

then A15: product pns is Dickson by A6;
A16: product pns is quasi_ordered by A6, A10;
A17: p . ne is Dickson by A7;
A18: p . ne is quasi_ordered by A7;
then A19: [:(product (p | ns)),(p . ne):] is Dickson by A15, A16, A17, Th38;
A20: [:(product (p | ns)),(p . ne):] is quasi_ordered by A15, A16, A17, A18, Th38;
[:(product (p | ns)),(p . ne):], product p are_isomorphic by Th42;
hence ( product p is quasi_ordered & product p is Dickson ) by A19, A20, Th39; :: thesis: verum

end;

end;

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