let C be CategoryStr ; for f1, f2 being morphism of C
for g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g1 (*) g2
let f1, f2 be morphism of C; for g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st f1 = g1 & f2 = g2 & f1 |> f2 holds
f1 (*) f2 = g1 (*) g2
let g1, g2 be morphism of CategoryStr(# the carrier of C, the composition of C #); ( f1 = g1 & f2 = g2 & f1 |> f2 implies f1 (*) f2 = g1 (*) g2 )
assume A1:
( f1 = g1 & f2 = g2 )
; ( not f1 |> f2 or f1 (*) f2 = g1 (*) g2 )
assume A2:
f1 |> f2
; f1 (*) f2 = g1 (*) g2
then A3:
g1 |> g2
by A1;
thus f1 (*) f2 =
the composition of C . (f1,f2)
by A2, Def3
.=
g1 (*) g2
by A1, A3, Def3
; verum