let A be category; :: thesis: for B being non empty subcategory of A holds B,B are_isomorphic_under id A

let B be non empty subcategory of A; :: thesis: B,B are_isomorphic_under id A

set F = id A;

thus ( B is subcategory of A & B is subcategory of A ) ; :: according to YELLOW20:def 4 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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 ) )

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; :: thesis: ( <^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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: ( f = f1 implies G . f = (Morph-Map ((id A),b1,c1)) . f1 )

assume A3: f = f1 ; :: thesis: 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 ; :: thesis: verum

let B be non empty subcategory of A; :: thesis: B,B are_isomorphic_under id A

set F = id A;

thus ( B is subcategory of A & B is subcategory of A ) ; :: according to YELLOW20:def 4 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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 ) )

hereby :: thesis: 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; :: thesis: for b, c being Object of A st <^b,c^> <> {} & b = b & c = c holds 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 a be Object of B; :: thesis: for a1 being Object of A st a = a1 holds

G . a = (id A) . a1

let a1 be Object of A; :: thesis: ( a = a1 implies G . a = (id A) . a1 )

assume a = a1 ; :: thesis: G . a = (id A) . a1

hence G . a = a1 by FUNCTOR0:29

.= (id A) . a1 by FUNCTOR0:29 ;

:: thesis: verum

end;G . a = (id A) . a1

let a1 be Object of A; :: thesis: ( a = a1 implies G . a = (id A) . a1 )

assume a = a1 ; :: thesis: G . a = (id A) . a1

hence G . a = a1 by FUNCTOR0:29

.= (id A) . a1 by FUNCTOR0:29 ;

:: thesis: verum

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; :: thesis: ( <^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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: ( f = f1 implies G . f = (Morph-Map ((id A),b1,c1)) . f1 )

assume A3: f = f1 ; :: thesis: 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 ; :: thesis: verum