let A be symmetrical Subset of REAL; :: thesis: signum is_odd_on A
A1: dom signum = REAL by FUNCT_2:def 1;
then A2: dom (signum | A) = A by RELAT_1:62;
for x being Real st x in dom (signum | A) & - x in dom (signum | A) holds
(signum | A) . (- x) = - ((signum | A) . x)
proof
let x be Real; :: thesis: ( x in dom (signum | A) & - x in dom (signum | A) implies (signum | A) . (- x) = - ((signum | A) . x) )
assume that
A3: x in dom (signum | A) and
A4: - x in dom (signum | A) ; :: thesis: (signum | A) . (- x) = - ((signum | A) . x)
reconsider x = x as Element of REAL by XREAL_0:def 1;
(signum | A) . (- x) = (signum | A) /. (- x) by A4, PARTFUN1:def 6
.= signum /. (- x) by A1, A4, PARTFUN2:17
.= - (signum /. x) by Th59
.= - ((signum | A) /. x) by A1, A3, PARTFUN2:17
.= - ((signum | A) . x) by A3, PARTFUN1:def 6 ;
hence (signum | A) . (- x) = - ((signum | A) . x) ; :: thesis: verum
end;
then ( signum | A is with_symmetrical_domain & signum | A is quasi_odd ) by A2;
hence signum is_odd_on A by A1; :: thesis: verum