take REAL --> t ; :: thesis: ( REAL --> t is t -periodic & REAL --> t is real-valued )
thus ( REAL --> t is t -periodic & REAL --> t is real-valued ) ; :: thesis: verum