theorem Th41: :: WAYBEL27:41

for X being non empty set
for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st
( F is commuting & F is isomorphic )