let L1, L2 be antisymmetric RelStr ; :: thesis: for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds
for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (),() st f is isomorphic holds
for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

let A1, B1 be Subset of L1; :: thesis: ( A1,B1 form_upper_lower_partition_of L1 implies for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (),() st f is isomorphic holds
for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )

assume A1: A1,B1 form_upper_lower_partition_of L1 ; :: thesis: for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (),() st f is isomorphic holds
for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

A2: A1 \/ B1 = the carrier of L1 by A1;
let A2, B2 be Subset of L2; :: thesis: ( A2,B2 form_upper_lower_partition_of L2 implies for f being Function of (),() st f is isomorphic holds
for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )

assume A3: A2,B2 form_upper_lower_partition_of L2 ; :: thesis: for f being Function of (),() st f is isomorphic holds
for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

A4: A2 misses B2 by ;
A5: A2 \/ B2 = the carrier of L2 by A3;
A6: A1 misses B1 by ;
let f be Function of (),(); :: thesis: ( f is isomorphic implies for g being Function of (),() st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )

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

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

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

set h = f +* g;
per cases ( the carrier of L1 = {} or the carrier of L1 <> {} ) ;
suppose A9: the carrier of L1 = {} ; :: thesis: ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

then A10: A1 = {} by A2;
then the carrier of () = {} by YELLOW_0:def 15;
then dom f = the carrier of () ;
then A11: dom f = A1 by YELLOW_0:def 15;
subrelstr A1 is empty by ;
then subrelstr A2 is empty by ;
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 () <> {} or the carrier of () = {} ) by YELLOW_0:def 15;
then dom g = the carrier of () by FUNCT_2:def 1;
then dom g = B1 by YELLOW_0:def 15;
then dom (f +* g) = the carrier of L1 by ;
then reconsider h = f +* g as Function of L1,L2 by ;
A15: L1 is empty by A9;
subrelstr B1 is empty by ;
then L2 is empty by ;
then h is isomorphic by ;
hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis: verum
end;
suppose A16: the carrier of L1 <> {} ; :: thesis: ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )

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 ;
( ( not A2 <> {} & not B2 <> {} ) or B2 <> {} or B1 = {} )
proof
assume ( A2 <> {} or B2 <> {} ) ; :: thesis: ( B2 <> {} or B1 = {} )
( the carrier of () <> {} or the carrier of () = {} ) by ;
hence ( B2 <> {} or B1 = {} ) by YELLOW_0:def 15; :: thesis: verum
end;
then A18: ( the carrier of () <> {} or the carrier of () = {} ) by ;
then A19: dom g = the carrier of () 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: ( A2 <> {} or A1 = {} )
( the carrier of () <> {} or the carrier of () = {} ) by ;
hence ( A2 <> {} or A1 = {} ) by YELLOW_0:def 15; :: thesis: verum
end;
then ( the carrier of () <> {} or the carrier of () = {} ) by YELLOW_0:def 15;
then dom f = the carrier of () 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: rng (f +* g) = (rng f) \/ (rng g)
A25: (rng f) \/ (rng g) c= rng (f +* g)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )
assume A26: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f +* g)
per cases ( x in rng f or x in rng g ) by ;
suppose x in rng f ; :: thesis: x in rng (f +* g)
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 ;
then A29: x = (f +* g) . z by ;
z in dom (f +* g) by ;
hence x in rng (f +* g) by ; :: thesis: verum
end;
suppose x in rng g ; :: thesis: x in rng (f +* g)
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 ;
hence x in rng (f +* g) by ; :: thesis: verum
end;
end;
end;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence rng (f +* g) = (rng f) \/ (rng g) by ; :: thesis: verum
end;
A32: rng (f +* g) = the carrier of L2
proof
per cases ( ( A2 = {} & A1 = {} ) or ( A2 = {} & A1 <> {} ) or ( A2 <> {} & A1 = {} ) or ( A2 <> {} & A1 <> {} ) ) ;
suppose A33: ( A2 = {} & A1 = {} ) ; :: thesis: rng (f +* g) = the carrier of L2
then not subrelstr B1 is empty by ;
then A34: rng g = the carrier of () by ;
rng f = {} by ;
hence rng (f +* g) = the carrier of L2 by ; :: thesis: verum
end;
suppose ( A2 = {} & A1 <> {} ) ; :: thesis: rng (f +* g) = the carrier of L2
then ( the carrier of () = {} & the carrier of () <> {} ) by YELLOW_0:def 15;
hence rng (f +* g) = the carrier of L2 by ; :: thesis: verum
end;
suppose ( A2 <> {} & A1 = {} ) ; :: thesis: rng (f +* g) = the carrier of L2
then ( the carrier of () <> {} & the carrier of () = {} ) by YELLOW_0:def 15;
hence rng (f +* g) = the carrier of L2 by ; :: thesis: verum
end;
suppose A35: ( A2 <> {} & A1 <> {} ) ; :: thesis: rng (f +* g) = the carrier of L2
rng (f +* g) = the carrier of L2
proof
per cases ( B2 <> {} or B2 = {} ) ;
suppose A36: B2 <> {} ; :: thesis: rng (f +* g) = the carrier of L2
then the carrier of () <> {} by YELLOW_0:def 15;
then the carrier of () <> {} by ;
then A37: not subrelstr B1 is empty ;
( not subrelstr A2 is empty & not subrelstr A1 is empty ) by ;
then rng f = the carrier of () by ;
then A38: rng f = A2 by YELLOW_0:def 15;
not subrelstr B2 is empty by ;
then rng g = the carrier of () by ;
hence rng (f +* g) = the carrier of L2 by ; :: thesis: verum
end;
suppose A39: B2 = {} ; :: thesis: rng (f +* g) = the carrier of L2
( not subrelstr A2 is empty & not subrelstr A1 is empty ) by ;
then A40: rng f = the carrier of () by ;
g = {} by ;
hence rng (f +* g) = the carrier of L2 by ; :: thesis: verum
end;
end;
end;
hence rng (f +* g) = the carrier of L2 ; :: thesis: verum
end;
end;
end;
A41: dom (f +* g) = the carrier of L1 by ;
then A42: for x being object st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by ;
( A2 <> {} or B2 <> {} ) by ;
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 ;
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: ( x <= y iff h . x <= h . y )
A44: dom f misses dom g by ;
per cases ( ( x in A1 & y in A1 ) or ( x in A1 & y in B1 ) or ( x in B1 & y in A1 ) or ( x in B1 & y in B1 ) ) by ;
suppose A45: ( x in A1 & y in A1 ) ; :: thesis: ( x <= y iff h . x <= h . y )
then the carrier of () <> {} by ;
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 ;
reconsider f9 = f as Function of (subrelstr A19),(subrelstr A29) ;
A46: ( h . x = f . x & h . y = f . y ) by ;
hereby :: thesis: ( h . x <= h . y implies x <= y )
assume x <= y ; :: thesis: h . x <= h . y
then ax <= ay by YELLOW_0:60;
then f9 . ax <= f9 . ay by ;
hence h . x <= h . y by ; :: thesis: verum
end;
assume h . x <= h . y ; :: thesis: x <= y
then f9 . ax <= f9 . ay by ;
then ax <= ay by ;
hence x <= y by YELLOW_0:59; :: thesis: verum
end;
suppose A47: ( x in A1 & y in B1 ) ; :: thesis: ( x <= y iff h . x <= h . y )
hereby :: thesis: ( h . x <= h . y implies x <= y )
( the carrier of () <> {} & the carrier of () <> {} ) 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: h . x <= h . y
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 ;
reconsider ay = y as Element of (subrelstr B19) by ;
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 ;
then h . x < h . y by A3, A48, A49;
hence h . x <= h . y by ORDERS_2:def 6; :: thesis: verum
end;
assume h . x <= h . y ; :: thesis: x <= y
x < y by ;
hence x <= y by ORDERS_2:def 6; :: thesis: verum
end;
suppose A50: ( x in B1 & y in A1 ) ; :: thesis: ( x <= y iff h . x <= h . y )
then not the carrier of () is empty by ;
then not subrelstr B2 is empty ;
then A51: rng g = the carrier of () by ;
g . x in rng g by ;
then A52: g . x in B2 by ;
not the carrier of () is empty by A7, A50, Th4;
then not subrelstr A2 is empty ;
then A53: rng f = the carrier of () by ;
f . y in rng f by ;
then A54: f . y in A2 by ;
y < x by ;
hence ( x <= y implies h . x <= h . y ) by ORDERS_2:6; :: thesis: ( h . x <= h . y implies x <= y )
assume A55: h . x <= h . y ; :: thesis: x <= y
( g . x = h . x & f . y = h . y ) by ;
then h . x > h . y by A3, A52, A54;
hence x <= y by ; :: thesis: verum
end;
suppose A56: ( x in B1 & y in B1 ) ; :: thesis: ( x <= y iff h . x <= h . y )
then the carrier of () <> {} by ;
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 ;
reconsider g9 = g as Function of (subrelstr B19),(subrelstr B29) ;
A57: ( h . x = g . x & h . y = g . y ) by ;
hereby :: thesis: ( h . x <= h . y implies x <= y )
assume x <= y ; :: thesis: h . x <= h . y
then ax <= ay by YELLOW_0:60;
then g9 . ax <= g9 . ay by ;
hence h . x <= h . y by ; :: thesis: verum
end;
assume h . x <= h . y ; :: thesis: x <= y
then g9 . ax <= g9 . ay by ;
then ax <= ay by ;
hence x <= y by YELLOW_0:59; :: thesis: verum
end;
end;
end;
h is V13()
proof
let x1, x2 be Element of L1; :: according to WAYBEL_1:def 1 :: thesis: ( not h . x1 = h . x2 or x1 = x2 )
assume A58: h . x1 = h . x2 ; :: thesis: x1 = x2
per cases ( ( x1 in A1 & x2 in A1 ) or ( x1 in A1 & x2 in B1 ) or ( x1 in B1 & x2 in A1 ) or ( x1 in B1 & x2 in B1 ) ) by ;
suppose A59: ( x1 in A1 & x2 in A1 ) ; :: thesis: x1 = x2
then not x1 in B1 by ;
then A60: h . x1 = f . x1 by ;
the carrier of () <> {} by A7, A59, Th4;
then A61: not subrelstr A2 is empty ;
not x2 in B1 by ;
then f . x1 = f . x2 by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A62: ( x1 in A1 & x2 in B1 ) ; :: thesis: x1 = x2
then the carrier of () <> {} by ;
then not subrelstr A2 is empty ;
then rng f = the carrier of () by ;
then A63: rng f = A2 by YELLOW_0:def 15;
not x1 in B1 by ;
then h . x2 = f . x1 by ;
then A64: h . x2 in rng f by ;
h . x2 = g . x2 by ;
then A65: h . x2 in rng g by ;
the carrier of () <> {} by A8, A62, Th4;
then not subrelstr B2 is empty ;
then rng g = the carrier of () by ;
then rng f misses rng g by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A66: ( x1 in B1 & x2 in A1 ) ; :: thesis: x1 = x2
then not x2 in dom g by ;
then h . x2 = f . x2 by FUNCT_4:11;
then A67: h . x2 in rng f by ;
the carrier of () <> {} by A8, A66, Th4;
then not subrelstr B2 is empty ;
then A68: rng g = the carrier of () by ;
h . x2 = g . x1 by ;
then A69: h . x2 in rng g by ;
the carrier of () <> {} by A7, A66, Th4;
then not subrelstr A2 is empty ;
then rng f = the carrier of () by
.= A2 by YELLOW_0:def 15 ;
then rng f misses rng g by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A70: ( x1 in B1 & x2 in B1 ) ; :: thesis: x1 = x2
then the carrier of () <> {} by ;
then A71: not subrelstr B2 is empty ;
h . x1 = g . x1 by ;
then g . x1 = g . x2 by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
then h is isomorphic by ;
hence ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; :: thesis: verum
end;
end;