defpred S₂[ object , object ] means for p being PartialPredicate of D st p = $1 holds
for f being Function st f = $2 holds
( dom p = dom f & ( for d being object holds
( ( S₁[d,p, TRUE ] implies f . d = FALSE ) & ( S₁[d,p, FALSE ] implies f . d = TRUE ) ) ) );
A1: for x being object st x in Pr D holds
ex y being object st
( y in Pr D & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in Pr D implies ex y being object st
( y in Pr D & S₂[x,y] ) )
assume x in Pr D ; :: thesis: ex y being object st
( y in Pr D & S₂[x,y] )
then reconsider X = x as PartFunc of D,BOOLEAN by PARTFUN1:46;
defpred S₃[ object , object ] means for d being object st d = $1 holds
( ( S₁[d,X, TRUE ] implies $2 = FALSE ) & ( S₁[d,X, FALSE ] implies $2 = TRUE ) );
A2: for a being object st a in dom X holds
ex b being object st
( b in BOOLEAN & S₃[a,b] )

proof

let a be object ; :: thesis: ( a in dom X implies ex b being object st
( b in BOOLEAN & S₃[a,b] ) )
assume a in dom X ; :: thesis: ex b being object st
( b in BOOLEAN & S₃[a,b] )
then X . a in BOOLEAN by PARTFUN1:4;

per cases then ( X . a = TRUE or X . a = FALSE ) by TARSKI:def 2;

suppose A3: X . a = TRUE ; :: thesis: ex b being object st
( b in BOOLEAN & S₃[a,b] )

take FALSE ; :: thesis: ( FALSE in BOOLEAN & S₃[a, FALSE ] )
thus ( FALSE in BOOLEAN & S₃[a, FALSE ] ) by A3; :: thesis: verum

end;

suppose A4: X . a = FALSE ; :: thesis: ex b being object st
( b in BOOLEAN & S₃[a,b] )

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S₃[a, TRUE ] )
thus ( TRUE in BOOLEAN & S₃[a, TRUE ] ) by A4; :: thesis: verum

end;

end;

end;

consider g being Function such that
A5: dom g = dom X and
A6: rng g c= BOOLEAN and
A7: for x being object st x in dom X holds
S₃[x,g . x] from FUNCT_1:sch 6(A2);
take g ; :: thesis: ( g in Pr D & S₂[x,g] )
g is PartFunc of D,BOOLEAN by A5, A6, RELSET_1:4;
hence g in Pr D by PARTFUN1:45; :: thesis: S₂[x,g]
thus S₂[x,g] by A5, A7; :: thesis: verum

end;

consider F being Function of (Pr D),(Pr D) such that
A8: for x being object st x in Pr D holds
S₂[x,F . x] from FUNCT_2:sch 1(A1);
take F ; :: thesis: for p being PartialPredicate of D holds
( dom (F . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (F . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (F . p) . d = TRUE ) ) ) )
let p be PartialPredicate of D; :: thesis: ( dom (F . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (F . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (F . p) . d = TRUE ) ) ) )
p in Pr D by PARTFUN1:45;
hence ( dom (F . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (F . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (F . p) . d = TRUE ) ) ) ) by A8; :: thesis: verum