let L1, L2 be antisymmetric RelStr ; :: thesis:
let A1, B1 be Subset of L1; :: thesis:
assume A1: A1,B1 form_upper_lower_partition_of L1 ; :: thesis:
let A2, B2 be Subset of L2; :: thesis:
assume A2: A2,B2 form_upper_lower_partition_of L2 ; :: thesis:
let f be Function of (subrelstr A1),(subrelstr A2); :: thesis:
assume A3: f is isomorphic ; :: thesis:
let g be Function of (subrelstr B1),(subrelstr B2); :: thesis:
assume A4: g is isomorphic ; :: thesis:
A5: ( A1 \/ B1 = the carrier of L1 & ( for a, b being Element of L1 st a in A1 & b in B1 holds
a < b ) ) by A1, Def3;
A6: A1 misses B1 by A1, Th2;
A7: A2 misses B2 by A2, Th2;
A8: ( A2 \/ B2 = the carrier of L2 & ( for a, b being Element of L2 st a in A2 & b in B2 holds
a < b ) ) by A2, Def3;
set h = f +* g;

per cases ;

suppose A9: the carrier of L1 = {} ; :: thesis:

then A10: ( A1 = {} & B1 = {} ) by A5;
then A11: the carrier of (subrelstr A1) = {} by YELLOW_0:def 15;
then dom f = the carrier of (subrelstr A1) by FUNCT_2:def 1;
then A12: dom f = A1 by YELLOW_0:def 15;
A13: dom f = {} by A11, FUNCT_2:def 1;
( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A10, YELLOW_0:def 15;
then dom g = the carrier of (subrelstr B1) by FUNCT_2:def 1;
then A14: dom g = B1 by YELLOW_0:def 15;
A15: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
A16: dom (f +* g) = the carrier of L1 by A5, A12, A14, FUNCT_4:def 1;
A17: rng (f +* g) c= the carrier of L2

proof

rng (f +* g) = {} by A10, A13, A14, A15, RELAT_1:65;
hence rng (f +* g) c= the carrier of L2 by XBOOLE_1:2; :: thesis:

end;

A18: ( the carrier of (subrelstr A1) = {} & the carrier of (subrelstr B1) = {} ) by A10, YELLOW_0:def 15;
then subrelstr A1 is empty ;
then A19: subrelstr A2 is empty by A3, WAYBEL_0:def 38;
subrelstr B1 is empty by A18;
then A20: subrelstr B2 is empty by A4, WAYBEL_0:def 38;
for x being set st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2

proof

let x be set ; :: thesis:
assume x in the carrier of L1 ; :: thesis:
then (f +* g) . x in rng (f +* g) by A16, FUNCT_1:def 5;
hence (f +* g) . x in the carrier of L2 by A17; :: thesis:

end;

then reconsider h = f +* g as Function of L1,L2 by A16, FUNCT_2:5;
the carrier of (subrelstr A2) is empty by A19;
then A21: A2 = {} by YELLOW_0:def 15;
the carrier of (subrelstr B2) is empty by A20;
then B2 is empty by YELLOW_0:def 15;
then A22: L2 is empty by A8, A21;
L1 is empty by A9;
then h is isomorphic by A22, WAYBEL_0:def 38;
hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis:

end;

suppose A23: the carrier of L1 <> {} ; :: thesis:

then ( A1 <> {} or B1 <> {} ) by A5;
then ( not the carrier of (subrelstr A1) is empty or not the carrier of (subrelstr B1) is empty ) by YELLOW_0:def 15;
then ( not subrelstr A1 is empty or not subrelstr B1 is empty ) ;
then A24: ( not subrelstr A2 is empty or not subrelstr B2 is empty ) by A3, A4, WAYBEL_0:def 38;
then A25: ( not the carrier of (subrelstr A2) is empty or not the carrier of (subrelstr B2) is empty ) ;
then ( A2 <> {} or B2 <> {} ) by YELLOW_0:def 15;
then A26: A2 \/ B2 <> {} ;
( ( not A1 <> {} & not B1 <> {} ) or A2 <> {} or A1 = {} )

proof

assume ( A1 <> {} or B1 <> {} ) ; :: thesis:
( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by A3, Th4;
hence ( A2 <> {} or A1 = {} ) by YELLOW_0:def 15; :: thesis:

end;

then ( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by YELLOW_0:def 15;
then dom f = the carrier of (subrelstr A1) by FUNCT_2:def 1;
then A27: dom f = A1 by YELLOW_0:def 15;
( ( not A2 <> {} & not B2 <> {} ) or B2 <> {} or B1 = {} )

proof

assume ( A2 <> {} or B2 <> {} ) ; :: thesis:
( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A4, Th4;
hence ( B2 <> {} or B1 = {} ) by YELLOW_0:def 15; :: thesis:

end;

then A28: ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A24, YELLOW_0:def 15;
then A29: dom g = the carrier of (subrelstr B1) by FUNCT_2:def 1;
then A30: dom g = B1 by YELLOW_0:def 15;
A31: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
A32: ( dom f misses dom g implies rng (f +* g) = (rng f) \/ (rng g) )

proof

assume A33: dom f misses dom g ; :: thesis:
A34: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:18;
(rng f) \/ (rng g) c= rng (f +* g)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A35: x in (rng f) \/ (rng g) ; :: thesis:

per cases by A35, XBOOLE_0:def 3;

suppose x in rng f ; :: thesis:

then consider z being set such that
A36: ( z in dom f & x = f . z ) by FUNCT_1:def 5;
A37: z in dom (f +* g) by A31, A36, XBOOLE_0:def 3;
x = (f +* g) . z

proof

not z in dom g by A33, A36, XBOOLE_0:3;
hence x = (f +* g) . z by A36, FUNCT_4:12; :: thesis:

end;

hence x in rng (f +* g) by A37, FUNCT_1:def 5; :: thesis:

end;

suppose x in rng g ; :: thesis:

then consider z being set such that
A38: ( z in dom g & x = g . z ) by FUNCT_1:def 5;
A39: z in dom (f +* g) by A31, A38, XBOOLE_0:def 3;
(f +* g) . z = g . z by A38, FUNCT_4:14;
hence x in rng (f +* g) by A38, A39, FUNCT_1:def 5; :: thesis:

end;

hence rng (f +* g) = (rng f) \/ (rng g) by A34, XBOOLE_0:def 10; :: thesis:

end;

A40: rng (f +* g) = the carrier of L2

proof

per cases ;

suppose A41: ( A2 = {} & A1 = {} ) ; :: thesis:

then the carrier of (subrelstr B1) <> {} by A5, A23, YELLOW_0:def 15;
then A42: ( not subrelstr B2 is empty & not subrelstr B1 is empty ) by A25, A41, YELLOW_0:def 15;
A43: rng f = {} by A27, A41, RELAT_1:65;
rng g = the carrier of (subrelstr B2) by A4, A42, WAYBEL_0:66;
hence rng (f +* g) = the carrier of L2 by A8, A27, A32, A41, A43, XBOOLE_1:65, YELLOW_0:def 15; :: thesis:

end;

suppose ( A2 = {} & A1 <> {} ) ; :: thesis:

then ( the carrier of (subrelstr A2) = {} & the carrier of (subrelstr A1) <> {} ) by YELLOW_0:def 15;
hence rng (f +* g) = the carrier of L2 by A3, Th4; :: thesis:

end;

suppose ( A2 <> {} & A1 = {} ) ; :: thesis:

then ( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr A1) = {} ) by YELLOW_0:def 15;
hence rng (f +* g) = the carrier of L2 by A3, Th4; :: thesis:

end;

suppose A44: ( A2 <> {} & A1 <> {} ) ; :: thesis:

rng (f +* g) = the carrier of L2

proof

per cases ;

suppose A45: B2 <> {} ; :: thesis:

( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr A1) <> {} ) by A44, YELLOW_0:def 15;
then ( not subrelstr A2 is empty & not subrelstr A1 is empty ) ;
then rng f = the carrier of (subrelstr A2) by A3, WAYBEL_0:66;
then A46: rng f = A2 by YELLOW_0:def 15;
A47: the carrier of (subrelstr B2) <> {} by A45, YELLOW_0:def 15;
then the carrier of (subrelstr B1) <> {} by A4, Th4;
then ( not subrelstr B2 is empty & not subrelstr B1 is empty ) by A47;
then rng g = the carrier of (subrelstr B2) by A4, WAYBEL_0:66;
hence rng (f +* g) = the carrier of L2 by A1, A8, A27, A30, A32, A46, Th2, YELLOW_0:def 15; :: thesis:

end;

suppose A48: B2 = {} ; :: thesis:

then dom g = {} by A28, FUNCT_2:def 1, YELLOW_0:def 15;
then for x, y being set holds not [x,y] in g by RELAT_1:20;
then A49: g = {} by RELAT_1:56;
( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr A1) <> {} ) by A44, YELLOW_0:def 15;
then ( not subrelstr A2 is empty & not subrelstr A1 is empty ) ;
then rng f = the carrier of (subrelstr A2) by A3, WAYBEL_0:66;
hence rng (f +* g) = the carrier of L2 by A8, A32, A48, A49, RELAT_1:60, XBOOLE_1:65, YELLOW_0:def 15; :: thesis:

end;

hence rng (f +* g) = the carrier of L2 ; :: thesis:

end;

A50: dom (f +* g) = the carrier of L1 by A5, A27, A29, A31, YELLOW_0:def 15;
then A51: for x being set st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by A40, FUNCT_1:def 5;
reconsider L1 = L1 as non empty RelStr by A23;
reconsider L2 = L2 as non empty RelStr by A8, A26;
reconsider h = f +* g as Function of L1,L2 by A50, A51, FUNCT_2:5;
A52: h is one-to-one

proof

let x1, x2 be Element of L1; :: according to WAYBEL_1:def 1 :: thesis:
assume A53: h . x1 = h . x2 ; :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose A54: ( x1 in A1 & x2 in A1 ) ; :: thesis:

then A55: the carrier of (subrelstr A1) <> {} ;
then the carrier of (subrelstr A2) <> {} by A3, Th4;
then A56: ( not subrelstr A1 is empty & not subrelstr A2 is empty ) by A55;
not x1 in B1 by A6, A54, XBOOLE_0:3;
then A57: h . x1 = f . x1 by A30, FUNCT_4:12;
not x2 in B1 by A6, A54, XBOOLE_0:3;
then A58: f . x1 = f . x2 by A30, A53, A57, FUNCT_4:12;
f is one-to-one by A3, A56;
hence x1 = x2 by A27, A54, A58, FUNCT_1:def 8; :: thesis:

end;

suppose A59: ( x1 in A1 & x2 in B1 ) ; :: thesis:

then not x1 in B1 by A6, XBOOLE_0:3;
then h . x2 = f . x1 by A30, A53, FUNCT_4:12;
then A60: h . x2 in rng f by A27, A59, FUNCT_1:def 5;
A61: the carrier of (subrelstr A1) <> {} by A59;
then the carrier of (subrelstr A2) <> {} by A3, Th4;
then ( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A61;
then rng f = the carrier of (subrelstr A2) by A3, WAYBEL_0:66;
then A62: rng f = A2 by YELLOW_0:def 15;
A63: rng f misses rng g

proof

A64: the carrier of (subrelstr B1) <> {} by A59;
then the carrier of (subrelstr B2) <> {} by A4, Th4;
then ( not subrelstr B2 is empty & not subrelstr B1 is empty ) by A64;
then rng g = the carrier of (subrelstr B2) by A4, WAYBEL_0:66;
hence rng f misses rng g by A7, A62, YELLOW_0:def 15; :: thesis:

end;

h . x2 = g . x2 by A30, A59, FUNCT_4:14;
then h . x2 in rng g by A30, A59, FUNCT_1:def 5;
hence x1 = x2 by A60, A63, XBOOLE_0:3; :: thesis:

end;

suppose A65: ( x1 in B1 & x2 in A1 ) ; :: thesis:

then h . x2 = g . x1 by A30, A53, FUNCT_4:14;
then A66: h . x2 in rng g by A30, A65, FUNCT_1:def 5;
A67: the carrier of (subrelstr A1) <> {} by A65;
then the carrier of (subrelstr A2) <> {} by A3, Th4;
then ( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A67;
then A68: rng f = the carrier of (subrelstr A2) by A3, WAYBEL_0:66
.= A2 by YELLOW_0:def 15 ;
A69: the carrier of (subrelstr B1) <> {} by A65;
then the carrier of (subrelstr B2) <> {} by A4, Th4;
then ( not subrelstr B2 is empty & not subrelstr B1 is empty ) by A69;
then rng g = the carrier of (subrelstr B2) by A4, WAYBEL_0:66;
then A70: rng f misses rng g by A7, A68, YELLOW_0:def 15;
not x2 in dom g by A6, A30, A65, XBOOLE_0:3;
then h . x2 = f . x2 by FUNCT_4:12;
then h . x2 in rng f by A27, A65, FUNCT_1:def 5;
hence x1 = x2 by A66, A70, XBOOLE_0:3; :: thesis:

end;

suppose A71: ( x1 in B1 & x2 in B1 ) ; :: thesis:

then the carrier of (subrelstr B1) <> {} ;
then ( the carrier of (subrelstr B1) <> {} & the carrier of (subrelstr B2) <> {} ) by A4, Th4;
then A72: ( not subrelstr B1 is empty & not subrelstr B2 is empty ) ;
h . x1 = g . x1 by A30, A71, FUNCT_4:14;
then A73: g . x1 = g . x2 by A30, A53, A71, FUNCT_4:14;
g is one-to-one by A4, A72;
hence x1 = x2 by A30, A71, A73, FUNCT_1:def 8; :: thesis:

end;

h is isomorphic

proof

for x, y being Element of L1 holds
( x <= y iff h . x <= h . y )

proof

let x, y be Element of L1; :: thesis:
A74: dom f misses dom g by A6, A27, A29, YELLOW_0:def 15;

per cases by A5, XBOOLE_0:def 3;

suppose A75: ( x in A1 & y in A1 ) ; :: thesis:

then A76: the carrier of (subrelstr A1) <> {} ;
reconsider A1' = A1 as non empty Subset of L1 by A75;
the carrier of (subrelstr A2) <> {} by A3, A76, Th4;
then reconsider A2' = A2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider ax = x, ay = y as Element of (subrelstr A1') by A75, YELLOW_0:def 15;
reconsider f' = f as Function of (subrelstr A1'),(subrelstr A2') ;
A77: h . x = f . x by A1, A27, A30, A75, Th2, FUNCT_4:17;
A78: h . y = f . y by A1, A27, A30, A75, Th2, FUNCT_4:17;

hereby :: thesis:

assume x <= y ; :: thesis:
then ax <= ay by YELLOW_0:61;
then f' . ax <= f' . ay by A3, WAYBEL_0:66;
hence h . x <= h . y by A77, A78, YELLOW_0:60; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
then f' . ax <= f' . ay by A77, A78, YELLOW_0:61;
then ax <= ay by A3, WAYBEL_0:66;
hence x <= y by YELLOW_0:60; :: thesis:

end;

suppose A79: ( x in A1 & y in B1 ) ; :: thesis:

then A80: x < y by A1, Def3;

hereby :: thesis:

assume x <= y ; :: thesis:
A81: f . x = h . x by A27, A74, A79, FUNCT_4:17;
A82: g . y = h . y by A30, A79, FUNCT_4:14;
the carrier of (subrelstr A1) <> {} by A79;
then A83: the carrier of (subrelstr A2) <> {} by A3, Th4;
the carrier of (subrelstr B1) <> {} by A79;
then A84: the carrier of (subrelstr B2) <> {} by A4, Th4;
reconsider A1' = A1, B1' = B1 as non empty Subset of L1 by A79;
reconsider A2' = A2, B2' = B2 as non empty Subset of L2 by A83, A84, YELLOW_0:def 15;
reconsider ax = x as Element of (subrelstr A1') by A79, YELLOW_0:def 15;
reconsider ay = y as Element of (subrelstr B1') by A79, YELLOW_0:def 15;
reconsider f' = f as Function of (subrelstr A1'),(subrelstr A2') ;
reconsider g' = g as Function of (subrelstr B1'),(subrelstr B2') ;
( f' . ax in the carrier of (subrelstr A2') & g' . ay in the carrier of (subrelstr B2') ) ;
then ( f' . ax in A2' & g' . ay in B2' ) by YELLOW_0:def 15;
then h . x < h . y by A2, A81, A82, Def3;
hence h . x <= h . y by ORDERS_2:def 10; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
thus x <= y by A80, ORDERS_2:def 10; :: thesis:

end;

suppose A85: ( x in B1 & y in A1 ) ; :: thesis:

then y < x by A1, Def3;
hence ( x <= y implies h . x <= h . y ) by ORDERS_2:30; :: thesis:
assume A86: h . x <= h . y ; :: thesis:
A87: ( g . x in rng g & f . y in rng f ) by A27, A30, A85, FUNCT_1:def 5;
A88: ( not the carrier of (subrelstr A1) is empty & not the carrier of (subrelstr B1) is empty ) by A85;
then A89: ( not subrelstr A1 is empty & not subrelstr B1 is empty ) ;
( not the carrier of (subrelstr A2) is empty & not the carrier of (subrelstr B2) is empty ) by A3, A4, A88, Th4;
then ( not subrelstr A2 is empty & not subrelstr B2 is empty ) ;
then ( rng f = the carrier of (subrelstr A2) & rng g = the carrier of (subrelstr B2) ) by A3, A4, A89, WAYBEL_0:66;
then A90: ( g . x in B2 & f . y in A2 ) by A87, YELLOW_0:def 15;
( g . x = h . x & f . y = h . y ) by A6, A27, A30, A85, FUNCT_4:14, FUNCT_4:17;
then h . x > h . y by A2, A90, Def3;
hence x <= y by A86, ORDERS_2:30; :: thesis:

end;

suppose A91: ( x in B1 & y in B1 ) ; :: thesis:

then the carrier of (subrelstr B1) <> {} ;
then A92: the carrier of (subrelstr B2) <> {} by A4, Th4;
reconsider B1' = B1 as non empty Subset of L1 by A91;
reconsider B2' = B2 as non empty Subset of L2 by A92, YELLOW_0:def 15;
reconsider ax = x, ay = y as Element of (subrelstr B1') by A91, YELLOW_0:def 15;
reconsider g' = g as Function of (subrelstr B1'),(subrelstr B2') ;
A93: h . x = g . x by A30, A91, FUNCT_4:14;
A94: h . y = g . y by A30, A91, FUNCT_4:14;

hereby :: thesis:

assume x <= y ; :: thesis:
then ax <= ay by YELLOW_0:61;
then g' . ax <= g' . ay by A4, WAYBEL_0:66;
hence h . x <= h . y by A93, A94, YELLOW_0:60; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
then g' . ax <= g' . ay by A93, A94, YELLOW_0:61;
then ax <= ay by A4, WAYBEL_0:66;
hence x <= y by YELLOW_0:60; :: thesis:

end;

hence h is isomorphic by A40, A52, WAYBEL_0:66; :: thesis:

end;

hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis:

end;