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_{1}(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_{1}(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_{1}(p,f)
by A13

.= dom (G . (a,b)) by A14 ; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom (F . (a,b)) or (F . (a,b)) . b_{1} = (G . (a,b)) . b_{1} )

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

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

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

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

.= dom (G . (a,b)) by A14 ; :: according to FUNCT_1:def 11 :: thesis: for b

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

hence
(F . (a,b)) . z = (G . (a,b)) . z
by A22, A25; :: thesis: verum
assume
m <> n
; :: thesis: contradiction

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

end;