set F = id C;
A1: id C = id the carrier of C by STRUCT_0:def 4;
for f1, f2 being morphism of C st f1 |> f2 holds
( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) )
proof
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) ) )
assume A2: f1 |> f2 ; :: thesis: ( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) )
per cases ( not C is empty or C is empty ) ;
suppose A3: not C is empty ; :: thesis: ( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) )
reconsider x1 = f1, x2 = f2, x3 = f1 (*) f2 as object ;
A4: (id C) . f1 = (id C) . x1 by A3, Def21
.= f1 by A1 ;
A5: (id C) . f2 = (id C) . x2 by A3, Def21
.= f2 by A1 ;
A6: (id C) . (f1 (*) f2) = (id C) . x3 by A3, Def21
.= f1 (*) f2 by A1 ;
thus (id C) . f1 |> (id C) . f2 by A4, A5, A2; :: thesis: (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2)
thus (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) by A4, A6, A5; :: thesis: verum
end;
suppose C is empty ; :: thesis: ( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) )
hence ( (id C) . f1 |> (id C) . f2 & (id C) . (f1 (*) f2) = ((id C) . f1) (*) ((id C) . f2) ) by A2; :: thesis: verum
end;
end;
end;
then A7: id C is multiplicative ;
for f being morphism of C st f is identity holds
(id C) . f is identity
proof
let f be morphism of C; :: thesis: ( f is identity implies (id C) . f is identity )
assume A8: f is identity ; :: thesis: (id C) . f is identity
per cases ( not C is empty or C is empty ) ;
suppose A9: not C is empty ; :: thesis: (id C) . f is identity
reconsider x = f as object ;
(id C) . f = (id C) . x by A9, Def21
.= f by A1 ;
hence (id C) . f is identity by A8; :: thesis: verum
end;
end;
end;
hence id C is covariant by A7, Def22; :: thesis: verum