let X be set ; :: thesis: for n being Nat
for f being Function of X,()
for g being Function of X,R^1 holds f <#> g is Function of X,()

let n be Nat; :: thesis: for f being Function of X,()
for g being Function of X,R^1 holds f <#> g is Function of X,()

let f be Function of X,(); :: thesis: for g being Function of X,R^1 holds f <#> g is Function of X,()
let g be Function of X,R^1; :: thesis: f <#> g is Function of X,()
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 ;
for x being object st x in X holds
(f <#> g) . x in the carrier of ()
proof
let x be object ; :: thesis: ( x in X implies (f <#> g) . x in the carrier of () )
assume A3: x in X ; :: thesis: (f <#> g) . x in the carrier of ()
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,() ;
(f <#> g) . x = (f . x) (#) (g . x) by ;
hence (f <#> g) . x in the carrier of () ; :: thesis: verum
end;
hence f <#> g is Function of X,() by ; :: thesis: verum