let L1, L2 be complete LATTICE; :: thesis: for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let T1 be Scott TopAugmentation of L1; :: thesis: for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let T2 be Scott TopAugmentation of L2; :: thesis: for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let h be Function of L1,L2; :: thesis: for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let H be Function of T1,T2; :: thesis: ( h = H & h is isomorphic implies H is being_homeomorphism )
assume that
A1: h = H and
A2: h is isomorphic ; :: thesis: H is being_homeomorphism
A3: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of T1,the InternalRel of T1 #) by YELLOW_9:def 4;
A4: RelStr(# the carrier of L2,the InternalRel of L2 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) by YELLOW_9:def 4;
A5: h is one-to-one by A2;
A6: rng h = [#] L2 by A2, WAYBEL_0:66;
consider g being Function of L2,L1 such that
A7: g = h " ;
g = h " by A5, A6, A7, TOPS_2:def 4;
then A8: g is isomorphic by A2, WAYBEL_0:68;
reconsider h1 = h as sups-preserving Function of L1,L2 by A2, WAYBEL13:20;
reconsider h2 = h " as sups-preserving Function of L2,L1 by A7, A8, WAYBEL13:20;
A9: h1 is directed-sups-preserving ;
A10: h2 is directed-sups-preserving ;
reconsider H' = h " as Function of T2,T1 by A3, A4;
H is directed-sups-preserving by A1, A3, A4, A9, WAYBEL21:6;
then A11: H is continuous ;
H' is directed-sups-preserving by A3, A4, A10, WAYBEL21:6;
then A12: H' is continuous ;
A13: dom H = [#] T1 by FUNCT_2:def 1;
A14: rng H = [#] T2 by A1, A2, A4, WAYBEL_0:66;
A15: H is one-to-one by A1, A2;
A16: dom (H " ) = the carrier of T2 by FUNCT_2:def 1
.= dom H' by FUNCT_2:def 1 ;
for x being set st x in dom H' holds
H' . x = (H " ) . x

proof

let x be set ; :: thesis: ( x in dom H' implies H' . x = (H " ) . x )
assume x in dom H' ; :: thesis: H' . x = (H " ) . x
thus H' . x = (h " ) . x by A5, A6, TOPS_2:def 4
.= (H " ) . x by A1, A5, A14, TOPS_2:def 4 ; :: thesis: verum

end;

then H " = H' by A16, FUNCT_1:9;
hence H is being_homeomorphism by A11, A12, A13, A14, A15, TOPS_2:def 5; :: thesis: verum