let C be non empty category; :: thesis: for f1 being morphism of C
for a1 being Morphism of (Alter C) st a1 = f1 holds
( dom f1 = dom a1 & cod f1 = cod a1 )
let f1 be morphism of C; :: thesis: for a1 being Morphism of (Alter C) st a1 = f1 holds
( dom f1 = dom a1 & cod f1 = cod a1 )
let a1 be Morphism of (Alter C); :: thesis: ( a1 = f1 implies ( dom f1 = dom a1 & cod f1 = cod a1 ) )
assume A1: a1 = f1 ; :: thesis: ( dom f1 = dom a1 & cod f1 = cod a1 )
thus dom f1 = the Source of (Alter C) . a1 by A1, Def30
.= dom a1 by GRAPH_1:def 3 ; :: thesis: cod f1 = cod a1
thus cod f1 = the Target of (Alter C) . a1 by A1, Def31
.= cod a1 by GRAPH_1:def 4 ; :: thesis: verum