let f, g be Function of [:(Pr D),(Pr D):],(Pr D); :: thesis: ( ( for p, q being PartialPredicate of D holds
( dom (f . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (f . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (f . (p,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D holds
( dom (g . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (g . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (g . (p,q)) . d = FALSE ) ) ) ) ) implies f = g )
assume that
A17: for p, q being PartialPredicate of D holds
( dom (f . (p,q)) = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies (f . (p,q)) . d = TRUE ) & ( S2[d,p,q] implies (f . (p,q)) . d = FALSE ) ) ) ) and
A18: for p, q being PartialPredicate of D holds
( dom (g . (p,q)) = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies (g . (p,q)) . d = TRUE ) & ( S2[d,p,q] implies (g . (p,q)) . d = FALSE ) ) ) ) ; :: thesis: f = g
let x1, x2 be set ; :: according to BINOP_1:def 21 :: thesis: ( not x1 in Pr D or not x2 in Pr D or f . (x1,x2) = g . (x1,x2) )
assume that
A19: x1 in Pr D and
A20: x2 in Pr D ; :: thesis: f . (x1,x2) = g . (x1,x2)
reconsider p1 = x1, p2 = x2 as PartialPredicate of D by A19, A20, PARTFUN1:46;
A21: dom (f . (x1,x2)) = H1(p1,p2) by A17;
hence dom (f . (x1,x2)) = dom (g . (x1,x2)) by A18; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (f . (x1,x2)) or (f . (x1,x2)) . b1 = (g . (x1,x2)) . b1 )
let a be object ; :: thesis: ( not a in dom (f . (x1,x2)) or (f . (x1,x2)) . a = (g . (x1,x2)) . a )
assume a in dom (f . (x1,x2)) ; :: thesis: (f . (x1,x2)) . a = (g . (x1,x2)) . a
then consider d being Element of D such that
A22: a = d and
A23: ( S1[d,p1] or S1[d,p2] or S2[d,p1,p2] ) by A21;
per cases ( S1[d,p1] or S1[d,p2] or S2[d,p1,p2] ) by A23;
suppose A24: ( S1[d,p1] or S1[d,p2] ) ; :: thesis: (f . (x1,x2)) . a = (g . (x1,x2)) . a
thus (f . (x1,x2)) . a = (f . (p1,p2)) . a
.= TRUE by A17, A22, A24
.= (g . (p1,p2)) . a by A18, A22, A24
.= (g . (x1,x2)) . a ; :: thesis: verum
end;
suppose A25: S2[d,p1,p2] ; :: thesis: (f . (x1,x2)) . a = (g . (x1,x2)) . a
thus (f . (x1,x2)) . a = FALSE by A17, A22, A25
.= (g . (x1,x2)) . a by A18, A22, A25 ; :: thesis: verum
end;
end;