let M, N be RelStr ; :: thesis: ( M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered implies ( [:M,N:] is quasi_ordered & [:M,N:] is Dickson ) )
assume that
A1: M is Dickson and
A2: N is Dickson and
A3: M is quasi_ordered and
A4: N is quasi_ordered ; :: thesis: ( [:M,N:] is quasi_ordered & [:M,N:] is Dickson )
reconsider M9 = M as reflexive transitive RelStr by A3;
reconsider N9 = N as reflexive transitive RelStr by A4;
[:M9,N9:] is reflexive ;
hence A5: [:M,N:] is quasi_ordered ; :: thesis: [:M,N:] is Dickson
per cases ( ( not M is empty & not N is empty ) or M is empty or N is empty ) ;
suppose ( not M is empty & not N is empty ) ; :: thesis: [:M,N:] is Dickson
then reconsider Me = M, Ne = N as non empty RelStr ;
set CPMN = [:Me,Ne:];
for f being sequence of [:Me,Ne:] ex i, j being Nat st
( i < j & f . i <= f . j )
proof
let f be sequence of [:Me,Ne:]; :: thesis: ex i, j being Nat st
( i < j & f . i <= f . j )
deffunc H1( Element of NAT ) -> Element of the carrier of Me = (f . $1) `1 ;
consider a being sequence of the carrier of Me such that
A6: for x being Element of NAT holds a . x = H1(x) from FUNCT_2:sch 4();
 reconsider a = a as sequence of Me ;
consider sa being sequence of Me such that
A7: sa is subsequence of a and
A8: sa is weakly-ascending by A1, Th34;
consider NS being increasing sequence of NAT such that
A9: sa = a * NS by A7, VALUED_0:def 17;
deffunc H2( Element of NAT ) -> Element of the carrier of Ne = (f . (NS . $1)) `2 ;
consider b being sequence of the carrier of Ne such that
A10: for x being Element of NAT holds b . x = H2(x) from FUNCT_2:sch 4();
 reconsider b = b as sequence of Ne ;
consider i, j being Nat such that
A11: i < j and
A12: b . i <= b . j by A2, Th28;
A13: i in NAT by ORDINAL1:def 12;
A14: j in NAT by ORDINAL1:def 12;
take NS . i ; :: thesis: ex j being Nat st
( NS . i < j & f . (NS . i) <= f . j )
take NS . j ; :: thesis: ( NS . i < NS . j & f . (NS . i) <= f . (NS . j) )
dom NS = NAT by FUNCT_2:def 1;
hence NS . i < NS . j by A11, VALUED_0:def 13, A13, A14; :: thesis: f . (NS . i) <= f . (NS . j)
reconsider x = f . (NS . i), y = f . (NS . j) as Element of [:Me,Ne:] ;
A15: dom sa = NAT by FUNCT_2:def 1;
then A16: sa . i = a . (NS . i) by A9, FUNCT_1:12, A13
.= (f . (NS . i)) `1 by A6 ;
A17: sa . j = a . (NS . j) by A9, A15, FUNCT_1:12, A14
.= (f . (NS . j)) `1 by A6 ;
M is transitive by A3;
then A18: x `1 <= y `1 by A8, A11, A16, A17, Th3;
A19: b . i = x `2 by A10, A13;
b . j = y `2 by A10, A14;
hence f . (NS . i) <= f . (NS . j) by A12, A18, A19, YELLOW_3:12; :: thesis: verum
end;
then for N being non empty Subset of [:Me,Ne:] holds
( min-classes N is finite & not min-classes N is empty ) by A5, Th30;
hence [:M,N:] is Dickson by A5, Th31; :: thesis: verum
end;
suppose A20: ( M is empty or N is empty ) ; :: thesis: [:M,N:] is Dickson
now :: thesis: [: the carrier of M, the carrier of N:] is empty
per cases ( M is empty or N is empty ) by A20;
suppose M is empty ; :: thesis: [: the carrier of M, the carrier of N:] is empty
then reconsider M2 = the carrier of M as empty set ;
[:M2, the carrier of N:] is empty ;
hence [: the carrier of M, the carrier of N:] is empty ; :: thesis: verum
end;
suppose N is empty ; :: thesis: [: the carrier of M, the carrier of N:] is empty
then reconsider N2 = the carrier of N as empty set ;
[: the carrier of M,N2:] is empty ;
hence [: the carrier of M, the carrier of N:] is empty ; :: thesis: verum
end;
end;
end;
then [:M,N:] is empty by YELLOW_3:def 2;
hence [:M,N:] is Dickson by Th35; :: thesis: verum
end;
end;