defpred S2[ object , object ] means for p being PartialPredicate of D st p = $1 holds
for f being Function st f = $2 holds
( H1(p) = dom f & ( for d being Element of D st not S1[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 & 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 Element of D st d = $1 & not S1[d,X] holds
$2 = TRUE ;
A2: H1(X) c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(X) or x in D )
assume x in H1(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 H1(X) holds
ex b being object st
( b in BOOLEAN & S3[a,b] )
proof
let a be object ; :: thesis: ( a in H1(X) implies ex b being object st
( b in BOOLEAN & S3[a,b] ) )
assume a in H1(X) ; :: 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 ] ) ; :: thesis: verum
end;
consider g being Function such that
A4: dom g = H1(X) and
A5: rng g c= BOOLEAN and
A6: for x being object st x in H1(X) holds
S3[x,g . x] from FUNCT_1:sch 6(A3);
 take g ; :: thesis: ( g in Pr D & S2[x,g] )
g is PartFunc of D,BOOLEAN by A2, A4, A5, RELSET_1:4;
hence g in Pr D by PARTFUN1:45; :: thesis: S2[x,g]
let p be PartialPredicate of D; :: thesis: ( p = x implies for f being Function st f = g holds
( H1(p) = dom f & ( for d being Element of D st not S1[d,p] holds
f . d = TRUE ) ) )
assume A7: p = x ; :: thesis: for f being Function st f = g holds
( H1(p) = dom f & ( for d being Element of D st not S1[d,p] holds
f . d = TRUE ) )
let f be Function; :: thesis: ( f = g implies ( H1(p) = dom f & ( for d being Element of D st not S1[d,p] holds
f . d = TRUE ) ) )
assume A8: f = g ; :: thesis: ( H1(p) = dom f & ( for d being Element of D st not S1[d,p] holds
f . d = TRUE ) )
thus H1(p) = dom f by A4, A7, A8; :: thesis: for d being Element of D st not S1[d,p] holds
f . d = TRUE
let d be Element of D; :: thesis: ( not S1[d,p] implies f . d = TRUE )
assume A9: not S1[d,p] ; :: thesis: f . d = TRUE
then d in H1(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
S2[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