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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

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: ( f is isomorphic implies for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

let g be Function of (subrelstr B1),(subrelstr B2); :: 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;

for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds

for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr A1),(subrelstr A2) st f is isomorphic holds

for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

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: ( f is isomorphic implies for g being Function of (subrelstr B1),(subrelstr B2) 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 (subrelstr B1),(subrelstr B2) st g is isomorphic holds

ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

let g be Function of (subrelstr B1),(subrelstr B2); :: 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 <> {} )
;

end;

suppose A9:
the carrier of L1 = {}
; :: thesis: ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

( h = f +* g & h is isomorphic )

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: verum

end;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: verum

suppose A16:
the carrier of L1 <> {}
; :: thesis: ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic )

( 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 A7, A8, WAYBEL_0:def 38;

( ( not A2 <> {} & not B2 <> {} ) or B2 <> {} or B1 = {} )

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 = {} )

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) )

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 )

hence ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic ) ; :: thesis: verum

end;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

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

( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A8, Th4;

hence ( B2 <> {} or B1 = {} ) by YELLOW_0:def 15; :: thesis: verum

end;( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A8, Th4;

hence ( B2 <> {} or B1 = {} ) by YELLOW_0:def 15; :: thesis: verum

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

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

( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by A7, Th4;

hence ( A2 <> {} or A1 = {} ) by YELLOW_0:def 15; :: thesis: verum

end;( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by A7, Th4;

hence ( A2 <> {} or A1 = {} ) by YELLOW_0:def 15; :: thesis: verum

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

A32:
rng (f +* g) = the carrier of L2
assume A24:
dom f misses dom g
; :: thesis: rng (f +* g) = (rng f) \/ (rng g)

A25: (rng f) \/ (rng g) c= rng (f +* g)

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

end;A25: (rng f) \/ (rng g) c= rng (f +* g)

proof

rng (f +* g) c= (rng f) \/ (rng g)
by FUNCT_4:17;
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)

end;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 A26, XBOOLE_0:def 3;

end;

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 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: verum

end;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: verum

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

proof
end;

A41:
dom (f +* g) = the carrier of L1
by A2, A21, A19, A22, YELLOW_0:def 15;per cases
( ( A2 = {} & A1 = {} ) or ( A2 = {} & A1 <> {} ) or ( A2 <> {} & A1 = {} ) or ( A2 <> {} & A1 <> {} ) )
;

end;

suppose A33:
( A2 = {} & A1 = {} )
; :: thesis: rng (f +* g) = the carrier of L2

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: verum

end;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: verum

suppose
( A2 = {} & A1 <> {} )
; :: thesis: rng (f +* g) = the carrier of L2

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: verum

end;hence rng (f +* g) = the carrier of L2 by A7, Th4; :: thesis: verum

suppose
( A2 <> {} & A1 = {} )
; :: thesis: rng (f +* g) = the carrier of L2

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: verum

end;hence rng (f +* g) = the carrier of L2 by A7, Th4; :: thesis: verum

suppose A35:
( A2 <> {} & A1 <> {} )
; :: thesis: rng (f +* g) = the carrier of L2

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

end;proof
end;

hence
rng (f +* g) = the carrier of L2
; :: thesis: verumper cases
( B2 <> {} or B2 = {} )
;

end;

suppose A36:
B2 <> {}
; :: thesis: rng (f +* g) = the carrier of L2

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: verum

end;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: verum

suppose A39:
B2 = {}
; :: thesis: rng (f +* g) = the carrier of L2

( 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: verum

end;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: verum

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

h is V13()
let x, y be Element of L1; :: thesis: ( x <= y iff h . x <= h . y )

A44: dom f misses dom g by A6, A21, A19, YELLOW_0:def 15;

end;A44: dom f misses dom g by A6, A21, A19, YELLOW_0:def 15;

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 A2, XBOOLE_0:def 3;

end;

suppose A45:
( x in A1 & y in A1 )
; :: thesis: ( x <= y iff h . x <= h . y )

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;

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: verum

end;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: ( h . x <= h . y implies x <= y )

assume
h . x <= h . y
; :: thesis: x <= yassume
x <= y
; :: thesis: h . x <= h . y

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: verum

end;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: verum

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: verum

suppose A47:
( x in A1 & y in B1 )
; :: thesis: ( x <= y iff h . x <= h . y )

x < y by A1, A47;

hence x <= y by ORDERS_2:def 6; :: thesis: verum

end;

hereby :: thesis: ( h . x <= h . y implies x <= y )

assume
h . x <= h . y
; :: thesis: x <= y
( 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: 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 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: verum

end;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 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: verum

x < y by A1, A47;

hence x <= y by ORDERS_2:def 6; :: thesis: verum

suppose A50:
( x in B1 & y in A1 )
; :: thesis: ( x <= y iff h . x <= h . y )

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: ( 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 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: verum

end;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: ( 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 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: verum

suppose A56:
( x in B1 & y in B1 )
; :: thesis: ( x <= y iff h . x <= h . y )

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;

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: verum

end;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: ( h . x <= h . y implies x <= y )

assume
h . x <= h . y
; :: thesis: x <= yassume
x <= y
; :: thesis: h . x <= h . y

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: verum

end;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: verum

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: verum

proof

then
h is isomorphic
by A32, A43, WAYBEL_0:66;
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

end;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 A2, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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

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: verum

end;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: verum

hence ex h being Function of L1,L2 st

( h = f +* g & h is isomorphic ) ; :: thesis: verum