let S1, S2, T1, T2 be complete LATTICE; :: thesis: for f being Function of S1,S2
for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds
UPS f,g is isomorphic
let f be Function of S1,S2; :: thesis: for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds
UPS f,g is isomorphic
let g be Function of T1,T2; :: thesis: ( f is isomorphic & g is isomorphic implies UPS f,g is isomorphic )
assume A1: ( f is isomorphic & g is isomorphic ) ; :: thesis: UPS f,g is isomorphic
then A2: ( f is sups-preserving Function of S1,S2 & g is sups-preserving Function of T1,T2 ) by WAYBEL13:20;
consider f' being monotone Function of S2,S1 such that
A3: ( f * f' = id S2 & f' * f = id S1 ) by A1, YELLOW16:17;
consider g' being monotone Function of T2,T1 such that
A4: ( g * g' = id T2 & g' * g = id T1 ) by A1, YELLOW16:17;
A5: UPS f,g is directed-sups-preserving Function of (UPS S2,T1),(UPS S1,T2) by A2, Th30;
( f' is isomorphic & g' is isomorphic ) by A2, A3, A4, YELLOW16:17;
then A6: ( f' is sups-preserving Function of S2,S1 & g' is sups-preserving Function of T2,T1 ) by WAYBEL13:20;
then A7: UPS f',g' is directed-sups-preserving Function of (UPS S1,T2),(UPS S2,T1) by Th30;
A8: (UPS f,g) * (UPS f',g') = UPS (id S1),(id T2) by A2, A3, A4, A6, Th28
.= id (UPS S1,T2) by Th29 ;
(UPS f',g') * (UPS f,g) = UPS (id S2),(id T1) by A2, A3, A4, A6, Th28
.= id (UPS S2,T1) by Th29 ;
hence UPS f,g is isomorphic by A5, A7, A8, YELLOW16:17; :: thesis: verum