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 ; :: according to FUNCTOR0:def 33,FUNCTOR0:def 35 :: thesis: ( id A is faithful & id A is surjective )
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 30 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: 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 30 :: thesis: 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; :: thesis: ( 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
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 2
.= {} by A7, ZFMISC_1:90 ;
hence f is one-to-one by A8; :: thesis: verum
end;
end;
end;
thus id A is full :: according to FUNCTOR0:def 34 :: 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 Def4;
take f ; :: according to FUNCTOR0:def 32 :: 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 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:] ; :: thesis: 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 ;
:: 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 Def29;
then reconsider B = the Arrows of A * the ObjectMap of (id A) as ManySortedSet of [: the carrier of A, the carrier of A:] by Th2;
reconsider f = the MorphMap of (id A) as ManySortedSet of [: the carrier of A, the carrier of A:] ;
f is ManySortedFunction of the Arrows of A,B
proof
let i be object ; :: according to PBOOLE:def 15 :: 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:90; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Arrows of A,B ;
take B ; :: according to FUNCTOR0:def 31 :: 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 proj2 (f . i) = B . i )
thus ( not i in [: the carrier of A, the carrier of A:] or proj2 (f . i) = B . i ) by A13, ZFMISC_1:90; :: thesis: verum
end;
end;
end;
the ObjectMap of (id A) is onto by A1;
hence id A is onto ; :: thesis: verum