let F, G be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D); ( ( 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)) = H1(p,f,g) & ( for d being object holds
( ( S1[d,p,f] implies (F . (p,f,g)) . d = f . d ) & ( S2[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)) = H1(p,f,g) & ( for d being object holds
( ( S1[d,p,f] implies (G . (p,f,g)) . d = f . d ) & ( S2[d,p,g] implies (G . (p,f,g)) . d = g . d ) ) ) )
; F = G
now 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]let x1,
x2,
x3 be
object ;
( 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
;
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]
verumproof
A20:
G . [x1,x2,x3] = G . (
x1,
x2,
x3)
;
F . [x1,x2,x3] = F . (
x1,
x2,
x3)
;
then A21:
dom (F . [x1,x2,x3]) = H1(
p1,
f2,
f3)
by A15;
hence
dom (F . [x1,x2,x3]) = dom (G . [x1,x2,x3])
by A16, A20;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (F . [x1,x2,x3]) or (F . [x1,x2,x3]) . b1 = (G . [x1,x2,x3]) . b1 )
let a be
object ;
( 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])
;
(F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . a
then consider d being
Element of
D such that A22:
a = d
and A23:
(
S1[
d,
p1,
f2] or
S2[
d,
p1,
f3] )
by A21;
per cases
( S1[d,p1,f2] or S2[d,p1,f3] )
by A23;
suppose A24:
S1[
d,
p1,
f2]
;
(F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . athus (F . [x1,x2,x3]) . a =
(F . (p1,f2,f3)) . a
.=
f2 . d
by A15, A22, A24
.=
(G . (p1,f2,f3)) . a
by A16, A22, A24
.=
(G . [x1,x2,x3]) . a
;
verum end; suppose A25:
S2[
d,
p1,
f3]
;
(F . [x1,x2,x3]) . a = (G . [x1,x2,x3]) . athus (F . [x1,x2,x3]) . a =
(F . (p1,f2,f3)) . a
.=
f3 . d
by A15, A22, A25
.=
(G . (p1,f2,f3)) . a
by A16, A22, A25
.=
(G . [x1,x2,x3]) . a
;
verum end; end;
end; end;
hence
F = G
by MULTOP_1:1; verum