let X be non empty set ; :: thesis: for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic
let S, T be non empty Poset; :: thesis: UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic
consider F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) such that
A1: ( F is commuting & F is isomorphic ) by Th41;
take F ; :: according to WAYBEL_1:def 8 :: thesis: F is isomorphic
thus F is isomorphic by A1; :: thesis: verum