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

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