let t be Real; :: thesis: for F being real-valued Function st F is t -periodic holds

|.F.| is t -periodic

let F be real-valued Function; :: thesis: ( F is t -periodic implies |.F.| is t -periodic )

assume A1: F is t -periodic ; :: thesis: |.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 |.F.| holds

( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )

|.F.| is t -periodic

let F be real-valued Function; :: thesis: ( F is t -periodic implies |.F.| is t -periodic )

assume A1: F is t -periodic ; :: thesis: |.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 |.F.| holds

( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )

proof

hence
|.F.| is t -periodic
by A2, Th1; :: thesis: verum
let x be Real; :: thesis: ( x in dom |.F.| implies ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) )

assume A3: x in dom |.F.| ; :: thesis: ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )

then A4: x in dom F by VALUED_1:def 11;

then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;

then A6: ( x + t in dom |.F.| & x - t in dom |.F.| ) by VALUED_1:def 11;

|.F.| . x = |.(F . x).| by A3, VALUED_1:def 11

.= |.(F . (x + t)).| by A1, A4

.= |.F.| . (x + t) by A6, VALUED_1:def 11 ;

hence ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) by A5, VALUED_1:def 11; :: thesis: verum

end;assume A3: x in dom |.F.| ; :: thesis: ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )

then A4: x in dom F by VALUED_1:def 11;

then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;

then A6: ( x + t in dom |.F.| & x - t in dom |.F.| ) by VALUED_1:def 11;

|.F.| . x = |.(F . x).| by A3, VALUED_1:def 11

.= |.(F . (x + t)).| by A1, A4

.= |.F.| . (x + t) by A6, VALUED_1:def 11 ;

hence ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) by A5, VALUED_1:def 11; :: thesis: verum