let f1, f2 be BinOp of (Pr D); :: thesis: ( ( for p, q being PartialPredicate of D holds f1 . (p,q) = PP_and (p,q) ) & ( for p, q being PartialPredicate of D holds f2 . (p,q) = PP_and (p,q) ) implies f1 = f2 )
assume that
A3: for p, q being PartialPredicate of D holds f1 . (p,q) = PP_and (p,q) and
A4: for p, q being PartialPredicate of D holds f2 . (p,q) = PP_and (p,q) ; :: thesis: f1 = f2
let x, y be set ; :: according to BINOP_1:def 21 :: thesis: ( not x in Pr D or not y in Pr D or f1 . (x,y) = f2 . (x,y) )
assume x in Pr D ; :: thesis: ( not y in Pr D or f1 . (x,y) = f2 . (x,y) )
then reconsider x1 = x as PartialPredicate of D by PARTFUN1:46;
assume y in Pr D ; :: thesis: f1 . (x,y) = f2 . (x,y)
then reconsider y1 = y as PartialPredicate of D by PARTFUN1:46;
thus f1 . (x,y) = PP_and (x1,y1) by A3
.= f2 . (x,y) by A4 ; :: thesis: verum