defpred S_{1}[ object , object ] means ( ( P_{1}[$1] & $2 = TRUE ) or ( P_{1}[$1] & $2 = FALSE ) );

A2: for d being object st d in F_{2}() holds

ex z being object st

( z in BOOLEAN & S_{1}[d,z] )
_{2}(),BOOLEAN such that

A5: for d being object st d in F_{2}() holds

S_{1}[d,p . d]
from FUNCT_2:sch 1(A2);

A6: p in PFuncs (F_{2}(),BOOLEAN)
by PARTFUN1:45;

PFuncs (F_{2}(),BOOLEAN) c= PFuncs (F_{1}(),BOOLEAN)
by A1, PARTFUN1:50;

then reconsider p = p as PartialPredicate of F_{1}() by A6, PARTFUN1:46;

take p ; :: thesis: ( dom p = F_{2}() & ( for d being object st d in dom p holds

( ( P_{1}[d] implies p . d = TRUE ) & ( P_{1}[d] implies p . d = FALSE ) ) ) )

dom p = F_{2}()
by FUNCT_2:def 1;

hence ( dom p = F_{2}() & ( for d being object st d in dom p holds

( ( P_{1}[d] implies p . d = TRUE ) & ( P_{1}[d] implies p . d = FALSE ) ) ) )
by A5; :: thesis: verum

A2: for d being object st d in F

ex z being object st

( z in BOOLEAN & S

proof

consider p being Function of F
let d be object ; :: thesis: ( d in F_{2}() implies ex z being object st

( z in BOOLEAN & S_{1}[d,z] ) )

assume d in F_{2}()
; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[d,z] )

end;( z in BOOLEAN & S

assume d in F

( z in BOOLEAN & S

per cases
( S_{1}[d, TRUE ] or S_{1}[d, FALSE ] )
;

end;

suppose A3:
S_{1}[d, TRUE ]
; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[d,z] )

( z in BOOLEAN & S

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

thus ( TRUE in BOOLEAN & S_{1}[d, TRUE ] )
by A3; :: thesis: verum

end;thus ( TRUE in BOOLEAN & S

suppose A4:
S_{1}[d, FALSE ]
; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[d,z] )

( z in BOOLEAN & S

take
FALSE
; :: thesis: ( FALSE in BOOLEAN & S_{1}[d, FALSE ] )

thus ( FALSE in BOOLEAN & S_{1}[d, FALSE ] )
by A4; :: thesis: verum

end;thus ( FALSE in BOOLEAN & S

A5: for d being object st d in F

S

A6: p in PFuncs (F

PFuncs (F

then reconsider p = p as PartialPredicate of F

take p ; :: thesis: ( dom p = F

( ( P

dom p = F

hence ( dom p = F

( ( P