let C be CategoryStr ; :: thesis: for f being morphism of C
for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds
( f is right_identity iff g is right_identity )
let f be morphism of C; :: thesis: for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds
( f is right_identity iff g is right_identity )
let g be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis: ( f = g implies ( f is right_identity iff g is right_identity ) )
assume A1: f = g ; :: thesis: ( f is right_identity iff g is right_identity )

hereby :: thesis: ( g is right_identity implies f is right_identity )

assume A2: f is right_identity ; :: thesis: g is right_identity
for g1 being morphism of CategoryStr(# the carrier of C, the composition of C #) st g1 |> g holds
g1 (*) g = g1

proof

let g1 be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis: ( g1 |> g implies g1 (*) g = g1 )
reconsider f1 = g1 as morphism of C ;
assume g1 |> g ; :: thesis: g1 (*) g = g1
then A3: f1 |> f by A1;
then f1 (*) f = f1 by A2;
hence g1 (*) g = g1 by A1, A3, Th11; :: thesis: verum

end;

hence g is right_identity ; :: thesis: verum

end;

assume A4: g is right_identity ; :: thesis: f is right_identity
for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1

proof

let f1 be morphism of C; :: thesis: ( f1 |> f implies f1 (*) f = f1 )
reconsider g1 = f1 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume A5: f1 |> f ; :: thesis: f1 (*) f = f1
then g1 |> g by A1;
then g1 (*) g = g1 by A4;
hence f1 (*) f = f1 by A1, A5, Th11; :: thesis: verum

end;

hence f is right_identity ; :: thesis: verum