let A be non empty transitive with_units AltCatStr ; :: thesis: (id A) " = id A
set CCA = [:the carrier of A,the carrier of A:];
A1: the ObjectMap of ((id A) " ) = the ObjectMap of (id A) " by FUNCTOR0:def 39;
consider f being ManySortedFunction of the Arrows of A,the Arrows of A * the ObjectMap of (id A) such that
A2: ( f = the MorphMap of (id A) & the MorphMap of ((id A) " ) = (f "" ) * (the ObjectMap of (id A) " ) ) by FUNCTOR0:def 39;
A3: the ObjectMap of ((id A) " ) = (id [:the carrier of A,the carrier of A:]) " by A1, 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 ;
A4: the MorphMap of (id A) is "1-1"

proof

A5: the MorphMap of (id A) = id the Arrows of A by FUNCTOR0:def 30;
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 A6: 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 A6, MSUALG_3:def 1; :: thesis: verum

end;

hence the MorphMap of (id A) is "1-1" by A5, MSUALG_3:1; :: thesis: verum

end;

A7: f is "onto"

proof

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

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 A8: i in [:the carrier of A,the carrier of A:] ; :: thesis: rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i
dom the Arrows of A = [:the carrier of A,the carrier of A:] by PBOOLE:def 3;
then A9: (dom the Arrows of A) /\ [:the carrier of A,the carrier of A:] = [:the carrier of A,the carrier of A:] ;
rng (f . i) = rng ((id the Arrows of A) . i) by A2, FUNCTOR0:def 30
.= rng (id (the Arrows of A . i)) by A8, 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 A8, A9, 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;

hence f is "onto" by MSUALG_3:def 3; :: thesis: verum

end;

A10: f "" = f

proof

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 A11: 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 A2, A4, A7, MSUALG_3:def 5
.= ((id the Arrows of A) . i) " by FUNCTOR0:def 30
.= (id (the Arrows of A . i)) " by A11, MSUALG_3:def 1
.= id (the Arrows of A . i) by FUNCT_1:67
.= (id the Arrows of A) . i by A11, MSUALG_3:def 1
.= f . i by A2, FUNCTOR0:def 30 ;
hence (f "" ) . i = f . i ; :: thesis: verum

end;

hence f "" = f by PBOOLE:3; :: thesis: verum

end;

the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:]) = the MorphMap of (id A)

proof

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

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 A12: 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
dom the MorphMap of (id A) = [:the carrier of A,the carrier of A:] by PBOOLE:def 3;
then (dom the MorphMap of (id A)) /\ [:the carrier of A,the carrier of A:] = [:the carrier of A,the carrier of A:] ;
hence (the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:])) . i = the MorphMap of (id A) . i by A12, FUNCT_1:38; :: thesis: verum

end;

hence the MorphMap of (id A) * (id [:the carrier of A,the carrier of A:]) = the MorphMap of (id A) by PBOOLE:3; :: thesis: verum

end;

hence (id A) " = id A by A1, A2, A3, A10, FUNCTOR0:def 30; :: thesis: verum