let f, g be Function of (Pr D),(Pr D); :: 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 ) ) ) & ( for p being PartialPredicate of D holds

( dom (g . 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

(g . p) . d = TRUE ) ) ) implies f = g )

assume that

A11: for p being PartialPredicate of D holds

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

(f . p) . d = TRUE ) ) and

A12: for p being PartialPredicate of D holds

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

(g . p) . d = TRUE ) ) ; :: thesis: f = g

let x be Element of Pr D; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x

reconsider p = x as PartialPredicate of D by PARTFUN1:46;

thus dom (f . x) = H_{1}(p)
by A11

.= dom (g . x) by A12 ; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom (f . x) or (f . x) . b_{1} = (g . x) . b_{1} )

let a be object ; :: thesis: ( not a in dom (f . x) or (f . x) . a = (g . x) . a )

assume a in dom (f . x) ; :: thesis: (f . x) . a = (g . x) . a

then a in H_{1}(p)
by A11;

then A13: ex d being Element of D st

( a = d & not d in dom p ) ;

hence (f . x) . a = TRUE by A11

.= (g . x) . a by A12, A13 ;

:: thesis: verum

( 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 ) ) ) & ( for p being PartialPredicate of D holds

( dom (g . 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

(g . p) . d = TRUE ) ) ) implies f = g )

assume that

A11: for p being PartialPredicate of D holds

( dom (f . p) = H

(f . p) . d = TRUE ) ) and

A12: for p being PartialPredicate of D holds

( dom (g . p) = H

(g . p) . d = TRUE ) ) ; :: thesis: f = g

let x be Element of Pr D; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x

reconsider p = x as PartialPredicate of D by PARTFUN1:46;

thus dom (f . x) = H

.= dom (g . x) by A12 ; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let a be object ; :: thesis: ( not a in dom (f . x) or (f . x) . a = (g . x) . a )

assume a in dom (f . x) ; :: thesis: (f . x) . a = (g . x) . a

then a in H

then A13: ex d being Element of D st

( a = d & not d in dom p ) ;

hence (f . x) . a = TRUE by A11

.= (g . x) . a by A12, A13 ;

:: thesis: verum