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 a' being object of B
for a being object of A st a' = a holds
G . a' = (id A) . a ) & ( for b', c' being object of B
for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map (id A),b,c) . f ) )
take G = id B; :: thesis: ( G is bijective & ( for a' being object of B
for a being object of A st a' = a holds
G . a' = (id A) . a ) & ( for b', c' being object of B
for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map (id A),b,c) . f ) )
thus G is bijective ; :: thesis: ( ( for a' being object of B
for a being object of A st a' = a holds
G . a' = (id A) . a ) & ( for b', c' being object of B
for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map (id A),b,c) . f ) )

hereby :: thesis: for b', c' being object of B
for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (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:30
.= (id A) . a1 by FUNCTOR0:30 ;
:: thesis: verum

end;

let b, c be object of B; :: thesis: for b, c being object of A st <^b,c^> <> {} & b = b & c = c holds
for f' being Morphism of b,c
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map (id A),b,c) . f
let b1, c1 be object of A; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f' being Morphism of b,c
for f being Morphism of b1,c1 st f' = f holds
G . f' = (Morph-Map (id A),b1,c1) . f )
assume A1: ( <^b,c^> <> {} & b = b1 & c = c1 ) ; :: thesis: for f' being 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 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 A2: f = f1 ; :: thesis: G . f = (Morph-Map (id A),b1,c1) . f1
A3: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A1, ALTCAT_2:32;
A4: ( (id A) . b1 = b1 & (id A) . c1 = c1 ) by FUNCTOR0:30;
thus G . f = f by A1, FUNCTOR0:32
.= (id A) . f1 by A2, A3, FUNCTOR0:32
.= (Morph-Map (id A),b1,c1) . f1 by A3, A4, FUNCTOR0:def 16 ; :: thesis: verum