let C be composable with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C st f1 |> f2 & f1 is identity & f2 is identity holds
f1 = f2
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 & f1 is identity & f2 is identity implies f1 = f2 )
assume A1: f1 |> f2 ; :: thesis: ( not f1 is identity or not f2 is identity or f1 = f2 )
assume A2: f1 is identity ; :: thesis: ( not f2 is identity or f1 = f2 )
assume f2 is identity ; :: thesis: f1 = f2
hence f1 = f1 (*) f2 by A1, CAT_6:def 5, CAT_6:def 14
.= f2 by A1, A2, CAT_6:def 4, CAT_6:def 14 ;
:: thesis: verum