let C be non empty category; :: thesis: for a1, a2 being Morphism of (Alter C)
for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds
a1 (*) a2 = f1 (*) f2
let a1, a2 be Morphism of (Alter C); :: thesis: for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds
a1 (*) a2 = f1 (*) f2
let f1, f2 be morphism of C; :: thesis: ( a1 = f1 & a2 = f2 & f1 |> f2 implies a1 (*) a2 = f1 (*) f2 )
assume A1: ( a1 = f1 & a2 = f2 ) ; :: thesis: ( not f1 |> f2 or a1 (*) a2 = f1 (*) f2 )
assume A2: f1 |> f2 ; :: thesis: a1 (*) a2 = f1 (*) f2
thus a1 (*) a2 = the Comp of (Alter C) . (a1,a2) by A1, A2, CAT_1:def 1
.= f1 (*) f2 by A1, A2, Def3 ; :: thesis: verum