:: deftheorem defines Fdfl FINTOPO3:def 9 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fdfl (A,n) = (Fdfl A) . n;