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:
A2: A1 \/ B1 = the carrier of L1 by A1;
let A2, B2 be Subset of L2; :: thesis:
assume A3: A2,B2 form_upper_lower_partition_of L2 ; :: thesis:
A4: A2 misses B2 by A3, Th2;
A5: A2 \/ B2 = the carrier of L2 by A3;
A6: A1 misses B1 by A1, Th2;
let f be Function of (subrelstr A1),(subrelstr A2); :: thesis:
assume A7: f is isomorphic ; :: thesis:
let g be Function of (subrelstr B1),(subrelstr B2); :: thesis:
assume A8: g is isomorphic ; :: thesis:
set h = f +* g;

per cases ;

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

then A10: A1 = {} by A2;
then the carrier of (subrelstr A1) = {} by YELLOW_0:def 15;
then dom f = the carrier of (subrelstr A1) ;
then A11: dom f = A1 by YELLOW_0:def 15;
subrelstr A1 is empty by A10, YELLOW_0:def 15;
then subrelstr A2 is empty by A7, WAYBEL_0:def 38;
then A12: A2 = {} by YELLOW_0:def 15;
A13: for x being object st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by A9;
A14: B1 = {} by A2, A9;
then ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by YELLOW_0:def 15;
then dom g = the carrier of (subrelstr B1) by FUNCT_2:def 1;
then dom g = B1 by YELLOW_0:def 15;
then dom (f +* g) = the carrier of L1 by A2, A11, FUNCT_4:def 1;
then reconsider h = f +* g as Function of L1,L2 by A13, FUNCT_2:3;
A15: L1 is empty by A9;
subrelstr B1 is empty by A14, YELLOW_0:def 15;
then L2 is empty by A8, A5, A12, WAYBEL_0:def 38;
then h is isomorphic by A15, WAYBEL_0:def 38;
hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis:

end;

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

