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) ` ;
A1: for n being Element of NAT holds S₁[n]

proof

A2: S₁[ 0 ]

proof

((Finf (A ` )) . 0 ) ` = (A ` ) ` by Def6
.= A ;
hence S₁[ 0 ] by Def8; :: thesis: verum

end;

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: (Fdfl A) . (k + 1) = (Fdfl A,k) ^d by Def8;
(Fdfl A) . (k + 1) = ((((Fdfl A) . k) ` ) ^f ) ` by A5, Th4
.= ((Finf (A ` )) . (k + 1)) ` by A4, Def6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence for n being Element of NAT holds S₁[n] ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: Fdfl A,n = (Finf (A ` ),n) `
thus Fdfl A,n = (Finf (A ` ),n) ` by A1; :: thesis: verum