let t, r be Real; :: thesis: for F being real-valued Function st F is t -periodic holds
r (#) F is t -periodic

let F be real-valued Function; :: thesis: ( F is t -periodic implies r (#) F is t -periodic )
assume A1: F is t -periodic ; :: thesis: r (#) F is t -periodic
then A2: ( t <> 0 & ( for x being Real st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
for x being Real st x in dom (r (#) F) holds
( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) )
proof
let x be Real; :: thesis: ( x in dom (r (#) F) implies ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) )
assume A3: x in dom (r (#) F) ; :: thesis: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) )
then A4: x in dom F by VALUED_1:def 5;
then A5: ( x + t in dom F & x - t in dom F ) by ;
then A6: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) ) by VALUED_1:def 5;
(r (#) F) . x = r * (F . x) by
.= r * (F . (x + t)) by A1, A4
.= (r (#) F) . (x + t) by ;
hence ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) by ; :: thesis: verum
end;
hence r (#) F is t -periodic by ; :: thesis: verum