let t be real number ; :: thesis: for F being real-valued Function st F is t -periodic holds
F ^2 is t -periodic
let F be real-valued Function; :: thesis: ( F is t -periodic implies F ^2 is t -periodic )
assume A1: F is t -periodic ; :: thesis: F ^2 is t -periodic
A3: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1;
for x being real number st x in dom (F ^2 ) holds
( x + t in dom (F ^2 ) & x - t in dom (F ^2 ) & (F ^2 ) . x = (F ^2 ) . (x + t) )

proof

let x be real number ; :: thesis: ( x in dom (F ^2 ) implies ( x + t in dom (F ^2 ) & x - t in dom (F ^2 ) & (F ^2 ) . x = (F ^2 ) . (x + t) ) )
assume x in dom (F ^2 ) ; :: thesis: ( x + t in dom (F ^2 ) & x - t in dom (F ^2 ) & (F ^2 ) . x = (F ^2 ) . (x + t) )
then A5: x in dom F by VALUED_1:11;
then A6: ( x + t in dom F & x - t in dom F ) by A1, Th1;
(F ^2 ) . x = (F . x) ^2 by VALUED_1:11
.= (F . (x + t)) ^2 by A1, Th1, A5
.= (F ^2 ) . (x + t) by VALUED_1:11 ;
hence ( x + t in dom (F ^2 ) & x - t in dom (F ^2 ) & (F ^2 ) . x = (F ^2 ) . (x + t) ) by A6, VALUED_1:11; :: thesis: verum

end;

hence F ^2 is t -periodic by A3, Th1; :: thesis: verum