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) )

proof

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 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 A4: x in (dom F) /\ (dom G) by VALUED_1:16;
A5: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17;
then A6: ( x + t in dom F & x - t in dom F ) by A1, Th1, A4;
( x + t in dom G & x - t in dom G ) by A2, Th1, A4, A5;
then A7: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A6, XBOOLE_0:def 4;
(F /" G) . x = (F . x) / (G . x) by VALUED_1:17
.= (F . (x + t)) / (G . x) by A1, A4, A5
.= (F . (x + t)) / (G . (x + t)) by A2, A4, A5
.= (F /" G) . (x + t) by VALUED_1:17 ;
hence ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) by A7, VALUED_1:16; :: thesis: verum

end;

hence F /" G is t -periodic by A3, Th1; :: thesis: verum