then ( A1 <> {} or B1 <> {} ) by A2;
then ( not subrelstr A1 is empty or not subrelstr B1 is empty ) by YELLOW_0:def 15;
then A17: ( not subrelstr A2 is empty or not subrelstr B2 is empty ) by A7, A8, WAYBEL_0:def 38;
( ( 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 A8, Th4;
hence ( B2 <> {} or B1 = {} ) by YELLOW_0:def 15; :: thesis:

end;

then A18: ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A17, YELLOW_0:def 15;
then A19: dom g = the carrier of (subrelstr B1) by FUNCT_2:def 1;
then A20: dom g = B1 by YELLOW_0:def 15;
( ( 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 A7, 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 A21: dom f = A1 by YELLOW_0:def 15;
A22: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
A23: ( dom f misses dom g implies rng (f +* g) = (rng f) \/ (rng g) )

proof

assume A24: dom f misses dom g ; :: thesis:
A25: (rng f) \/ (rng g) c= rng (f +* g)

proof

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

per cases by A26, XBOOLE_0:def 3;

suppose x in rng f ; :: thesis:

then consider z being object such that
A27: z in dom f and
A28: x = f . z by FUNCT_1:def 3;
not z in dom g by A24, A27, XBOOLE_0:3;
then A29: x = (f +* g) . z by A28, FUNCT_4:11;
z in dom (f +* g) by A22, A27, XBOOLE_0:def 3;
hence x in rng (f +* g) by A29, FUNCT_1:def 3; :: thesis:

end;

suppose x in rng g ; :: thesis:

then consider z being object such that
A30: z in dom g and
A31: x = g . z by FUNCT_1:def 3;
( z in dom (f +* g) & (f +* g) . z = g . z ) by A22, A30, FUNCT_4:13, XBOOLE_0:def 3;
hence x in rng (f +* g) by A31, FUNCT_1:def 3; :: thesis:

end;

rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence rng (f +* g) = (rng f) \/ (rng g) by A25, XBOOLE_0:def 10; :: thesis:

end;

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

proof

per cases ;

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

then not subrelstr B1 is empty by A2, A16, YELLOW_0:def 15;
then A34: rng g = the carrier of (subrelstr B2) by A8, A17, A33, WAYBEL_0:66, YELLOW_0:def 15;
rng f = {} by A21, A33, RELAT_1:42;
hence rng (f +* g) = the carrier of L2 by A5, A21, A23, A33, A34, 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 A7, 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 A7, Th4; :: thesis:

end;

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

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

proof

per cases ;

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

then the carrier of (subrelstr B2) <> {} by YELLOW_0:def 15;
then the carrier of (subrelstr B1) <> {} by A8, Th4;
then A37: not subrelstr B1 is empty ;
( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A35, YELLOW_0:def 15;
then rng f = the carrier of (subrelstr A2) by A7, WAYBEL_0:66;
then A38: rng f = A2 by YELLOW_0:def 15;
not subrelstr B2 is empty by A36, YELLOW_0:def 15;
then rng g = the carrier of (subrelstr B2) by A8, A37, WAYBEL_0:66;
hence rng (f +* g) = the carrier of L2 by A1, A5, A21, A20, A23, A38, Th2, YELLOW_0:def 15; :: thesis:

end;

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

( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A35, YELLOW_0:def 15;
then A40: rng f = the carrier of (subrelstr A2) by A7, WAYBEL_0:66;
g = {} by A18, A39, YELLOW_0:def 15;
hence rng (f +* g) = the carrier of L2 by A5, A23, A39, A40, RELAT_1:38, XBOOLE_1:65, YELLOW_0:def 15; :: thesis:

end;

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

end;

A41: dom (f +* g) = the carrier of L1 by A2, A21, A19, A22, YELLOW_0:def 15;
then A42: for x being object st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by A32, FUNCT_1:def 3;
( A2 <> {} or B2 <> {} ) by A17, YELLOW_0:def 15;
then reconsider L2 = L2 as non empty RelStr by A5;
reconsider L1 = L1 as non empty RelStr by A16;
reconsider h = f +* g as Function of L1,L2 by A41, A42, FUNCT_2:3;
A43: for x, y being Element of L1 holds
( x <= y iff h . x <= h . y )

proof

let x, y be Element of L1; :: thesis:
A44: dom f misses dom g by A6, A21, A19, YELLOW_0:def 15;

per cases by A2, XBOOLE_0:def 3;

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

then the carrier of (subrelstr A2) <> {} by A7, Th4;
then reconsider A29 = A2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider A19 = A1 as non empty Subset of L1 by A45;
reconsider ax = x, ay = y as Element of (subrelstr A19) by A45, YELLOW_0:def 15;
reconsider f9 = f as Function of (subrelstr A19),(subrelstr A29) ;
A46: ( h . x = f . x & h . y = f . y ) by A1, A21, A20, A45, Th2, FUNCT_4:16;

hereby :: thesis:

assume x <= y ; :: thesis:
then ax <= ay by YELLOW_0:60;
then f9 . ax <= f9 . ay by A7, WAYBEL_0:66;
hence h . x <= h . y by A46, YELLOW_0:59; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
then f9 . ax <= f9 . ay by A46, YELLOW_0:60;
then ax <= ay by A7, WAYBEL_0:66;
hence x <= y by YELLOW_0:59; :: thesis:

end;

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

hereby :: thesis:

( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr B2) <> {} ) by A7, A8, A47, Th4;
then reconsider A29 = A2, B29 = B2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider A19 = A1, B19 = B1 as non empty Subset of L1 by A47;
assume x <= y ; :: thesis:
reconsider f9 = f as Function of (subrelstr A19),(subrelstr A29) ;
reconsider g9 = g as Function of (subrelstr B19),(subrelstr B29) ;
reconsider ax = x as Element of (subrelstr A19) by A47, YELLOW_0:def 15;
reconsider ay = y as Element of (subrelstr B19) by A47, YELLOW_0:def 15;
f9 . ax in the carrier of (subrelstr A29) ;
then A48: f9 . ax in A29 by YELLOW_0:def 15;
g9 . ay in the carrier of (subrelstr B29) ;
then A49: g9 . ay in B29 by YELLOW_0:def 15;
( f . x = h . x & g . y = h . y ) by A21, A20, A44, A47, FUNCT_4:13, FUNCT_4:16;
then h . x < h . y by A3, A48, A49;
hence h . x <= h . y by ORDERS_2:def 6; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
x < y by A1, A47;
hence x <= y by ORDERS_2:def 6; :: thesis:

end;

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

then not the carrier of (subrelstr B2) is empty by A8, Th4;
then not subrelstr B2 is empty ;
then A51: rng g = the carrier of (subrelstr B2) by A8, A50, WAYBEL_0:66;
g . x in rng g by A20, A50, FUNCT_1:def 3;
then A52: g . x in B2 by A51, YELLOW_0:def 15;
not the carrier of (subrelstr A2) is empty by A7, A50, Th4;
then not subrelstr A2 is empty ;
then A53: rng f = the carrier of (subrelstr A2) by A7, A50, WAYBEL_0:66;
f . y in rng f by A21, A50, FUNCT_1:def 3;
then A54: f . y in A2 by A53, YELLOW_0:def 15;
y < x by A1, A50;
hence ( x <= y implies h . x <= h . y ) by ORDERS_2:6; :: thesis:
assume A55: h . x <= h . y ; :: thesis:
( g . x = h . x & f . y = h . y ) by A1, A21, A20, A50, Th2, FUNCT_4:13, FUNCT_4:16;
then h . x > h . y by A3, A52, A54;
hence x <= y by A55, ORDERS_2:6; :: thesis:

end;

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

then the carrier of (subrelstr B2) <> {} by A8, Th4;
then reconsider B29 = B2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider B19 = B1 as non empty Subset of L1 by A56;
reconsider ax = x, ay = y as Element of (subrelstr B19) by A56, YELLOW_0:def 15;
reconsider g9 = g as Function of (subrelstr B19),(subrelstr B29) ;
A57: ( h . x = g . x & h . y = g . y ) by A20, A56, FUNCT_4:13;

hereby :: thesis:

assume x <= y ; :: thesis:
then ax <= ay by YELLOW_0:60;
then g9 . ax <= g9 . ay by A8, WAYBEL_0:66;
hence h . x <= h . y by A57, YELLOW_0:59; :: thesis:

end;

assume h . x <= h . y ; :: thesis:
then g9 . ax <= g9 . ay by A57, YELLOW_0:60;
then ax <= ay by A8, WAYBEL_0:66;
hence x <= y by YELLOW_0:59; :: thesis:

end;

h is V13()

proof

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

per cases by A2, XBOOLE_0:def 3;

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

then not x1 in B1 by A6, XBOOLE_0:3;
then A60: h . x1 = f . x1 by A20, FUNCT_4:11;
the carrier of (subrelstr A2) <> {} by A7, A59, Th4;
then A61: not subrelstr A2 is empty ;
not x2 in B1 by A6, A59, XBOOLE_0:3;
then f . x1 = f . x2 by A20, A58, A60, FUNCT_4:11;
hence x1 = x2 by A7, A21, A59, A61, FUNCT_1:def 4; :: thesis:

end;

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

then the carrier of (subrelstr A2) <> {} by A7, Th4;
then not subrelstr A2 is empty ;
then rng f = the carrier of (subrelstr A2) by A7, A62, WAYBEL_0:66;
then A63: rng f = A2 by YELLOW_0:def 15;
not x1 in B1 by A6, A62, XBOOLE_0:3;
then h . x2 = f . x1 by A20, A58, FUNCT_4:11;
then A64: h . x2 in rng f by A21, A62, FUNCT_1:def 3;
h . x2 = g . x2 by A20, A62, FUNCT_4:13;
then A65: h . x2 in rng g by A20, A62, FUNCT_1:def 3;
the carrier of (subrelstr B2) <> {} by A8, A62, Th4;
then not subrelstr B2 is empty ;
then rng g = the carrier of (subrelstr B2) by A8, A62, WAYBEL_0:66;
then rng f misses rng g by A4, A63, YELLOW_0:def 15;
hence x1 = x2 by A64, A65, XBOOLE_0:3; :: thesis:

end;

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

then not x2 in dom g by A6, A20, XBOOLE_0:3;
then h . x2 = f . x2 by FUNCT_4:11;
then A67: h . x2 in rng f by A21, A66, FUNCT_1:def 3;
the carrier of (subrelstr B2) <> {} by A8, A66, Th4;
then not subrelstr B2 is empty ;
then A68: rng g = the carrier of (subrelstr B2) by A8, A66, WAYBEL_0:66;
h . x2 = g . x1 by A20, A58, A66, FUNCT_4:13;
then A69: h . x2 in rng g by A20, A66, FUNCT_1:def 3;
the carrier of (subrelstr A2) <> {} by A7, A66, Th4;
then not subrelstr A2 is empty ;
then rng f = the carrier of (subrelstr A2) by A7, A66, WAYBEL_0:66
.= A2 by YELLOW_0:def 15 ;
then rng f misses rng g by A4, A68, YELLOW_0:def 15;
hence x1 = x2 by A69, A67, XBOOLE_0:3; :: thesis:

end;

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

then the carrier of (subrelstr B2) <> {} by A8, Th4;
then A71: not subrelstr B2 is empty ;
h . x1 = g . x1 by A20, A70, FUNCT_4:13;
then g . x1 = g . x2 by A20, A58, A70, FUNCT_4:13;
hence x1 = x2 by A8, A20, A70, A71, FUNCT_1:def 4; :: thesis:

end;

then h is isomorphic by A32, A43, WAYBEL_0:66;
hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis:

end;