let F, G be Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D); :: thesis: ( ( for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (G . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (G . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (G . (p,f,q)) . d = FALSE ) ) ) ) ) implies F = G )
assume that
A15: for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (F . (p,f,q)) = H₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies (F . (p,f,q)) . d = TRUE ) & ( S₂[d,p,f,q] implies (F . (p,f,q)) . d = FALSE ) ) ) ) and
A16: for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (G . (p,f,q)) = H₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies (G . (p,f,q)) . d = TRUE ) & ( S₂[d,p,f,q] implies (G . (p,f,q)) . d = FALSE ) ) ) ) ; :: thesis: F = G

now :: thesis: for x1, x2, x3 being object st x1 in Pr D & x2 in FPrg D & x3 in Pr D holds
F . [x1,x2,x3] = G . [x1,x2,x3]

let x1, x2, x3 be object ; :: thesis: ( x1 in Pr D & x2 in FPrg D & x3 in Pr D implies F . [x1,x2,x3] = G . [x1,x2,x3] )
assume that
A17: x1 in Pr D and
A18: x2 in FPrg D and
A19: x3 in Pr D ; :: thesis: F . [x1,x2,x3] = G . [x1,x2,x3]
reconsider p1 = x1, p3 = x3 as PartialPredicate of D by A17, A19, PARTFUN1:46;
reconsider f2 = x2 as BinominativeFunction of D by A18, PARTFUN1:46;
thus F . [x1,x2,x3] = G . [x1,x2,x3] :: thesis: verum

proof

A20: G . [x1,x2,x3] = G . (x1,x2,x3) ;
F . [x1,x2,x3] = F . (x1,x2,x3) ;
then A21: dom (F . [x1,x2,x3]) = H₁(p1,f2,p3) by A15;
hence dom (F . [x1,x2,x3]) = dom (G . [x1,x2,x3]) by A16, A20; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (F . [x1,x2,x3]) or (F . [x1,x2,x3]) . b₁ = (G . [x1,x2,x3]) . b₁ )
let a be object ; :: thesis: ( not a in dom (F . [x1,x2,x3]) or (F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . a )
assume a in dom (F . [x1,x2,x3]) ; :: thesis: (F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . a
then consider d being Element of D such that
A22: a = d and
A23: ( S₁[d,p1,f2,p3] or S₂[d,p1,f2,p3] ) by A21;

per cases ( S₁[d,p1,f2,p3] or S₂[d,p1,f2,p3] ) by A23;

suppose A24: S₁[d,p1,f2,p3] ; :: thesis: (F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . a

thus (F . [x1,x2,x3]) . a = (F . (p1,f2,p3)) . a
.= TRUE by A15, A22, A24
.= (G . (p1,f2,p3)) . a by A16, A22, A24
.= (G . [x1,x2,x3]) . a ; :: thesis: verum

end;

suppose A25: S₂[d,p1,f2,p3] ; :: thesis: (F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . a

thus (F . [x1,x2,x3]) . a = (F . (p1,f2,p3)) . a
.= FALSE by A15, A22, A25
.= (G . (p1,f2,p3)) . a by A16, A22, A25
.= (G . [x1,x2,x3]) . a ; :: thesis: verum

end;

end;

end;

end;

hence F = G by MULTOP_1:1; :: thesis: verum