let R be Ring; :: thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
let V be LeftMod_DOMAIN of R; :: thesis: for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
let g, f be Element of Morphs V; :: thesis: ( [g,f] in dom (comp V) iff dom g = cod f )
( dom g = dom' g & cod f = cod' f ) ;
hence ( [g,f] in dom (comp V) iff dom g = cod f ) by Def13; :: thesis: verum