let n be Nat; :: thesis: for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds
<*p,(iter (f,n)),p*> is SFHT of D
let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds
<*p,(iter (f,n)),p*> is SFHT of D
let f be BinominativeFunction of D; :: thesis: for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds
<*p,(iter (f,n)),p*> is SFHT of D
let p be PartialPredicate of D; :: thesis: ( f coincides_with p & <*p,f,p*> is SFHT of D implies <*p,(iter (f,n)),p*> is SFHT of D )
assume that
A1: f coincides_with p and
A2: <*p,f,p*> is SFHT of D ; :: thesis: <*p,(iter (f,n)),p*> is SFHT of D
defpred S₁[ Nat] means <*p,(iter (f,$1)),p*> is SFHT of D;
iter (f,0) = id (field f) by FUNCT_7:68;
then A3: S₁[ 0 ] by Th14;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
set i = iter (f,(k + 1));
A6: iter (f,(k + 1)) is BinominativeFunction of D by FUNCT_7:86;
for d being Element of D st d in dom p & p . d = TRUE & d in dom (iter (f,(k + 1))) & (iter (f,(k + 1))) . d in dom p holds
p . ((iter (f,(k + 1))) . d) = TRUE

proof

let d be Element of D; :: thesis: ( d in dom p & p . d = TRUE & d in dom (iter (f,(k + 1))) & (iter (f,(k + 1))) . d in dom p implies p . ((iter (f,(k + 1))) . d) = TRUE )
assume that
A7: d in dom p and
A8: p . d = TRUE and
A9: d in dom (iter (f,(k + 1))) and
A10: (iter (f,(k + 1))) . d in dom p ; :: thesis: p . ((iter (f,(k + 1))) . d) = TRUE
set j = iter (f,k);
A11: iter (f,k) is BinominativeFunction of D by FUNCT_7:86;
A12: iter (f,(k + 1)) = (iter (f,k)) * f by FUNCT_7:69;
then A13: (iter (f,(k + 1))) . d = (iter (f,k)) . (f . d) by A9, FUNCT_1:12;
A14: d in dom f by A9, A12, FUNCT_1:11;
A15: f . d in dom (iter (f,k)) by A9, A12, FUNCT_1:11;
A16: f . d in dom p by A1, A7;
p . (f . d) = TRUE by A1, A2, A7, A8, A14, Th11;
hence p . ((iter (f,(k + 1))) . d) = TRUE by A5, A10, A11, A13, A15, A16, Th11; :: thesis: verum

end;

then <*p,(iter (f,(k + 1))),p*> in SFHTs D by A6;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence <*p,(iter (f,n)),p*> is SFHT of D ; :: thesis: verum