let C be non empty with_identities CategoryStr ; :: thesis: for f, f1 being morphism of C
for o being Object of C st f = o holds
( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )
let f, f1 be morphism of C; :: thesis: for o being Object of C st f = o holds
( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )
let o be Object of C; :: thesis: ( f = o implies ( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f ) )
assume A1: f = o ; :: thesis: ( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )
A2: f is identity by A1, Th22;
consider c being morphism of C such that
A3: ( c |> f & c is left_identity ) by Def12, Def6;
A4: c = c (*) f by A2, A3, Def5
.= f by A3 ;
thus ( f |> f1 implies f (*) f1 = f1 ) by A2, Def4; :: thesis: ( ( f1 |> f implies f1 (*) f = f1 ) & f |> f )
thus ( f1 |> f implies f1 (*) f = f1 ) by A2, Def5; :: thesis: f |> f
thus f |> f by A3, A4; :: thesis: verum