let C be discrete CategoryStr ; :: thesis: for f1, f2 being morphism of C st f1 |> f2 holds
( f1 = f2 & f1 (*) f2 = f2 )
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( f1 = f2 & f1 (*) f2 = f2 ) )
assume A1: f1 |> f2 ; :: thesis: ( f1 = f2 & f1 (*) f2 = f2 )
f2 is identity by Def15;
then A2: f1 (*) f2 = f1 by Def5, A1;
f1 is identity by Def15;
hence ( f1 = f2 & f1 (*) f2 = f2 ) by A2, A1, Def4; :: thesis: verum