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