let A be category; for B being non empty subcategory of A holds B,B are_isomorphic_under id A
let B be non empty subcategory of A; B,B are_isomorphic_under id A
set F = id A;
thus
( B is subcategory of A & B is subcategory of A )
; YELLOW20:def 4 ex G being covariant Functor of B,B st
( G is bijective & ( for a9 being Object of B
for a being Object of A st a9 = a holds
G . a9 = (id A) . a ) & ( for b9, c9 being Object of B
for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map ((id A),b,c)) . f ) )
take G = id B; ( G is bijective & ( for a9 being Object of B
for a being Object of A st a9 = a holds
G . a9 = (id A) . a ) & ( for b9, c9 being Object of B
for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map ((id A),b,c)) . f ) )
thus
G is bijective
; ( ( for a9 being Object of B
for a being Object of A st a9 = a holds
G . a9 = (id A) . a ) & ( for b9, c9 being Object of B
for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map ((id A),b,c)) . f ) )
let b, c be Object of B; for b, c being Object of A st <^b,c^> <> {} & b = b & c = c holds
for f9 being Morphism of b,c
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map ((id A),b,c)) . f
let b1, c1 be Object of A; ( <^b,c^> <> {} & b = b1 & c = c1 implies for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
G . f9 = (Morph-Map ((id A),b1,c1)) . f )
assume that
A1:
<^b,c^> <> {}
and
A2:
( b = b1 & c = c1 )
; for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
G . f9 = (Morph-Map ((id A),b1,c1)) . f
let f be Morphism of b,c; for f being Morphism of b1,c1 st f = f holds
G . f = (Morph-Map ((id A),b1,c1)) . f
let f1 be Morphism of b1,c1; ( f = f1 implies G . f = (Morph-Map ((id A),b1,c1)) . f1 )
assume A3:
f = f1
; G . f = (Morph-Map ((id A),b1,c1)) . f1
A4:
( <^b,c^> c= <^b1,c1^> & f in <^b,c^> )
by A1, A2, ALTCAT_2:31;
A5:
( (id A) . b1 = b1 & (id A) . c1 = c1 )
by FUNCTOR0:29;
thus G . f =
f
by A1, FUNCTOR0:31
.=
(id A) . f1
by A3, A4, FUNCTOR0:31
.=
(Morph-Map ((id A),b1,c1)) . f1
by A4, A5, FUNCTOR0:def 15
; verum