let T be non empty RelStr ; :: thesis: for A being Subset of T
for n being Element of NAT holds (Fint (A ` ),n) ` = Fcl A,n
let A be Subset of T; :: thesis: for n being Element of NAT holds (Fint (A ` ),n) ` = Fcl A,n
defpred S₁[ Element of NAT ] means (Fint (A ` ),$1) ` = Fcl A,$1;
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
Fcl A,(k + 1) = (Fcl A,k) ^b by Def2
.= ((((Fint (A ` ),k) ` ) ` ) ^i ) ` by A2, FIN_TOPO:22
.= (Fint (A ` ),(k + 1)) ` by Def4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Fint (A ` ),0 ) ` = (A ` ) ` by Def4
.= Fcl A,0 by Def2 ;
then A3: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence for n being Element of NAT holds (Fint (A ` ),n) ` = Fcl A,n ; :: thesis: verum