let A be non empty transitive with_units AltCatStr ; :: thesis: (id A) " = id A
set CCA = [:the carrier of A,the carrier of A:];
consider f being ManySortedFunction of the Arrows of A,the Arrows of A * the ObjectMap of (id A) such that
A1: f = the MorphMap of (id A) and
A2: the MorphMap of ((id A) " ) = (f "" ) * (the ObjectMap of (id A) " ) by FUNCTOR0:def 39;
A3: for i being set st i in [:the carrier of A,the carrier of A:] holds
(id the Arrows of A) . i is one-to-one

proof

let i be set ; :: thesis: ( i in [:the carrier of A,the carrier of A:] implies (id the Arrows of A) . i is one-to-one )
assume A4: i in [:the carrier of A,the carrier of A:] ; :: thesis: (id the Arrows of A) . i is one-to-one
id (the Arrows of A . i) is one-to-one ;
hence (id the Arrows of A) . i is one-to-one by A4, MSUALG_3:def 1; :: thesis: verum

end;

the MorphMap of (id A) = id the Arrows of A by FUNCTOR0:def 30;
then A5: the MorphMap of (id A) is "1-1" by A3, MSUALG_3:1;
for i being set st i in [:the carrier of A,the carrier of A:] holds
rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i

proof

dom the Arrows of A = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then A6: (dom the Arrows of A) /\ [:the carrier of A,the carrier of A:] = [:the carrier of A,the carrier of A:] ;
let i be set ; :: thesis: ( i in [:the carrier of A,the carrier of A:] implies rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i )
assume A7: i in [:the carrier of A,the carrier of A:] ; :: thesis: rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i
rng (f . i) = rng ((id the Arrows of A) . i) by A1, FUNCTOR0:def 30
.= rng (id (the Arrows of A . i)) by A7, MSUALG_3:def 1
.= the Arrows of A . i by RELAT_1:71
.= (the Arrows of A * (id [:the carrier of A,the carrier of A:])) . i by A7, A6, FUNCT_1:38
.= (the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def 30 ;
hence rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i ; :: thesis: verum

end;

then A8: f is "onto" by MSUALG_3:def 3;
for i being set st i in [:the carrier of A,the carrier of A:] holds
(f "" ) . i = f . i

proof

let i be set ; :: thesis: ( i in [:the carrier of A,the carrier of A:] implies (f "" ) . i = f . i )
assume A9: i in [:the carrier of A,the carrier of A:] ; :: thesis: (f "" ) . i = f . i
then (f "" ) . i = (the MorphMap of (id A) . i) " by A1, A5, A8, MSUALG_3:def 5
.= ((id the Arrows of A) . i) " by FUNCTOR0:def 30
.= (id (the Arrows of A . i)) " by A9, MSUALG_3:def 1
.= id (the Arrows of A . i) by FUNCT_1:67
.= (id the Arrows of A) . i by A9, MSUALG_3:def 1
.= f . i by A1, FUNCTOR0:def 30 ;
hence (f "" ) . i = f . i ; :: thesis: verum

end;

then A10: f "" = f by PBOOLE:3;
for i being set st i in [:the carrier of A,the carrier of A:] holds
(the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:])) . i = the MorphMap of (id A) . i

proof

dom the MorphMap of (id A) = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then A11: (dom the MorphMap of (id A)) /\ [:the carrier of A,the carrier of A:] = [:the carrier of A,the carrier of A:] ;
let i be set ; :: thesis: ( i in [:the carrier of A,the carrier of A:] implies (the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:])) . i = the MorphMap of (id A) . i )
assume i in [:the carrier of A,the carrier of A:] ; :: thesis: (the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:])) . i = the MorphMap of (id A) . i
hence (the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:])) . i = the MorphMap of (id A) . i by A11, FUNCT_1:38; :: thesis: verum

end;

then A12: the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:]) = the MorphMap of (id A) by PBOOLE:3;
A13: the ObjectMap of ((id A) " ) = the ObjectMap of (id A) " by FUNCTOR0:def 39;
then the ObjectMap of ((id A) " ) = (id [:the carrier of A,the carrier of A:]) " by FUNCTOR0:def 30
.= id [:the carrier of A,the carrier of A:] by FUNCT_1:67
.= the ObjectMap of (id A) by FUNCTOR0:def 30 ;
hence (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def 30; :: thesis: verum