deffunc H₁( Function) -> set = commute $1;
let X be non empty set ; :: thesis: 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 )
let S, T be non empty Poset; :: thesis: ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st
( F is commuting & F is isomorphic )
consider F being ManySortedSet of the carrier of (UPS (S,(T |^ X))) such that
A1: for f being Element of (UPS (S,(T |^ X))) holds F . f = H₁(f) from PBOOLE:sch 5();
A2: dom F = the carrier of (UPS (S,(T |^ X))) by PARTFUN1:def 2;
A3: rng F c= the carrier of ((UPS (S,T)) |^ X)

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in rng F or g in the carrier of ((UPS (S,T)) |^ X) )
assume g in rng F ; :: thesis: g in the carrier of ((UPS (S,T)) |^ X)
then consider f being object such that
A4: f in dom F and
A5: g = F . f by FUNCT_1:def 3;
reconsider f = f as directed-sups-preserving Function of S,(T |^ X) by A4, Def4;
g = commute f by A1, A4, A5;
then reconsider g = g as Function of X, the carrier of (UPS (S,T)) by Th39;
A6: rng g c= the carrier of (UPS (S,T)) ;
dom g = X by FUNCT_2:def 1;
then g in Funcs (X, the carrier of (UPS (S,T))) by A6, FUNCT_2:def 2;
hence g in the carrier of ((UPS (S,T)) |^ X) by YELLOW_1:28; :: thesis: verum

end;

then reconsider F = F as Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) by A2, FUNCT_2:2;
take F ; :: thesis: ( F is commuting & F is isomorphic )
consider G being ManySortedSet of the carrier of ((UPS (S,T)) |^ X) such that
A7: for f being Element of ((UPS (S,T)) |^ X) holds G . f = H₁(f) from PBOOLE:sch 5();
A8: dom G = the carrier of ((UPS (S,T)) |^ X) by PARTFUN1:def 2;
A9: rng G c= the carrier of (UPS (S,(T |^ X)))

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in rng G or g in the carrier of (UPS (S,(T |^ X))) )
assume g in rng G ; :: thesis: g in the carrier of (UPS (S,(T |^ X)))
then consider f being object such that
A10: f in dom G and
A11: g = G . f by FUNCT_1:def 3;
the carrier of ((UPS (S,T)) |^ X) = Funcs (X, the carrier of (UPS (S,T))) by YELLOW_1:28;
then reconsider f = f as Function of X, the carrier of (UPS (S,T)) by A10, FUNCT_2:66;
g = commute f by A7, A10, A11;
then g is directed-sups-preserving Function of S,(T |^ X) by Th40;
hence g in the carrier of (UPS (S,(T |^ X))) by Def4; :: thesis: verum

end;

then reconsider G = G as Function of ((UPS (S,T)) |^ X),(UPS (S,(T |^ X))) by A8, FUNCT_2:2;
A12: G is commuting

proof

hereby :: according to WAYBEL27:def 3 :: thesis: for f being Function st f in dom G holds
G . f = commute f

let x be set ; :: thesis: ( x in dom G implies x is Function-yielding Function )
assume x in dom G ; :: thesis: x is Function-yielding Function
then x in Funcs (X, the carrier of (UPS (S,T))) by A8, YELLOW_1:28;
then x is Function of X, the carrier of (UPS (S,T)) by FUNCT_2:66;
hence x is Function-yielding Function ; :: thesis: verum

end;

thus for f being Function st f in dom G holds
G . f = commute f by A7, A8; :: thesis: verum

end;

A13: the carrier of (T |^ X) = Funcs (X, the carrier of T) by YELLOW_1:28;
UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
then A14: (UPS (S,T)) |^ X is full SubRelStr of (T |^ the carrier of S) |^ X by YELLOW16:39;
A15: UPS (S,(T |^ X)) is full SubRelStr of (T |^ X) |^ the carrier of S by Def4;
then A16: G is monotone by A12, A14, Th19;
thus A17: F is commuting :: thesis: F is isomorphic

proof

hereby :: according to WAYBEL27:def 3 :: thesis: for f being Function st f in dom F holds
F . f = commute f

let x be set ; :: thesis: ( x in dom F implies x is Function-yielding Function )
assume x in dom F ; :: thesis: x is Function-yielding Function
then x is Function of S,(T |^ X) by Def4;
hence x is Function-yielding Function ; :: thesis: verum

end;

thus for f being Function st f in dom F holds
F . f = commute f by A1, A2; :: thesis: verum

end;

then A18: F is monotone by A15, A14, Th19;
the carrier of ((UPS (S,T)) |^ X) = Funcs (X, the carrier of (UPS (S,T))) by YELLOW_1:28;
then the carrier of ((UPS (S,T)) |^ X) c= Funcs (X,(Funcs ( the carrier of S, the carrier of T))) by Th22, FUNCT_5:56;
then A19: F * G = id ((UPS (S,T)) |^ X) by A2, A8, A9, A17, A12, Th3;
the carrier of (UPS (S,(T |^ X))) c= Funcs ( the carrier of S, the carrier of (T |^ X)) by Th22;
then G * F = id (UPS (S,(T |^ X))) by A2, A3, A8, A17, A12, A13, Th3;
hence F is isomorphic by A19, A18, A16, YELLOW16:15; :: thesis: verum