defpred S1[ non zero Nat] means for p being RelStr-yielding ManySortedSet of Segm $1 st ( for i being Element of Segm $1 holds
( p . i is Dickson & p . i is quasi_ordered ) ) holds
( product p is quasi_ordered & product p is Dickson );
A1: S1[1]
proof
let p be RelStr-yielding ManySortedSet of Segm 1; :: thesis: ( ( for i being Element of Segm 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 Segm 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 Segm 1 by CARD_1:49, TARSKI:def 1;
A3: p . z is Dickson by A2;
A4: p . z is quasi_ordered by A2;
Segm 1 = {0} by CARD_1:49;
then p . z, product p are_isomorphic by Th38;
hence ( product p is quasi_ordered & product p is Dickson ) by A3, A4, Th37; :: thesis: verum
end;
A5: now :: thesis: for n being non zero Nat st S1[n] holds
S1[n + 1]
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let p be RelStr-yielding ManySortedSet of Segm (n + 1); :: thesis: ( ( for i being Element of Segm (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 Segm (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 = Segm n as Subset of (Segm (n + 1)) by NAT_1:39;
A8: n + 1 = { k where k is Nat : k < n + 1 } by AXIOMS:4;
n < n + 1 by NAT_1:13;
then n in n + 1 by A8;
then reconsider ne = n as Element of Segm (n + 1) ;
reconsider pns = p | ns as RelStr-yielding ManySortedSet of Segm n ;
A9: for i being Element of Segm n holds
( pns . i is Dickson & pns . i is quasi_ordered )
proof
let i be Element of Segm n; :: thesis: ( pns . i is Dickson & pns . i is quasi_ordered )
A10: pns . i = p . i by FUNCT_1:49;
A11: n = { k where k is Nat : k < n } by AXIOMS:4;
i in n ;
then consider k being Nat such that
A12: k = i and
A13: k < n by A11;
k < n + 1 by A13, NAT_1:13;
then i in n + 1 by A8, A12;
then reconsider i9 = i as Element of n + 1 ;
i9 = i ;
hence ( pns . i is Dickson & pns . i is quasi_ordered ) by A7, A10; :: thesis: verum
end;
then A14: product pns is Dickson by A6;
A15: product pns is quasi_ordered by A6, A9;
A16: p . ne is Dickson by A7;
A17: p . ne is quasi_ordered by A7;
then A18: [:(product (p | ns)),(p . ne):] is Dickson by A14, A15, A16, Th36;
A19: [:(product (p | ns)),(p . ne):] is quasi_ordered by A15, A17;
[:(product (p | ns)),(p . ne):], product p are_isomorphic by Th40;
hence ( product p is quasi_ordered & product p is Dickson ) by A18, A19, Th37; :: thesis: verum
end;
end;
thus for n being non zero Nat holds S1[n] from NAT_1:sch 10(A1, A5); :: thesis: verum