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 L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by YELLOW_9:def 4;
A4: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by YELLOW_9:def 4;
then reconsider H9 = h " as Function of T2,T1 by A3;
consider g being Function of L2,L1 such that
A5: g = h " ;
g = h " by A2, A5, TOPS_2:def 4;
then g is isomorphic by A2, WAYBEL_0:68;
then reconsider h2 = h " as sups-preserving Function of L2,L1 by A5, WAYBEL13:20;
A6: rng H = [#] T2 by A1, A2, A3, WAYBEL_0:66;
A7: for x being object st x in dom H9 holds
H9 . x = (H ") . x

proof

let x be object ; :: thesis: ( x in dom H9 implies H9 . x = (H ") . x )
assume x in dom H9 ; :: thesis: H9 . x = (H ") . x
A8: H is onto by A6, FUNCT_2:def 3;
thus H9 . x = (h ") . x by A2, TOPS_2:def 4
.= (H ") . x by A1, A2, A8, TOPS_2:def 4 ; :: thesis: verum

end;

h2 is directed-sups-preserving ;
then A9: H9 is directed-sups-preserving by A4, A3, WAYBEL21:6;
dom (H ") = the carrier of T2 by FUNCT_2:def 1
.= dom H9 by FUNCT_2:def 1 ;
then A10: H " = H9 by A7, FUNCT_1:2;
reconsider h1 = h as sups-preserving Function of L1,L2 by A2, WAYBEL13:20;
h1 is directed-sups-preserving ;
then A11: H is directed-sups-preserving by A1, A4, A3, WAYBEL21:6;
dom H = [#] T1 by FUNCT_2:def 1;
hence H is being_homeomorphism by A1, A2, A11, A9, A6, A10; :: thesis: verum