reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat, Relation, set ] means $3 = f * $2;
set FX = bool [:(field f),(field f):];
reconsider ID = id (field f) as Element of bool [:(field f),(field f):] by PARTFUN1:45;
A1: for n being Element of NAT
for x being Element of bool [:(field f),(field f):] ex y being Element of bool [:(field f),(field f):] st S₁[n,x,y]

proof

( dom f c= field f & rng f c= field f ) by XBOOLE_1:7;
then reconsider h = f as Relation of (field f),(field f) by RELSET_1:4;
let n be Element of NAT ; :: thesis: for x being Element of bool [:(field f),(field f):] ex y being Element of bool [:(field f),(field f):] st S₁[n,x,y]
let x be Element of bool [:(field f),(field f):]; :: thesis: ex y being Element of bool [:(field f),(field f):] st S₁[n,x,y]
reconsider g = x as Relation of (field f),(field f) by PARTFUN1:46;
h * g is Element of bool [:(field f),(field f):] by PARTFUN1:45;
hence ex y being Element of bool [:(field f),(field f):] st S₁[n,x,y] ; :: thesis: verum

end;

consider p being Function of NAT,(bool [:(field f),(field f):]) such that
A2: ( p . 0 = ID & ( for n being Element of NAT holds S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
A3: for n being Nat holds S₁[n,p . n,p . (n + 1)]

proof

let n be Nat; :: thesis: S₁[n,p . n,p . (n + 1)]
n in NAT by ORDINAL1:def 12;
hence S₁[n,p . n,p . (n + 1)] by A2; :: thesis: verum

end;

p . n9 is Relation of (field f),(field f) by PARTFUN1:46;
hence ex b₁ being Relation ex p being Function of NAT,(bool [:(field f),(field f):]) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) by A2, A3; :: thesis: verum