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