let X, Y be set ; :: thesis: for x being object
for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
let x be object ; :: thesis: for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
let f be Function of X,Y; :: thesis: for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)
let g be Function; :: thesis: ( Y <> {} & x in X implies (g * f) . x = g . (f . x) )
assume Y <> {} ; :: thesis: ( not x in X or (g * f) . x = g . (f . x) )
then X = dom f by Def1;
hence ( not x in X or (g * f) . x = g . (f . x) ) by FUNCT_1:13; :: thesis: verum