let t, a be Real; :: thesis: ( t <> 0 implies REAL --> a is t -periodic )
set F = REAL --> a;
assume t <> 0 ; :: thesis: REAL --> a is t -periodic
hence t <> 0 ; :: according to FUNCT_9:def 1 :: thesis: for x being Real holds
( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) )
let x be Real; :: thesis: ( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) )
A1: ( x in REAL & x + t in REAL ) by XREAL_0:def 1;
hence ( x in dom (REAL --> a) iff x + t in dom (REAL --> a) ) ; :: thesis: ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) )
assume x in dom (REAL --> a) ; :: thesis: (REAL --> a) . x = (REAL --> a) . (x + t)
thus (REAL --> a) . x = a by A1, FUNCOP_1:7
.= (REAL --> a) . (x + t) by A1, FUNCOP_1:7 ; :: thesis: verum