let X be set ; :: thesis: for n being Nat

for r being Real

for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

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

for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

let r be Real; :: thesis: for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

let f be Function of X,(TOP-REAL n); :: thesis: f [#] r is Function of X,(TOP-REAL n)

set h = f [#] r;

dom f = X by FUNCT_2:def 1;

then A1: dom (f [#] r) = X by VALUED_2:def 39;

for x being object st x in X holds

(f [#] r) . x in the carrier of (TOP-REAL n)

for r being Real

for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

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

for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

let r be Real; :: thesis: for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)

let f be Function of X,(TOP-REAL n); :: thesis: f [#] r is Function of X,(TOP-REAL n)

set h = f [#] r;

dom f = X by FUNCT_2:def 1;

then A1: dom (f [#] r) = X by VALUED_2:def 39;

for x being object st x in X holds

(f [#] r) . x in the carrier of (TOP-REAL n)

proof

hence
f [#] r is Function of X,(TOP-REAL n)
by A1, FUNCT_2:3; :: thesis: verum
let x be object ; :: thesis: ( x in X implies (f [#] r) . x in the carrier of (TOP-REAL n) )

assume A2: x in X ; :: thesis: (f [#] r) . x in the carrier of (TOP-REAL n)

then reconsider X = X as non empty set ;

reconsider x = x as Element of X by A2;

reconsider f = f as Function of X,(TOP-REAL n) ;

A3: (f . x) (#) r = (f . x) (#) r ;

(f [#] r) . x = (f . x) (#) r by A1, VALUED_2:def 39;

hence (f [#] r) . x in the carrier of (TOP-REAL n) by A3; :: thesis: verum

end;assume A2: x in X ; :: thesis: (f [#] r) . x in the carrier of (TOP-REAL n)

then reconsider X = X as non empty set ;

reconsider x = x as Element of X by A2;

reconsider f = f as Function of X,(TOP-REAL n) ;

A3: (f . x) (#) r = (f . x) (#) r ;

(f [#] r) . x = (f . x) (#) r by A1, VALUED_2:def 39;

hence (f [#] r) . x in the carrier of (TOP-REAL n) by A3; :: thesis: verum