let UN be Universe; for f, g, h being Morphism of (RingCat UN) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
set X = Morphs (RingObjects UN);
let f, g, h be Morphism of (RingCat UN); ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A1:
( dom h = cod g & dom g = cod f )
; h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (RingObjects UN) by Th22;
A2:
( h9 * g9 = h (*) g & dom (h (*) g) = cod f )
by A1, Lm9, Th23;
A3:
( dom h9 = cod g9 & dom g9 = cod f9 )
by A1, Th23;
then reconsider gf = g9 * f9, hg = h9 * g9 as strict Element of Morphs (RingObjects UN) by Th20;
( g9 * f9 = g (*) f & dom h = cod (g (*) f) )
by A1, Lm9, Th23;
then h (*) (g (*) f) =
h9 * gf
by Th23
.=
hg * f9
by A3, Th10
.=
(h (*) g) (*) f
by A2, Th23
;
hence
h (*) (g (*) f) = (h (*) g) (*) f
; verum