let n be Nat; :: thesis: for r being real non negative number
for f being Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n) holds f (-) is Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n)
let r be real non negative number ; :: thesis: for f being Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n) holds f (-) is Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n)
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),(TOP-REAL n); :: thesis: f (-) is Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n)
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 set st x in the carrier of (Tcircle (0. (TOP-REAL (n + 1))),r) holds
(f (-) ) . x in the carrier of (TOP-REAL n)

proof

let x be set ; :: thesis: ( x in the carrier of (Tcircle (0. (TOP-REAL (n + 1))),r) implies (f (-) ) . x in the carrier of (TOP-REAL n) )
assume x in the carrier of (Tcircle (0. (TOP-REAL (n + 1))),r) ; :: thesis: (f (-) ) . x in the carrier of (TOP-REAL n)
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),(TOP-REAL n) ;
(f (-) ) . x = f . y by A1, A2, VALUED_2:def 34;
hence (f (-) ) . x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

hence f (-) is Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n) by A1, A2, FUNCT_2:5; :: thesis: verum