let A be symmetrical Subset of REAL ; :: thesis: sinh is_odd_on A
A1: dom sinh = REAL by FUNCT_2:def 1;
then A2: dom (sinh | A) = A by RELAT_1:91;
for x being Real st x in dom (sinh | A) & - x in dom (sinh | A) holds
(sinh | A) . (- x) = - ((sinh | A) . x)

proof

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

end;

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