let n be Nat; :: thesis: for r being non negative Real

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 non negative Real; :: 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 object st x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) holds

(f (-)) . x in the carrier of (TOP-REAL n)

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 non negative Real; :: 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 object st x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) holds

(f (-)) . x in the carrier of (TOP-REAL n)

proof

hence
f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n)
by A1, A2, FUNCT_2:3; :: thesis: verum
let x be object ; :: 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;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