let R, S be RelStr ; :: thesis: ( R,S are_isomorphic & R is Dickson & R is quasi_ordered implies ( S is quasi_ordered & S is Dickson ) )
assume that
A1: R,S are_isomorphic and
A2: R is Dickson and
A3: R is quasi_ordered ; :: thesis: ( S is quasi_ordered & S is Dickson )
set CRS = the carrier of S;
set IRS = the InternalRel of S;

per cases ( ( not R is empty & not S is empty ) or R is empty or S is empty ) ;

suppose ( not R is empty & not S is empty ) ; :: thesis: ( S is quasi_ordered & S is Dickson )

then reconsider Re = R, Se = S as non empty RelStr ;
consider f being Function of Re,Se such that
A4: f is isomorphic by A1, WAYBEL_1:def 8;
A5: f is one-to-one by A4, WAYBEL_0:66;
A6: rng f = the carrier of Se by A4, WAYBEL_0:66;
A7: Re is reflexive by A3;
A8: Re is transitive by A3;
A9: Se is reflexive by A1, A7, WAYBEL20:15;
Se is transitive by A1, A8, WAYBEL20:16;
hence A10: S is quasi_ordered by A9; :: thesis: S is Dickson

now :: thesis: for t being sequence of Se ex i, j being Nat st
( i < j & t . i <= t . j )

let t be sequence of Se; :: thesis: ex i, j being Nat st
( i < j & t . i <= t . j )
reconsider fi = f " as Function of the carrier of Se, the carrier of Re by A5, A6, FUNCT_2:25;
deffunc H₁( Element of NAT ) -> Element of the carrier of Re = fi . (t . $1);
consider sr being sequence of the carrier of Re such that
A11: for x being Element of NAT holds sr . x = H₁(x) from FUNCT_2:sch 4();
reconsider sr = sr as sequence of Re ;
consider i, j being Nat such that
A12: i < j and
A13: sr . i <= sr . j by A2, Th28;
take i = i; :: thesis: ex j being Nat st
( i < j & t . i <= t . j )
take j = j; :: thesis: ( i < j & t . i <= t . j )
A14: i in NAT by ORDINAL1:def 12;
A15: j in NAT by ORDINAL1:def 12;
thus i < j by A12; :: thesis: t . i <= t . j
A16: f . (sr . i) = f . ((f ") . (t . i)) by A11, A14
.= t . i by A5, A6, FUNCT_1:35 ;
f . (sr . j) = f . ((f ") . (t . j)) by A11, A15
.= t . j by A5, A6, FUNCT_1:35 ;
hence t . i <= t . j by A4, A13, A16, WAYBEL_0:66; :: thesis: verum

end;

then for N being non empty Subset of Se holds
( min-classes N is finite & not min-classes N is empty ) by A10, Th30;
hence S is Dickson by A10, Th31; :: thesis: verum

end;

suppose A17: ( R is empty or S is empty ) ; :: thesis: ( S is quasi_ordered & S is Dickson )

A18: now :: thesis: S is empty

per cases ( R is empty or S is empty ) by A17;

suppose A19: R is empty ; :: thesis: S is empty

ex f being Function of R,S st f is isomorphic by A1, WAYBEL_1:def 8;
hence S is empty by A19, WAYBEL_0:def 38; :: thesis: verum

end;

suppose S is empty ; :: thesis: S is empty

hence S is empty ; :: thesis: verum

end;

end;

end;

then for x being object st x in the carrier of S holds
[x,x] in the InternalRel of S ;
then A20: the InternalRel of S is_reflexive_in the carrier of S ;
for x, y, z being object st x in the carrier of S & y in the carrier of S & z in the carrier of S & [x,y] in the InternalRel of S & [y,z] in the InternalRel of S holds
[x,z] in the InternalRel of S by A18;
then A21: the InternalRel of S is_transitive_in the carrier of S ;
A22: S is reflexive by A20;
S is transitive by A21;
hence S is quasi_ordered by A22; :: thesis: S is Dickson
thus S is Dickson by A18, Th35; :: thesis: verum

end;

end;