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 Def30;
thus id A is one-to-one :: according to FUNCTOR0:def 34,FUNCTOR0:def 36 :: thesis: ( id A is faithful & id A is surjective )

proof

thus the ObjectMap of (id A) is one-to-one by A1; :: according to FUNCTOR0:def 7 :: thesis: verum

end;

thus id A is faithful :: thesis: id A is surjective

proof

per cases ( the carrier of A <> {} or the carrier of A = {} ) ;

suppose A2: the carrier of A <> {} ; :: thesis: id A is faithful

let i be set ; :: according to MSUALG_3:def 2,FUNCTOR0:def 31 :: thesis: for b₁ being set holds
( not i in dom the MorphMap of (id A) or not the MorphMap of (id A) . i = b₁ or b₁ is one-to-one )
let f be Function; :: thesis: ( not i in dom 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 ; :: thesis: f is one-to-one
dom the MorphMap of (id A) = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then consider o1, o2 being Element of A such that
A5: i = [o1,o2] by A2, A3, DOMAIN_1:9;
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:106;
f = (id the Arrows of A) . o1,o2 by A4, A5, Def30
.= id (the Arrows of A . [o1,o2]) by A6, MSUALG_3:def 1 ;
hence f is one-to-one ; :: thesis: verum

end;

suppose A7: the carrier of A = {} ; :: thesis: id A is faithful

let i be set ; :: according to MSUALG_3:def 2,FUNCTOR0:def 31 :: thesis: for b₁ being set holds
( not i in dom the MorphMap of (id A) or not the MorphMap of (id A) . i = b₁ or b₁ is one-to-one )
let f be Function; :: thesis: ( not i in dom the MorphMap of (id A) or not the MorphMap of (id A) . i = f or f is one-to-one )
assume that
A8: i in dom the MorphMap of (id A) and
the MorphMap of (id A) . i = f ; :: thesis: f is one-to-one
dom the MorphMap of (id A) = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4
.= {} by A7, ZFMISC_1:113 ;
hence f is one-to-one by A8; :: thesis: verum

end;

end;

end;

thus id A is full :: according to FUNCTOR0:def 35 :: thesis: id A is onto

proof

per cases ( not A is empty or A is empty ) ;

suppose not A is empty ; :: thesis: 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 Def5;
take f ; :: according to FUNCTOR0:def 33 :: thesis: ( f = the MorphMap of (id A) & f is "onto" )
thus f = the MorphMap of (id A) ; :: thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [:the carrier of A,the carrier of A:] or rng (f . i) = (the Arrows of A * the ObjectMap of (id A)) . i )
assume A9: i in [:the carrier of A,the carrier of A:] ; :: thesis: rng (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:9;
reconsider o1 = o1, o2 = o2 as object of A ;
A11: [o1,o2] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
A12: dom the ObjectMap of (id A) = [:the carrier of A,the carrier of A:] by A1, RELAT_1:71;
f . i = (id the Arrows of A) . o1,o2 by A10, Def30
.= id (the Arrows of A . [o1,o2]) by A11, MSUALG_3:def 1 ;
hence rng (f . i) = the Arrows of A . [o1,o2] by RELAT_1:71
.= the Arrows of A . (the ObjectMap of (id A) . i) by A1, A9, A10, FUNCT_1:35
.= (the Arrows of A * the ObjectMap of (id A)) . i by A9, A12, FUNCT_1:23 ;
:: thesis: verum

end;

hence id A is full ; :: thesis: verum

end;

suppose A is empty ; :: thesis: id A is full

then A13: the carrier of A = {} ;
the ObjectMap of (id A) = id [:the carrier of A,the carrier of A:] by Def30;
then reconsider B = the Arrows of A * the ObjectMap of (id A) as ManySortedSet of by Th3;
reconsider f = the MorphMap of (id A) as ManySortedSet of ;
f is ManySortedFunction of the Arrows of A,B

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in [:the carrier of A,the carrier of A:] or f . i is Element of bool [:(the Arrows of A . i),(B . i):] )
thus ( not i in [:the carrier of A,the carrier of A:] or f . i is Element of bool [:(the Arrows of A . i),(B . i):] ) by A13, ZFMISC_1:113; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of the Arrows of A,B ;
take B ; :: according to FUNCTOR0:def 32 :: thesis: ex f being ManySortedFunction of the Arrows of A,B st
( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" )
take f ; :: thesis: ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) & f is "onto" )
thus ( B = the Arrows of A * the ObjectMap of (id A) & f = the MorphMap of (id A) ) ; :: thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [:the carrier of A,the carrier of A:] or rng (f . i) = B . i )
thus ( not i in [:the carrier of A,the carrier of A:] or rng (f . i) = B . i ) by A13, ZFMISC_1:113; :: thesis: verum

end;

end;

end;

thus id A is onto :: thesis: verum

proof

rng (id [:the carrier of A,the carrier of A:]) = [:the carrier of A,the carrier of A:] by RELAT_1:71;
hence the ObjectMap of (id A) is onto by A1, FUNCT_2:def 3; :: according to FUNCTOR0:def 8 :: thesis: verum

end;