let t be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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) )

F + G is t -periodic

let F, G be real-valued Function; :: thesis: ( 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 ; :: thesis: 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

hence
F + G is t -periodic
by A3, Th1; :: thesis: verum
let x be Real; :: thesis: ( 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) ; :: thesis: ( 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 1;

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 1;

(F + G) . x = (F . x) + (G . x) by A4, VALUED_1:def 1

.= (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 1 ;

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 1; :: thesis: verum

end;assume A4: x in dom (F + G) ; :: thesis: ( 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 1;

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 1;

(F + G) . x = (F . x) + (G . x) by A4, VALUED_1:def 1

.= (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 1 ;

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 1; :: thesis: verum