let f, g be Function of (Pr D),(Pr D); ( ( for p being PartialPredicate of D holds
( dom (f . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (f . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (f . p) . d = TRUE ) ) ) ) ) & ( for p being PartialPredicate of D holds
( dom (g . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (g . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (g . p) . d = TRUE ) ) ) ) ) implies f = g )
assume that
A9:
for p being PartialPredicate of D holds
( dom p = dom (f . p) & ( for d being object holds
( ( S1[d,p, TRUE ] implies (f . p) . d = FALSE ) & ( S1[d,p, FALSE ] implies (f . p) . d = TRUE ) ) ) )
and
A10:
for p being PartialPredicate of D holds
( dom p = dom (g . p) & ( for d being object holds
( ( S1[d,p, TRUE ] implies (g . p) . d = FALSE ) & ( S1[d,p, FALSE ] implies (g . p) . d = TRUE ) ) ) )
; f = g
let x be Element of Pr D; FUNCT_2:def 8 f . x = g . x
reconsider p = x as PartialPredicate of D by PARTFUN1:46;
thus dom (f . x) =
dom p
by A9
.=
dom (g . x)
by A10
; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (f . x) or (f . x) . b1 = (g . x) . b1 )
let a be object ; ( not a in dom (f . x) or (f . x) . a = (g . x) . a )
assume
a in dom (f . x)
; (f . x) . a = (g . x) . a
then A11:
a in dom p
by A9;
then
p . a in BOOLEAN
by PARTFUN1:4;