let f, g be Function of (Pr D),(Pr D); :: thesis: ( ( 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 ) ) ) ) ; :: 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) = dom p by A9
.= dom (g . x) by A10 ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (f . x) or (f . x) . b1 = (g . x) . b1 )
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 A11: a in dom p by A9;
then p . a in BOOLEAN by PARTFUN1:4;
per cases then ( p . a = TRUE or p . a = FALSE ) by TARSKI:def 2;
suppose A12: p . a = TRUE ; :: thesis: (f . x) . a = (g . x) . a
hence (f . x) . a = FALSE by A9, A11
.= (g . x) . a by A10, A11, A12 ;
:: thesis: verum
end;
suppose A13: p . a = FALSE ; :: thesis: (f . x) . a = (g . x) . a
hence (f . x) . a = TRUE by A9, A11
.= (g . x) . a by A10, A11, A13 ;
:: thesis: verum
end;
end;