let X, Y be non empty set ; :: thesis: for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let Z be set ; :: thesis: for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let f be Function of X,Y; :: thesis: for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let g be PartFunc of Y,Z; :: thesis: for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)
let x be Element of X; :: thesis: ( g is total implies (g /* f) . x = g . (f . x) )
assume g is total ; :: thesis: (g /* f) . x = g . (f . x)
then dom g = Y ;
then rng f c= dom g ;
hence (g /* f) . x = g . (f . x) by Th107; :: thesis: verum