let n be Nat; :: thesis: for r being non negative Real
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),() holds f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),()

let r be non negative Real; :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),() holds f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),()
set X = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r));
let f be Function of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(); :: thesis: f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),()
set g = f (-) ;
A1: dom (f (-)) = dom f by VALUED_2:def 34;
A2: dom f = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by FUNCT_2:def 1;
for x being object st x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) holds
(f (-)) . x in the carrier of ()
proof
let x be object ; :: thesis: ( x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) implies (f (-)) . x in the carrier of () )
assume x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; :: thesis: (f (-)) . x in the carrier of ()
then reconsider x = x as Element of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ;
reconsider y = - x as Element of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by Th60;
reconsider f = f as Function of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)),() ;
(f (-)) . x = f . y by ;
hence (f (-)) . x in the carrier of () ; :: thesis: verum
end;
hence f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),() by ; :: thesis: verum