let X be set ; :: thesis: for n being Nat
for r being Real
for f being Function of X,() holds f [+] r is Function of X,()

let n be Nat; :: thesis: for r being Real
for f being Function of X,() holds f [+] r is Function of X,()

let r be Real; :: thesis: for f being Function of X,() holds f [+] r is Function of X,()
let f be Function of X,(); :: thesis: f [+] r is Function of X,()
set h = f [+] r;
dom f = X by FUNCT_2:def 1;
then A1: dom (f [+] r) = X by VALUED_2:def 37;
for x being object st x in X holds
(f [+] r) . x in the carrier of ()
proof
let x be object ; :: thesis: ( x in X implies (f [+] r) . x in the carrier of () )
assume A2: x in X ; :: thesis: (f [+] r) . x in the carrier of ()
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A2;
reconsider f = f as Function of X,() ;
A3: (f . x) + r = (f . x) + r ;
(f [+] r) . x = (f . x) + r by ;
hence (f [+] r) . x in the carrier of () by A3; :: thesis: verum
end;
hence f [+] r is Function of X,() by ; :: thesis: verum