let F, G be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D); :: thesis: ( ( for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (F . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (F . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (F . (p,f,g)) . d = g . d ) ) ) ) ) & ( for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (G . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (G . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (G . (p,f,g)) . d = g . d ) ) ) ) ) implies F = G )

assume that

A15: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (F . (p,f,g)) = H_{1}(p,f,g) & ( for d being object holds

( ( S_{1}[d,p,f] implies (F . (p,f,g)) . d = f . d ) & ( S_{2}[d,p,g] implies (F . (p,f,g)) . d = g . d ) ) ) )
and

A16: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (G . (p,f,g)) = H_{1}(p,f,g) & ( for d being object holds

( ( S_{1}[d,p,f] implies (G . (p,f,g)) . d = f . d ) & ( S_{2}[d,p,g] implies (G . (p,f,g)) . d = g . d ) ) ) )
; :: thesis: F = G

for f, g being BinominativeFunction of D holds

( dom (F . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (F . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (F . (p,f,g)) . d = g . d ) ) ) ) ) & ( for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (G . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (G . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (G . (p,f,g)) . d = g . d ) ) ) ) ) implies F = G )

assume that

A15: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (F . (p,f,g)) = H

( ( S

A16: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (G . (p,f,g)) = H

( ( S

now :: thesis: for x1, x2, x3 being object st x1 in Pr D & x2 in FPrg D & x3 in FPrg D holds

F . [x1,x2,x3] = G . [x1,x2,x3]

hence
F = G
by MULTOP_1:1; :: thesis: verumF . [x1,x2,x3] = G . [x1,x2,x3]

let x1, x2, x3 be object ; :: thesis: ( x1 in Pr D & x2 in FPrg D & x3 in FPrg 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 FPrg D ; :: thesis: F . [x1,x2,x3] = G . [x1,x2,x3]

reconsider p1 = x1 as PartialPredicate of D by A17, PARTFUN1:46;

reconsider f2 = x2, f3 = x3 as BinominativeFunction of D by A18, A19, PARTFUN1:46;

thus F . [x1,x2,x3] = G . [x1,x2,x3] :: thesis: verum

end;assume that

A17: x1 in Pr D and

A18: x2 in FPrg D and

A19: x3 in FPrg D ; :: thesis: F . [x1,x2,x3] = G . [x1,x2,x3]

reconsider p1 = x1 as PartialPredicate of D by A17, PARTFUN1:46;

reconsider f2 = x2, f3 = x3 as BinominativeFunction of D by A18, A19, 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_{1}(p1,f2,f3)
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_{1} being object holds

( not b_{1} in dom (F . [x1,x2,x3]) or (F . [x1,x2,x3]) . b_{1} = (G . [x1,x2,x3]) . b_{1} )

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_{1}[d,p1,f2] or S_{2}[d,p1,f3] )
by A21;

end;F . [x1,x2,x3] = F . (x1,x2,x3) ;

then A21: dom (F . [x1,x2,x3]) = H

hence dom (F . [x1,x2,x3]) = dom (G . [x1,x2,x3]) by A16, A20; :: according to FUNCT_1:def 11 :: thesis: for b

( not 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

per cases
( S_{1}[d,p1,f2] or S_{2}[d,p1,f3] )
by A23;

end;