take 1 ; :: according to FUNCT_9:def 2 :: thesis: REAL --> a is 1 -periodic
thus REAL --> a is 1 -periodic by Lm1; :: thesis: verum