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