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