let t be Real; for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F (#) G is t -periodic
let F, G be real-valued Function; ( F is t -periodic & G is t -periodic implies F (#) G is t -periodic )
assume that
A1:
F is t -periodic
and
A2:
G is t -periodic
; F (#) G is t -periodic
A3:
( 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 A1, Th1;
for x being Real st x in dom (F (#) G) holds
( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) )
proof
let x be
Real;
( x in dom (F (#) G) implies ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) )
assume A4:
x in dom (F (#) G)
;
( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) )
then A5:
x in (dom F) /\ (dom G)
by VALUED_1:def 4;
A6:
(
(dom F) /\ (dom G) c= dom F &
(dom F) /\ (dom G) c= dom G )
by XBOOLE_1:17;
then A7:
(
x + t in dom F &
x - t in dom F )
by A1, Th1, A5;
(
x + t in dom G &
x - t in dom G )
by A2, Th1, A5, A6;
then A8:
(
x + t in (dom F) /\ (dom G) &
x - t in (dom F) /\ (dom G) )
by A7, XBOOLE_0:def 4;
then A9:
(
x + t in dom (F (#) G) &
x - t in dom (F (#) G) )
by VALUED_1:def 4;
(F (#) G) . x =
(F . x) * (G . x)
by A4, VALUED_1:def 4
.=
(F . (x + t)) * (G . x)
by A1, A5, A6
.=
(F . (x + t)) * (G . (x + t))
by A2, A5, A6
.=
(F (#) G) . (x + t)
by A9, VALUED_1:def 4
;
hence
(
x + t in dom (F (#) G) &
x - t in dom (F (#) G) &
(F (#) G) . x = (F (#) G) . (x + t) )
by A8, VALUED_1:def 4;
verum
end;
hence
F (#) G is t -periodic
by A3, Th1; verum