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

for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)

let n be Nat; :: thesis: for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)

let f, g be Function of X,(TOP-REAL n); :: thesis: f <++> g is Function of X,(TOP-REAL n)

set h = f <++> g;

A1: dom f = X by FUNCT_2:def 1;

dom g = X by FUNCT_2:def 1;

then A2: dom (f <++> g) = X by A1, VALUED_2:def 45;

for x being object st x in X holds

(f <++> g) . x in the carrier of (TOP-REAL n)

for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)

let n be Nat; :: thesis: for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)

let f, g be Function of X,(TOP-REAL n); :: thesis: f <++> g is Function of X,(TOP-REAL n)

set h = f <++> g;

A1: dom f = X by FUNCT_2:def 1;

dom g = X by FUNCT_2:def 1;

then A2: dom (f <++> g) = X by A1, VALUED_2:def 45;

for x being object st x in X holds

(f <++> g) . x in the carrier of (TOP-REAL n)

proof

hence
f <++> g is Function of X,(TOP-REAL n)
by A2, FUNCT_2:3; :: thesis: verum
let x be object ; :: thesis: ( x in X implies (f <++> g) . x in the carrier of (TOP-REAL n) )

assume A3: x in X ; :: thesis: (f <++> g) . 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, g = g as Function of X,(TOP-REAL n) ;

A4: (f . x) + (g . x) = (f . x) + (g . x) ;

(f <++> g) . x = (f . x) + (g . x) by A2, VALUED_2:def 45;

hence (f <++> g) . x in the carrier of (TOP-REAL n) by A4; :: thesis: verum

end;assume A3: x in X ; :: thesis: (f <++> g) . 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, g = g as Function of X,(TOP-REAL n) ;

A4: (f . x) + (g . x) = (f . x) + (g . x) ;

(f <++> g) . x = (f . x) + (g . x) by A2, VALUED_2:def 45;

hence (f <++> g) . x in the carrier of (TOP-REAL n) by A4; :: thesis: verum