defpred S2[ 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 = H1(p,f) & ( for d being object st d in dom h holds
ex n being Nat st
( S1[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 & S2[x1,x2,y] )
proof
let x1, x2 be object ; :: thesis: ( x1 in Pr D & x2 in FPrg D implies ex y being object st
( y in FPrg D & S2[x1,x2,y] ) )
assume x1 in Pr D ; :: thesis: ( not x2 in FPrg D or ex y being object st
( y in FPrg D & S2[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 & S2[x1,x2,y] )
then reconsider X2 = x2 as PartFunc of D,D by PARTFUN1:46;
defpred S3[ object , object ] means for d being object st d = $1 holds
ex n being Nat st
( S1[d,X1,X2,n] & $2 = (iter (X2,n)) . d );
A2: for a being object st a in H1(X1,X2) holds
ex b being object st
( b in D & S3[a,b] )
proof
let a be object ; :: thesis: ( a in H1(X1,X2) implies ex b being object st
( b in D & S3[a,b] ) )
assume a in H1(X1,X2) ; :: thesis: ex b being object st
( b in D & S3[a,b] )
then consider d being Element of D such that
A3: d = a and
A4: ex n being Nat st S1[d,X1,X2,n] ;
consider n being Nat such that
A5: S1[d,X1,X2,n] by A4;
take (iter (X2,n)) . d ; :: thesis: ( (iter (X2,n)) . d in D & S3[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: S3[a,(iter (X2,n)) . d]
thus S3[a,(iter (X2,n)) . d] by A3, A5; :: thesis: verum
end;
consider K being Function such that
A7: dom K = H1(X1,X2) and
A8: rng K c= D and
A9: for x being object st x in H1(X1,X2) holds
S3[x,K . x] from FUNCT_1:sch 6(A2);
 take K ; :: thesis: ( K in FPrg D & S2[x1,x2,K] )
H1(X1,X2) c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(X1,X2) or x in D )
assume x in H1(X1,X2) ; :: thesis: x in D
then ex d being Element of D st
( d = x & ex n being Nat st S1[d,X1,X2,n] ) ;
hence x in D ; :: thesis: verum
end;
then K is PartFunc of D,D by A7, A8, RELSET_1:4;
hence K in FPrg D by PARTFUN1:45; :: thesis: S2[x1,x2,K]
thus S2[x1,x2,K] by A7, A9; :: thesis: verum
end;
consider F being Function of [:(Pr D),(FPrg D):],(FPrg D) such that
A10: for x, y being object st x in Pr D & y in FPrg D holds
S2[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)) = H1(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: ( S1[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