let UN be Universe; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: h * (g * f) = (h * g) * f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (RingObjects UN) by Th27;
A2: ( h9 * g9 = h * g & dom (h * g) = cod f ) by A1, Lm9, Th30;
A3: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A1, Th30;
then reconsider gf = g9 * f9, hg = h9 * g9 as strict Element of Morphs (RingObjects UN) by Th25;
( g9 * f9 = g * f & dom h = cod (g * f) ) by A1, Lm9, Th30;
then h * (g * f) = h9 * gf by Th30
.= hg * f9 by A3, Th13
.= (h * g) * f by A2, Th30 ;
hence h * (g * f) = (h * g) * f ; :: thesis: verum