let F, G be Function of [:(Pr D),(FPrg D):],(FPrg D); :: thesis: ( ( for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (F . (p,f)) = { d where d is Element of D : ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (F . (p,f)) holds
ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (F . (p,f)) . d = (iter (f,n)) . d ) ) ) ) & ( for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (G . (p,f)) = { d where d is Element of D : ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (G . (p,f)) holds
ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (G . (p,f)) . d = (iter (f,n)) . d ) ) ) ) implies F = G )
assume that
A13: for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (F . (p,f)) = H₁(p,f) & ( for d being object st d in dom (F . (p,f)) holds
ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (F . (p,f)) . d = (iter (f,n)) . d ) ) ) and
A14: for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (G . (p,f)) = H₁(p,f) & ( for d being object st d in dom (G . (p,f)) holds
ex n being Nat st
( ( for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (G . (p,f)) . d = (iter (f,n)) . d ) ) ) ; :: thesis: F = G
let a, b be set ; :: according to BINOP_1:def 21 :: thesis: ( not a in Pr D or not b in FPrg D or F . (a,b) = G . (a,b) )
assume A15: a in Pr D ; :: thesis: ( not b in FPrg D or F . (a,b) = G . (a,b) )
then reconsider p = a as PartialPredicate of D by PARTFUN1:46;
assume A16: b in FPrg D ; :: thesis: F . (a,b) = G . (a,b)
then reconsider f = b as BinominativeFunction of D by PARTFUN1:46;
F . (a,b) in FPrg D by A15, A16, BINOP_1:17;
then A17: dom (F . (a,b)) c= D by RELAT_1:def 18;
thus A18: dom (F . (a,b)) = H₁(p,f) by A13
.= dom (G . (a,b)) by A14 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (F . (a,b)) or (F . (a,b)) . b₁ = (G . (a,b)) . b₁ )
let z be object ; :: thesis: ( not z in dom (F . (a,b)) or (F . (a,b)) . z = (G . (a,b)) . z )
assume A19: z in dom (F . (a,b)) ; :: thesis: (F . (a,b)) . z = (G . (a,b)) . z
then reconsider d = z as Element of D by A17;
consider n being Nat such that
A20: for i being Nat st i <= n - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) and
A21: ( d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) and
A22: (F . (p,f)) . d = (iter (f,n)) . d by A13, A19;
consider m being Nat such that
A23: for i being Nat st i <= m - 1 holds
( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) and
A24: ( d in dom (p * (iter (f,m))) & (p * (iter (f,m))) . d = FALSE ) and
A25: (G . (p,f)) . d = (iter (f,m)) . d by A14, A18, A19;
m = n

proof

assume m <> n ; :: thesis: contradiction

per cases then ( m < n or m > n ) by XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

then m <= n - 1 by INT_1:52;
hence contradiction by A20, A24; :: thesis: verum

end;

suppose m > n ; :: thesis: contradiction

then n <= m - 1 by INT_1:52;
hence contradiction by A21, A23; :: thesis: verum

end;

end;

end;

hence (F . (a,b)) . z = (G . (a,b)) . z by A22, A25; :: thesis: verum