theorem :: FINTOPO3:48

for T being non empty RelStr
for x being Element of T
for n being Nat holds U_FT (x,(n + 1)) = (U_FT (x,n)) ^f by Def6;