let A be Category; :: thesis: for a1, a2 being Morphism of A
for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds
a1 (*) a2 = f1 (*) f2
let a1, a2 be Morphism of A; :: thesis: for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds
a1 (*) a2 = f1 (*) f2
let f1, f2 be morphism of (alter A); :: thesis: ( a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A implies a1 (*) a2 = f1 (*) f2 )
assume A1: ( a1 = f1 & a2 = f2 ) ; :: thesis: ( not [a1,a2] in dom the Comp of A or a1 (*) a2 = f1 (*) f2 )
assume A2: [a1,a2] in dom the Comp of A ; :: thesis: a1 (*) a2 = f1 (*) f2
thus a1 (*) a2 = the composition of (alter A) . (f1,f2) by A1, A2, CAT_1:def 1
.= f1 (*) f2 by A2, A1, Def2, Def3 ; :: thesis: verum