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):] ;
A1: for n being 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 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) ;
h * g is Element of bool [:(field f),(field f):] ;
hence ex y being Element of bool [:(field f),(field f):] st S₁[n,x,y] ; :: thesis: verum

end;

consider p being sequence of (bool [:(field f),(field f):]) such that
A2: ( p . 0 = ID & ( for n being Nat holds S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
p . n9 is Relation of (field f),(field f) ;
hence ex b₁ being Relation ex p being sequence of (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; :: thesis: verum