let T be non empty RelStr ; :: thesis: for A being Subset of T
for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) `
let A be Subset of T; :: thesis: for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) `
defpred S₁[ Element of NAT ] means (Fdfl A) . $1 = ((Finf (A `)) . $1) ` ;
let n be Element of NAT ; :: thesis: Fdfl (A,n) = (Finf ((A `),n)) `
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]
(Fdfl A) . (k + 1) = (Fdfl (A,k)) ^d by Def8;
then (Fdfl A) . (k + 1) = ((((Fdfl A) . k) `) ^f) ` by Th4
.= ((Finf (A `)) . (k + 1)) ` by A2, Def6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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