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 that
A1: f is isomorphic and
A2: g is isomorphic ; :: thesis: UPS f,g is isomorphic
A3: g is sups-preserving Function of T1,T2 by A2, WAYBEL13:20;
A4: f is sups-preserving Function of S1,S2 by A1, WAYBEL13:20;
then A5: UPS f,g is directed-sups-preserving Function of (UPS S2,T1),(UPS S1,T2) by A3, Th30;
consider g' being monotone Function of T2,T1 such that
A6: g * g' = id T2 and
A7: g' * g = id T1 by A2, YELLOW16:17;
g' is isomorphic by A2, A6, A7, YELLOW16:17;
then A8: g' is sups-preserving Function of T2,T1 by WAYBEL13:20;
consider f' being monotone Function of S2,S1 such that
A9: f * f' = id S2 and
A10: f' * f = id S1 by A1, YELLOW16:17;
f' is isomorphic by A1, A9, A10, YELLOW16:17;
then A11: f' is sups-preserving Function of S2,S1 by WAYBEL13:20;
then A12: UPS f',g' is directed-sups-preserving Function of (UPS S1,T2),(UPS S2,T1) by A8, Th30;
A13: (UPS f',g') * (UPS f,g) = UPS (id S2),(id T1) by A4, A3, A9, A7, A11, A8, Th28
.= id (UPS S2,T1) by Th29 ;
(UPS f,g) * (UPS f',g') = UPS (id S1),(id T2) by A4, A3, A10, A6, A11, A8, Th28
.= id (UPS S1,T2) by Th29 ;
hence UPS f,g is isomorphic by A13, A5, A12, YELLOW16:17; :: thesis: verum