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 left_identity iff g is left_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 left_identity iff g is left_identity )
let g be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis: ( f = g implies ( f is left_identity iff g is left_identity ) )
assume A1: f = g ; :: thesis: ( f is left_identity iff g is left_identity )
hereby :: thesis: ( g is left_identity implies f is left_identity )
assume A2: f is left_identity ; :: thesis: g is left_identity
for g1 being morphism of CategoryStr(# the carrier of C, the composition of C #) st g |> g1 holds
g (*) g1 = g1
proof
let g1 be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis: ( g |> g1 implies g (*) g1 = g1 )
reconsider f1 = g1 as morphism of C ;
assume g |> g1 ; :: thesis: g (*) g1 = g1
then A3: f |> f1 by A1;
then f (*) f1 = f1 by A2;
hence g (*) g1 = g1 by A1, A3, Th11; :: thesis: verum
end;
hence g is left_identity ; :: thesis: verum
end;
assume A4: g is left_identity ; :: thesis: f is left_identity
for f2 being morphism of C st f |> f2 holds
f (*) f2 = f2
proof
let f2 be morphism of C; :: thesis: ( f |> f2 implies f (*) f2 = f2 )
reconsider g2 = f2 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume A5: f |> f2 ; :: thesis: f (*) f2 = f2
then g |> g2 by A1;
then g (*) g2 = g2 by A4;
hence f (*) f2 = f2 by A1, A5, Th11; :: thesis: verum
end;
hence f is left_identity ; :: thesis: verum