let t be Real; :: thesis: for F being real-valued Function st F is t -periodic holds
for x being Real st x in dom F holds
F . x = F . (x - t)
let F be real-valued Function; :: thesis: ( F is t -periodic implies for x being Real st x in dom F holds
F . x = F . (x - t) )
assume A1: F is t -periodic ; :: thesis: for x being Real st x in dom F holds
F . x = F . (x - t)
let x be Real; :: thesis: ( x in dom F implies F . x = F . (x - t) )
assume x in dom F ; :: thesis: F . x = F . (x - t)
then ( x + t in dom F & x - t in dom F ) by A1, Th1;
then F . (x - t) = F . ((x - t) + t) by A1
.= F . x ;
hence F . x = F . (x - t) ; :: thesis: verum