let X, Y be non empty set ; :: thesis: for f being Function of X,Y

for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

let f be Function of X,Y; :: thesis: for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

let g be Function of Y,X; :: thesis: ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

deffunc H_{1}( set ) -> Element of bool X = X \ (g .: (Y \ (f .: $1)));

A1: for x being set st x in bool X holds

H_{1}(x) in bool X
;

consider h being Function of (bool X),(bool X) such that

A2: for x being set st x in bool X holds

h . x = H_{1}(x)
from FUNCT_2:sch 11(A1);

take Xa = lfp (X,h); :: thesis: ex Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Xb = X \ Xa; :: thesis: ex Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Ya = f .: Xa; :: thesis: ex Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Yb = Y \ Ya; :: thesis: ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Xa misses Xb by XBOOLE_1:79; :: thesis: ( Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Ya misses Yb by XBOOLE_1:79; :: thesis: ( Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Xa \/ Xb = X by XBOOLE_1:45; :: thesis: ( Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Ya \/ Yb = Y by XBOOLE_1:45; :: thesis: ( f .: Xa = Ya & g .: Yb = Xb )

thus f .: Xa = Ya ; :: thesis: g .: Yb = Xb

A6: Xa is_a_fixpoint_of h by Th4;

thus g .: Yb = X /\ (g .: (Y \ (f .: Xa))) by XBOOLE_1:28

.= X \ (X \ (g .: (Y \ (f .: Xa)))) by XBOOLE_1:48

.= X \ (h . Xa) by A2

.= Xb by A6 ; :: thesis: verum

for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

let f be Function of X,Y; :: thesis: for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

let g be Function of Y,X; :: thesis: ex Xa, Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

deffunc H

A1: for x being set st x in bool X holds

H

consider h being Function of (bool X),(bool X) such that

A2: for x being set st x in bool X holds

h . x = H

now :: thesis: for x, y being set st x in dom h & y in dom h & x c= y holds

h . x c= h . y

then reconsider h = h as V224() Function of (bool X),(bool X) by COHSP_1:def 11;h . x c= h . y

let x, y be set ; :: thesis: ( x in dom h & y in dom h & x c= y implies h . x c= h . y )

assume that

A3: x in dom h and

A4: y in dom h and

A5: x c= y ; :: thesis: h . x c= h . y

f .: x c= f .: y by A5, RELAT_1:123;

then Y \ (f .: y) c= Y \ (f .: x) by XBOOLE_1:34;

then g .: (Y \ (f .: y)) c= g .: (Y \ (f .: x)) by RELAT_1:123;

then X \ (g .: (Y \ (f .: x))) c= X \ (g .: (Y \ (f .: y))) by XBOOLE_1:34;

then h . x c= X \ (g .: (Y \ (f .: y))) by A2, A3;

hence h . x c= h . y by A2, A4; :: thesis: verum

end;assume that

A3: x in dom h and

A4: y in dom h and

A5: x c= y ; :: thesis: h . x c= h . y

f .: x c= f .: y by A5, RELAT_1:123;

then Y \ (f .: y) c= Y \ (f .: x) by XBOOLE_1:34;

then g .: (Y \ (f .: y)) c= g .: (Y \ (f .: x)) by RELAT_1:123;

then X \ (g .: (Y \ (f .: x))) c= X \ (g .: (Y \ (f .: y))) by XBOOLE_1:34;

then h . x c= X \ (g .: (Y \ (f .: y))) by A2, A3;

hence h . x c= h . y by A2, A4; :: thesis: verum

take Xa = lfp (X,h); :: thesis: ex Xb, Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Xb = X \ Xa; :: thesis: ex Ya, Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Ya = f .: Xa; :: thesis: ex Yb being set st

( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

take Yb = Y \ Ya; :: thesis: ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Xa misses Xb by XBOOLE_1:79; :: thesis: ( Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Ya misses Yb by XBOOLE_1:79; :: thesis: ( Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Xa \/ Xb = X by XBOOLE_1:45; :: thesis: ( Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )

thus Ya \/ Yb = Y by XBOOLE_1:45; :: thesis: ( f .: Xa = Ya & g .: Yb = Xb )

thus f .: Xa = Ya ; :: thesis: g .: Yb = Xb

A6: Xa is_a_fixpoint_of h by Th4;

thus g .: Yb = X /\ (g .: (Y \ (f .: Xa))) by XBOOLE_1:28

.= X \ (X \ (g .: (Y \ (f .: Xa)))) by XBOOLE_1:48

.= X \ (h . Xa) by A2

.= Xb by A6 ; :: thesis: verum