let t, a be real number ; :: 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 number 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 number ; :: 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) ) by FUNCOP_1:19; :: 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:13
.= (REAL --> a) . (x + t) by A1, FUNCOP_1:13 ; :: thesis: verum