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, Def3;
reconsider N9 = N as reflexive transitive RelStr by A4, Def3;
[:M9,N9:] is reflexive ;
hence A5: [:M,N:] is quasi_ordered by Def3; :: 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 Element of NAT st
( i < j & f . i <= f . j )

proof

let f be sequence of [:Me,Ne:]; :: thesis: ex i, j being Element of NAT st
( i < j & f . i <= f . j )
deffunc H₁( Element of NAT ) -> Element of the carrier of Me = (f . $1) `1 ;
consider a being Function of NAT, the carrier of Me such that
A6: for x being Element of NAT holds a . x = H<sub>1</sub>(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, Th36;
consider NS being increasing sequence of NAT such that
A9: sa = a * NS by A7, VALUED_0:def 17;
deffunc H<sub>2</sub>( Element of NAT ) -> Element of the carrier of Ne = (f . (NS . $1)) `2 ;
consider b being Function of NAT, the carrier of Ne such that
A10: for x being Element of NAT holds b . x = H₂(x) from FUNCT_2:sch 4();
reconsider b = b as sequence of Ne ;
consider i, j being Element of NAT such that
A11: i < j and
A12: b . i <= b . j by A2, Th30;
take NS . i ; :: thesis: ex j being Element of 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; :: thesis: f . (NS . i) <= f . (NS . j)
reconsider x = f . (NS . i), y = f . (NS . j) as Element of [:Me,Ne:] ;
A13: dom sa = NAT by FUNCT_2:def 1;
then A14: sa . i = a . (NS . i) by A9, FUNCT_1:12
.= (f . (NS . i)) `1 by A6 ;
A15: sa . j = a . (NS . j) by A9, A13, FUNCT_1:12
.= (f . (NS . j)) `1 by A6 ;
M is transitive by A3, Def3;
then A16: x `1 <= y `1 by A8, A11, A14, A15, Th4;
A17: b . i = x `2 by A10;
b . j = y `2 by A10;
hence f . (NS . i) <= f . (NS . j) by A12, A16, A17, 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, Th32;
hence [:M,N:] is Dickson by A5, Th33; :: thesis: verum

end;

suppose A18: ( M is empty or N is empty ) ; :: thesis: [:M,N:] is Dickson

now

per cases ( M is empty or N is empty ) by A18;

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 Th37; :: thesis: verum

end;

end;