let X be set ; :: thesis: for n being Nat
for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)
let n be Nat; :: thesis: for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)
let f be Function of X,(TOP-REAL n); :: thesis: <-> f is Function of X,(TOP-REAL n)
set g = <-> f;
A1: dom (<-> f) = dom f by VALUED_2:def 33;
A2: dom f = X by FUNCT_2:def 1;
for x being set st x in X holds
(<-> f) . x in the carrier of (TOP-REAL n)

proof

let x be set ; :: thesis: ( x in X implies (<-> f) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; :: thesis: (<-> f) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
A4: - (f . x) = - (f . x) ;
(<-> f) . x = - (f . x) by A1, A2, VALUED_2:def 33;
hence (<-> f) . x in the carrier of (TOP-REAL n) by A4; :: thesis: verum

end;

hence <-> f is Function of X,(TOP-REAL n) by A1, A2, FUNCT_2:5; :: thesis: verum