take REAL --> the Element of REAL ; :: thesis: REAL --> the Element of REAL is t -periodic
thus REAL --> the Element of REAL is t -periodic by Lm1; :: thesis: verum