defpred S_{2}[ object , object ] means for p being PartialPredicate of D st p = $1 holds

for f being Function st f = $2 holds

( H_{1}(p) = dom f & ( for d being Element of D st not S_{1}[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_{2}[x,y] )

A10: for x being object st x in Pr D holds

S_{2}[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

for f being Function st f = $2 holds

( H

f . d = TRUE ) );

A1: for x being object st x in Pr D holds

ex y being object st

( y in Pr D & S

proof

consider F being Function of (Pr D),(Pr D) such that
let x be object ; :: thesis: ( x in Pr D implies ex y being object st

( y in Pr D & S_{2}[x,y] ) )

assume x in Pr D ; :: thesis: ex y being object st

( y in Pr D & S_{2}[x,y] )

then reconsider X = x as PartFunc of D,BOOLEAN by PARTFUN1:46;

defpred S_{3}[ object , object ] means for d being Element of D st d = $1 & not S_{1}[d,X] holds

$2 = TRUE ;

A2: H_{1}(X) c= D
_{1}(X) holds

ex b being object st

( b in BOOLEAN & S_{3}[a,b] )

A4: dom g = H_{1}(X)
and

A5: rng g c= BOOLEAN and

A6: for x being object st x in H_{1}(X) holds

S_{3}[x,g . x]
from FUNCT_1:sch 6(A3);

take g ; :: thesis: ( g in Pr D & S_{2}[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_{2}[x,g]

let p be PartialPredicate of D; :: thesis: ( p = x implies for f being Function st f = g holds

( H_{1}(p) = dom f & ( for d being Element of D st not S_{1}[d,p] holds

f . d = TRUE ) ) )

assume A7: p = x ; :: thesis: for f being Function st f = g holds

( H_{1}(p) = dom f & ( for d being Element of D st not S_{1}[d,p] holds

f . d = TRUE ) )

let f be Function; :: thesis: ( f = g implies ( H_{1}(p) = dom f & ( for d being Element of D st not S_{1}[d,p] holds

f . d = TRUE ) ) )

assume A8: f = g ; :: thesis: ( H_{1}(p) = dom f & ( for d being Element of D st not S_{1}[d,p] holds

f . d = TRUE ) )

thus H_{1}(p) = dom f
by A4, A7, A8; :: thesis: for d being Element of D st not S_{1}[d,p] holds

f . d = TRUE

let d be Element of D; :: thesis: ( not S_{1}[d,p] implies f . d = TRUE )

assume A9: not S_{1}[d,p]
; :: thesis: f . d = TRUE

then d in H_{1}(X)
by A7;

hence f . d = TRUE by A6, A7, A8, A9; :: thesis: verum

end;( y in Pr D & S

assume x in Pr D ; :: thesis: ex y being object st

( y in Pr D & S

then reconsider X = x as PartFunc of D,BOOLEAN by PARTFUN1:46;

defpred S

$2 = TRUE ;

A2: H

proof

A3:
for a being object st a in H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(X) or x in D )

assume x in H_{1}(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;assume x in H

then ex d being Element of D st

( x = d & not d in dom X ) ;

hence x in D ; :: thesis: verum

ex b being object st

( b in BOOLEAN & S

proof

consider g being Function such that
let a be object ; :: thesis: ( a in H_{1}(X) implies ex b being object st

( b in BOOLEAN & S_{3}[a,b] ) )

assume a in H_{1}(X)
; :: thesis: ex b being object st

( b in BOOLEAN & S_{3}[a,b] )

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S_{3}[a, TRUE ] )

thus ( TRUE in BOOLEAN & S_{3}[a, TRUE ] )
; :: thesis: verum

end;( b in BOOLEAN & S

assume a in H

( b in BOOLEAN & S

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S

thus ( TRUE in BOOLEAN & S

A4: dom g = H

A5: rng g c= BOOLEAN and

A6: for x being object st x in H

S

take g ; :: thesis: ( g in Pr D & S

g is PartFunc of D,BOOLEAN by A2, A4, A5, RELSET_1:4;

hence g in Pr D by PARTFUN1:45; :: thesis: S

let p be PartialPredicate of D; :: thesis: ( p = x implies for f being Function st f = g holds

( H

f . d = TRUE ) ) )

assume A7: p = x ; :: thesis: for f being Function st f = g holds

( H

f . d = TRUE ) )

let f be Function; :: thesis: ( f = g implies ( H

f . d = TRUE ) ) )

assume A8: f = g ; :: thesis: ( H

f . d = TRUE ) )

thus H

f . d = TRUE

let d be Element of D; :: thesis: ( not S

assume A9: not S

then d in H

hence f . d = TRUE by A6, A7, A8, A9; :: thesis: verum

A10: for x being object st x in Pr D holds

S

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