defpred S2[ 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
( ( S1[d,p, TRUE ] implies f . d = FALSE ) & ( S1[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 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in Pr D implies ex y being object st
( y in Pr D & S2[x,y] ) )
assume x in Pr D ; :: thesis: ex y being object st
( y in Pr D & S2[x,y] )
then reconsider X = x as PartFunc of D,BOOLEAN by PARTFUN1:46;
defpred S3[ object , object ] means for d being object st d = $1 holds
( ( S1[d,X, TRUE ] implies $2 = FALSE ) & ( S1[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 & S3[a,b] )
proof
let a be object ; :: thesis: ( a in dom X implies ex b being object st
( b in BOOLEAN & S3[a,b] ) )
assume a in dom X ; :: thesis: ex b being object st
( b in BOOLEAN & S3[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 & S3[a,b] )
take FALSE ; :: thesis: ( FALSE in BOOLEAN & S3[a, FALSE ] )
thus ( FALSE in BOOLEAN & S3[a, FALSE ] ) by A3; :: thesis: verum
end;
suppose A4: X . a = FALSE ; :: thesis: ex b being object st
( b in BOOLEAN & S3[a,b] )
take TRUE ; :: thesis: ( TRUE in BOOLEAN & S3[a, TRUE ] )
thus ( TRUE in BOOLEAN & S3[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
S3[x,g . x] from FUNCT_1:sch 6(A2);
 take g ; :: thesis: ( g in Pr D & S2[x,g] )
g is PartFunc of D,BOOLEAN by A5, A6, RELSET_1:4;
hence g in Pr D by PARTFUN1:45; :: thesis: S2[x,g]
thus S2[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
S2[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