theorem :: FINTOPO3:47

for T being non empty RelStr
for x being Element of T holds U_FT (x,0) = U_FT x by Def6;