let C be non empty category; 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); 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; ( a1 = f1 & a2 = f2 & f1 |> f2 implies a1 (*) a2 = f1 (*) f2 )
assume A1:
( a1 = f1 & a2 = f2 )
; ( not f1 |> f2 or a1 (*) a2 = f1 (*) f2 )
assume A2:
f1 |> f2
; 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
; verum