defpred S_{2}[ object , object , object ] means for p being PartialPredicate of D

for f being BinominativeFunction of D st $1 = p & $2 = f holds

for h being Function st h = $3 holds

( dom h = H_{1}(p,f) & ( for d being object st d in dom h holds

ex n being Nat st

( S_{1}[d,p,f,n] & h . d = (iter (f,n)) . d ) ) );

A1: for x1, x2 being object st x1 in Pr D & x2 in FPrg D holds

ex y being object st

( y in FPrg D & S_{2}[x1,x2,y] )

A10: for x, y being object st x in Pr D & y in FPrg D holds

S_{2}[x,y,F . (x,y)]
from BINOP_1:sch 1(A1);

take F ; :: 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 ) ) )

let p be PartialPredicate of D; :: thesis: 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 ) ) )

let f be BinominativeFunction of D; :: thesis: ( 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 ) ) )

A11: ( p in Pr D & f in FPrg D ) by PARTFUN1:45;

hence dom (F . (p,f)) = H_{1}(p,f)
by A10; :: thesis: 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 )

let d be object ; :: thesis: ( d in dom (F . (p,f)) implies 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 ) )

assume d in dom (F . (p,f)) ; :: thesis: 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 )

then consider n being Nat such that

A12: ( S_{1}[d,p,f,n] & (F . (p,f)) . d = (iter (f,n)) . d )
by A10, A11;

take n ; :: thesis: ( ( 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 )

thus ( ( 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 ) by A12; :: thesis: verum

for f being BinominativeFunction of D st $1 = p & $2 = f holds

for h being Function st h = $3 holds

( dom h = H

ex n being Nat st

( S

A1: for x1, x2 being object st x1 in Pr D & x2 in FPrg D holds

ex y being object st

( y in FPrg D & S

proof

consider F being Function of [:(Pr D),(FPrg D):],(FPrg D) such that
let x1, x2 be object ; :: thesis: ( x1 in Pr D & x2 in FPrg D implies ex y being object st

( y in FPrg D & S_{2}[x1,x2,y] ) )

assume x1 in Pr D ; :: thesis: ( not x2 in FPrg D or ex y being object st

( y in FPrg D & S_{2}[x1,x2,y] ) )

then reconsider X1 = x1 as PartFunc of D,BOOLEAN by PARTFUN1:46;

assume x2 in FPrg D ; :: thesis: ex y being object st

( y in FPrg D & S_{2}[x1,x2,y] )

then reconsider X2 = x2 as PartFunc of D,D by PARTFUN1:46;

defpred S_{3}[ object , object ] means for d being object st d = $1 holds

ex n being Nat st

( S_{1}[d,X1,X2,n] & $2 = (iter (X2,n)) . d );

A2: for a being object st a in H_{1}(X1,X2) holds

ex b being object st

( b in D & S_{3}[a,b] )

A7: dom K = H_{1}(X1,X2)
and

A8: rng K c= D and

A9: for x being object st x in H_{1}(X1,X2) holds

S_{3}[x,K . x]
from FUNCT_1:sch 6(A2);

take K ; :: thesis: ( K in FPrg D & S_{2}[x1,x2,K] )

H_{1}(X1,X2) c= D

hence K in FPrg D by PARTFUN1:45; :: thesis: S_{2}[x1,x2,K]

thus S_{2}[x1,x2,K]
by A7, A9; :: thesis: verum

end;( y in FPrg D & S

assume x1 in Pr D ; :: thesis: ( not x2 in FPrg D or ex y being object st

( y in FPrg D & S

then reconsider X1 = x1 as PartFunc of D,BOOLEAN by PARTFUN1:46;

assume x2 in FPrg D ; :: thesis: ex y being object st

( y in FPrg D & S

then reconsider X2 = x2 as PartFunc of D,D by PARTFUN1:46;

defpred S

ex n being Nat st

( S

A2: for a being object st a in H

ex b being object st

( b in D & S

proof

consider K being Function such that
let a be object ; :: thesis: ( a in H_{1}(X1,X2) implies ex b being object st

( b in D & S_{3}[a,b] ) )

assume a in H_{1}(X1,X2)
; :: thesis: ex b being object st

( b in D & S_{3}[a,b] )

then consider d being Element of D such that

A3: d = a and

A4: ex n being Nat st S_{1}[d,X1,X2,n]
;

consider n being Nat such that

A5: S_{1}[d,X1,X2,n]
by A4;

take (iter (X2,n)) . d ; :: thesis: ( (iter (X2,n)) . d in D & S_{3}[a,(iter (X2,n)) . d] )

A6: iter (X2,n) is PartFunc of D,D by FUNCT_7:86;

dom (X1 * (iter (X2,n))) c= dom (iter (X2,n)) by RELAT_1:25;

hence (iter (X2,n)) . d in D by A5, A6, PARTFUN1:4; :: thesis: S_{3}[a,(iter (X2,n)) . d]

thus S_{3}[a,(iter (X2,n)) . d]
by A3, A5; :: thesis: verum

end;( b in D & S

assume a in H

( b in D & S

then consider d being Element of D such that

A3: d = a and

A4: ex n being Nat st S

consider n being Nat such that

A5: S

take (iter (X2,n)) . d ; :: thesis: ( (iter (X2,n)) . d in D & S

A6: iter (X2,n) is PartFunc of D,D by FUNCT_7:86;

dom (X1 * (iter (X2,n))) c= dom (iter (X2,n)) by RELAT_1:25;

hence (iter (X2,n)) . d in D by A5, A6, PARTFUN1:4; :: thesis: S

thus S

A7: dom K = H

A8: rng K c= D and

A9: for x being object st x in H

S

take K ; :: thesis: ( K in FPrg D & S

H

proof

then
K is PartFunc of D,D
by A7, A8, RELSET_1:4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(X1,X2) or x in D )

assume x in H_{1}(X1,X2)
; :: thesis: x in D

then ex d being Element of D st

( d = x & ex n being Nat st S_{1}[d,X1,X2,n] )
;

hence x in D ; :: thesis: verum

end;assume x in H

then ex d being Element of D st

( d = x & ex n being Nat st S

hence x in D ; :: thesis: verum

hence K in FPrg D by PARTFUN1:45; :: thesis: S

thus S

A10: for x, y being object st x in Pr D & y in FPrg D holds

S

take F ; :: 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 ) ) )

let p be PartialPredicate of D; :: thesis: 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 ) ) )

let f be BinominativeFunction of D; :: thesis: ( 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 ) ) )

A11: ( p in Pr D & f in FPrg D ) by PARTFUN1:45;

hence 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 )

let d be object ; :: thesis: ( d in dom (F . (p,f)) implies 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 ) )

assume d in dom (F . (p,f)) ; :: thesis: 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 )

then consider n being Nat such that

A12: ( S

take n ; :: thesis: ( ( 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 )

thus ( ( 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 ) by A12; :: thesis: verum