set CC = [: the carrier of A, the carrier of A:];
A1:
the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:]
by Def29;
hence
id A is one-to-one
; FUNCTOR0:def 33,FUNCTOR0:def 35 ( id A is faithful & id A is surjective )
thus
id A is faithful
id A is surjective proof
per cases
( the carrier of A <> {} or the carrier of A = {} )
;
suppose A2:
the
carrier of
A <> {}
;
id A is faithful let i be
set ;
MSUALG_3:def 2,
FUNCTOR0:def 30 for b1 being set holds
( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = b1 or b1 is one-to-one )let f be
Function;
( not i in proj1 the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one )assume that A3:
i in dom the
MorphMap of
(id A)
and A4:
the
MorphMap of
(id A) . i = f
;
f is one-to-one consider o1,
o2 being
Element of
A such that A5:
i = [o1,o2]
by A2, A3, DOMAIN_1:1;
reconsider o1 =
o1,
o2 =
o2 as
Object of
A ;
A6:
[o1,o2] in [: the carrier of A, the carrier of A:]
by A2, ZFMISC_1:87;
f =
(id the Arrows of A) . (
o1,
o2)
by A4, A5, Def29
.=
id ( the Arrows of A . [o1,o2])
by A6, MSUALG_3:def 1
;
hence
f is
one-to-one
;
verum end; end;
end;
thus
id A is full
FUNCTOR0:def 34 id A is onto proof
per cases
( not A is empty or A is empty )
;
suppose
not
A is
empty
;
id A is full then reconsider A =
A as non
empty AltGraph ;
id A is
full
proof
reconsider f = the
MorphMap of
(id A) as
ManySortedFunction of the
Arrows of
A, the
Arrows of
A * the
ObjectMap of
(id A) by Def4;
take
f
;
FUNCTOR0:def 32 ( f = the MorphMap of (id A) & f is "onto" )
thus
f = the
MorphMap of
(id A)
;
f is "onto"
let i be
set ;
MSUALG_3:def 3 ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i )
assume A9:
i in [: the carrier of A, the carrier of A:]
;
proj2 (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i
then consider o1,
o2 being
Element of
A such that A10:
i = [o1,o2]
by DOMAIN_1:1;
reconsider o1 =
o1,
o2 =
o2 as
Object of
A ;
A11:
[o1,o2] in [: the carrier of A, the carrier of A:]
by ZFMISC_1:87;
A12:
dom the
ObjectMap of
(id A) = [: the carrier of A, the carrier of A:]
by A1;
f . i =
(id the Arrows of A) . (
o1,
o2)
by A10, Def29
.=
id ( the Arrows of A . [o1,o2])
by A11, MSUALG_3:def 1
;
hence rng (f . i) =
the
Arrows of
A . [o1,o2]
.=
the
Arrows of
A . ( the ObjectMap of (id A) . i)
by A1, A9, A10, FUNCT_1:18
.=
( the Arrows of A * the ObjectMap of (id A)) . i
by A9, A12, FUNCT_1:13
;
verum
end; hence
id A is
full
;
verum end; end;
end;
the ObjectMap of (id A) is onto
by A1;
hence
id A is onto
; verum