let C be CategoryStr ; :: thesis: 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; :: thesis: 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 #); :: thesis: ( f1 = g1 & f2 = g2 & f1 |> f2 implies f1 (*) f2 = g1 (*) g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; :: thesis: ( not f1 |> f2 or f1 (*) f2 = g1 (*) g2 )
assume A2: f1 |> f2 ; :: thesis: 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 ; :: thesis: verum