take REAL --> the Real ; :: thesis: REAL --> the Real is t -periodic
thus REAL --> the Real is t -periodic by Lm38; :: thesis: verum