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

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