let A be symmetrical Subset of REAL ; :: thesis: sin is_odd_on A
A1: dom (sin | A) = A by RELAT_1:91, SIN_COS:27;
for x being Real st x in dom (sin | A) & - x in dom (sin | A) holds
(sin | A) . (- x) = - ((sin | A) . x)

proof

let x be Real; :: thesis: ( x in dom (sin | A) & - x in dom (sin | A) implies (sin | A) . (- x) = - ((sin | A) . x) )
assume that
A2: x in dom (sin | A) and
A3: - x in dom (sin | A) ; :: thesis: (sin | A) . (- x) = - ((sin | A) . x)
(sin | A) . (- x) = (sin | A) /. (- x) by A3, PARTFUN1:def 8
.= sin /. (- x) by A1, A3, PARTFUN2:35, SIN_COS:27
.= - (sin /. x) by SIN_COS:33
.= - ((sin | A) /. x) by A1, A2, PARTFUN2:35, SIN_COS:27
.= - ((sin | A) . x) by A2, PARTFUN1:def 8 ;
hence (sin | A) . (- x) = - ((sin | A) . x) ; :: thesis: verum

end;

then ( sin | A is with_symmetrical_domain & sin | A is quasi_odd ) by A1, Def2, Def6;
hence sin is_odd_on A by Def8, SIN_COS:27; :: thesis: verum