let A be non empty transitive with_units AltCatStr ; (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
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 ;
( 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:]
;
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
;
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
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
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; verum