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₁(p) & ( for d being Element of D st not S₁[d,p] holds
(f . p) . d = TRUE ) ) and
A12: for p being PartialPredicate of D holds
( dom (g . p) = H₁(p) & ( for d being Element of D st not S₁[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₁(p) by A11
.= dom (g . x) by A12 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (f . x) or (f . x) . b₁ = (g . x) . 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₁(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