defpred S₂[ object , object ] means for p being PartialPredicate of D st p = $1 holds
for f being Function st f = $2 holds
( H₁(p) = dom f & ( for d being Element of D st not S₁[d,p] holds
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 Element of D st d = $1 & not S₁[d,X] holds
$2 = TRUE ;
A2: H₁(X) c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(X) or x in D )
assume x in H₁(X) ; :: thesis: x in D
then ex d being Element of D st
( x = d & not d in dom X ) ;
hence x in D ; :: thesis: verum

end;

A3: for a being object st a in H₁(X) holds
ex b being object st
( b in BOOLEAN & S₃[a,b] )

proof

let a be object ; :: thesis: ( a in H₁(X) implies ex b being object st
( b in BOOLEAN & S₃[a,b] ) )
assume a in H₁(X) ; :: 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 ] ) ; :: thesis: verum

end;

consider g being Function such that
A4: dom g = H₁(X) and
A5: rng g c= BOOLEAN and
A6: for x being object st x in H₁(X) holds
S₃[x,g . x] from FUNCT_1:sch 6(A3);
take g ; :: thesis: ( g in Pr D & S₂[x,g] )
g is PartFunc of D,BOOLEAN by A2, A4, A5, RELSET_1:4;
hence g in Pr D by PARTFUN1:45; :: thesis: S₂[x,g]
let p be PartialPredicate of D; :: thesis: ( p = x implies for f being Function st f = g holds
( H₁(p) = dom f & ( for d being Element of D st not S₁[d,p] holds
f . d = TRUE ) ) )
assume A7: p = x ; :: thesis: for f being Function st f = g holds
( H₁(p) = dom f & ( for d being Element of D st not S₁[d,p] holds
f . d = TRUE ) )
let f be Function; :: thesis: ( f = g implies ( H₁(p) = dom f & ( for d being Element of D st not S₁[d,p] holds
f . d = TRUE ) ) )
assume A8: f = g ; :: thesis: ( H₁(p) = dom f & ( for d being Element of D st not S₁[d,p] holds
f . d = TRUE ) )
thus H₁(p) = dom f by A4, A7, A8; :: thesis: for d being Element of D st not S₁[d,p] holds
f . d = TRUE
let d be Element of D; :: thesis: ( not S₁[d,p] implies f . d = TRUE )
assume A9: not S₁[d,p] ; :: thesis: f . d = TRUE
then d in H₁(X) by A7;
hence f . d = TRUE by A6, A7, A8, A9; :: thesis: verum

end;

consider F being Function of (Pr D),(Pr D) such that
A10: 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) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds
(F . p) . d = TRUE ) )
let p be PartialPredicate of D; :: thesis: ( dom (F . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds
(F . p) . d = TRUE ) )
p in Pr D by PARTFUN1:45;
hence ( dom (F . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds
(F . p) . d = TRUE ) ) by A10; :: thesis: verum