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 38;
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 29;
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 2;
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 29
.= rng (id ( the Arrows of A . i)) by A7, MSUALG_3:def 1
.= the Arrows of A . i
.= ( the Arrows of A * (id [: the carrier of A, the carrier of A:])) . i by A7, A6, FUNCT_1:20
.= ( the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def 29 ;
hence rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ; :: thesis: verum
end;
then A8: f is "onto" ;
for i being object st i in [: the carrier of A, the carrier of A:] holds
(f "") . i = f . i
proof
let i be object ; :: 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 4
.= ((id the Arrows of A) . i) " by FUNCTOR0:def 29
.= (id ( the Arrows of A . i)) " by A9, MSUALG_3:def 1
.= id ( the Arrows of A . i) by FUNCT_1:45
.= (id the Arrows of A) . i by A9, MSUALG_3:def 1
.= f . i by A1, FUNCTOR0:def 29 ;
hence (f "") . i = f . i ; :: thesis: verum
end;
then A10: f "" = f ;
for i being object 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 2;
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 object ; :: 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:20; :: thesis: verum
end;
then A12: the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:]) = the MorphMap of (id A) ;
A13: the ObjectMap of ((id A) ") = the ObjectMap of (id A) " by FUNCTOR0:def 38;
then the ObjectMap of ((id A) ") = (id [: the carrier of A, the carrier of A:]) " by FUNCTOR0:def 29
.= id [: the carrier of A, the carrier of A:] by FUNCT_1:45
.= the ObjectMap of (id A) by FUNCTOR0:def 29 ;
hence (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def 29; :: thesis: verum