let A1, A2 be category; :: thesis: for F being covariant Functor of A1,A2
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F

let F be covariant Functor of A1,A2; :: thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F

let B1 be non empty subcategory of A1; :: thesis: for B2 being non empty subcategory of A2 st F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F

let B2 be non empty subcategory of A2; :: thesis: ( F is bijective & ( for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) ) & ( for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) implies B1,B2 are_isomorphic_under F )

assume that
A1: F is bijective and
A2: for a being Object of A1 holds
( a is Object of B1 iff F . a is Object of B2 ) and
A3: for a, b being Object of A1 st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ; :: thesis: B1,B2 are_isomorphic_under F
thus B1,B2 are_isomorphic_under F :: thesis: verum
proof
deffunc H1( Object of B1, Object of B1, Morphism of \$1,\$2) -> M3(<^((F | B1) . \$1),((F | B1) . \$2)^>) = (F | B1) . \$3;
deffunc H2( Object of B1) -> M3( the carrier of A2) = (F | B1) . \$1;
A4: ( F is injective & F is surjective ) by A1;
A5: for a, b being Object of B2 st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
proof
A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
let a, b be Object of B2; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) ) )

assume A7: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )

reconsider a1 = a, b1 = b as Object of A2 by A6;
let f be Morphism of a,b; :: thesis: ex c, d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )

A8: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by ;
then reconsider f1 = f as Morphism of a1,b1 ;
consider c1, d1 being Object of A1, g1 being Morphism of c1,d1 such that
A9: ( a1 = F . c1 & b1 = F . d1 ) and
A10: <^c1,d1^> <> {} and
A11: f1 = F . g1 by A4, A8, Th33;
reconsider c = c1, d = d1 as Object of B1 by A2, A9;
reconsider g = g1 as Morphism of c,d by A3, A7, A9, A10, A11;
take c ; :: thesis: ex d being Object of B1 ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )

take d ; :: thesis: ex g being Morphism of c,d st
( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )

take g ; :: thesis: ( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
g1 in <^c,d^> by A3, A7, A9, A10, A11;
hence ( a = H2(c) & b = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) ) by ; :: thesis: verum
end;
A12: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;
A13: now :: thesis: for a being Object of B1 holds H2(a) is Object of B2
let a be Object of B1; :: thesis: H2(a) is Object of B2
reconsider b = a as Object of A1 by A12;
(F | B1) . a = F . b by Th28;
hence H2(a) is Object of B2 by A2; :: thesis: verum
end;
A14: now :: thesis: for a, b being Object of B1 st <^a,b^> <> {} holds
for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))
let a, b be Object of B1; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b)) )
assume A15: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))
let f be Morphism of a,b; :: thesis: H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b))
reconsider c = a, d = b as Object of A1 by A12;
A16: ( <^a,b^> c= <^c,d^> & f in <^a,b^> ) by ;
then reconsider g = f as Morphism of c,d ;
reconsider a9 = (F | B1) . a, b9 = (F | B1) . b as Object of B2 by A13;
A17: ( (F | B1) . a = F . c & (F | B1) . b = F . d ) by Th28;
(F | B1) . f = F . g by ;
then (F | B1) . f in <^a9,b9^> by A3, A16, A17;
hence H1(a,b,f) in the Arrows of B2 . (H2(a),H2(b)) ; :: thesis: verum
end;
thus ( B1 is subcategory of A1 & B2 is subcategory of A2 ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B1,B2 st
( G is bijective & ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 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 (F,b,c)) . f ) )

A18: ( F is one-to-one & F is faithful & F is surjective ) by A4;
A19: now :: thesis: for a, b being Object of B1 st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = g
let a, b be Object of B1; :: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = g )

assume A20: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st H1(a,b,f) = H1(a,b,g) holds
f = g

reconsider a1 = a, b1 = b as Object of A1 by A12;
let f, g be Morphism of a,b; :: thesis: ( H1(a,b,f) = H1(a,b,g) implies f = g )
A21: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by ;
reconsider f1 = f, g1 = g as Morphism of a1,b1 by A21;
assume H1(a,b,f) = H1(a,b,g) ; :: thesis: f = g
then F . f1 = (F | B1) . g by
.= F . g1 by ;
hence f = g by ; :: thesis: verum
end;
A22: now :: thesis: for a, b, c being Object of B1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9
let a, b, c be Object of B1; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9 )

assume that
A23: <^a,b^> <> {} and
A24: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c
for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9

let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of B2 st a9 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9

reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;
let a9, b9, c9 be Object of B2; :: thesis: ( a9 = H2(a) & b9 = H2(b) & c9 = H2(c) implies for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9 )

assume that
A25: a9 = H2(a) and
A26: b9 = H2(b) and
A27: c9 = H2(c) ; :: thesis: for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9

let f9 be Morphism of a9,b9; :: thesis: for g9 being Morphism of b9,c9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = g9 * f9

let g9 be Morphism of b9,c9; :: thesis: ( f9 = H1(a,b,f) & g9 = H1(b,c,g) implies H1(a,c,g * f) = g9 * f9 )
assume that
A28: f9 = H1(a,b,f) and
A29: g9 = H1(b,c,g) ; :: thesis: H1(a,c,g * f) = g9 * f9
A30: b9 = F . b1 by ;
A31: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by ;
then reconsider g1 = g as Morphism of b1,c1 ;
A32: c9 = F . c1 by ;
A33: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by ;
then reconsider f1 = f as Morphism of a1,b1 ;
A34: a9 = F . a1 by ;
A35: g9 = F . g1 by ;
then A36: g9 in <^b9,c9^> by A3, A31, A30, A32;
A37: f9 = F . f1 by ;
then A38: f9 in <^a9,b9^> by A3, A33, A34, A30;
( <^a,c^> <> {} & g * f = g1 * f1 ) by ;
then (F | B1) . (g * f) = F . (g1 * f1) by Th29;
hence H1(a,c,g * f) = (F . g1) * (F . f1) by
.= g9 * f9 by ;
:: thesis: verum
end;
A39: now :: thesis: for a being Object of B1
for a9 being Object of B2 st a9 = H2(a) holds
H1(a,a, idm a) = idm a9
let a be Object of B1; :: thesis: for a9 being Object of B2 st a9 = H2(a) holds
H1(a,a, idm a) = idm a9

let a9 be Object of B2; :: thesis: ( a9 = H2(a) implies H1(a,a, idm a) = idm a9 )
assume A40: a9 = H2(a) ; :: thesis: H1(a,a, idm a) = idm a9
reconsider a1 = a as Object of A1 by A12;
thus H1(a,a, idm a) = F . (idm a1) by
.= idm (F . a1) by FUNCTOR2:1
.= idm a9 by ; :: thesis: verum
end;
consider G being strict covariant Functor of B1,B2 such that
A41: for a being Object of B1 holds G . a = H2(a) and
A42: for a, b being Object of B1 st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = H1(a,b,f) from take G ; :: thesis: ( G is bijective & ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 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 (F,b,c)) . f ) )

A43: now :: thesis: for a, b being Object of B1 st H2(a) = H2(b) holds
a = b
let a, b be Object of B1; :: thesis: ( H2(a) = H2(b) implies a = b )
reconsider a1 = a, b1 = b as Object of A1 by A12;
assume H2(a) = H2(b) ; :: thesis: a = b
then F . a1 = (F | B1) . b by Th28
.= F . b1 by Th28 ;
hence a = b by ; :: thesis: verum
end;
thus G is bijective from :: thesis: ( ( for a9 being Object of B1
for a being Object of A1 st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of B1
for b, c being Object of A1 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 (F,b,c)) . f ) )

hereby :: thesis: for b9, c9 being Object of B1
for b, c being Object of A1 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 (F,b,c)) . f
let a be Object of B1; :: thesis: for a1 being Object of A1 st a = a1 holds
G . a = F . a1

let a1 be Object of A1; :: thesis: ( a = a1 implies G . a = F . a1 )
assume A44: a = a1 ; :: thesis: G . a = F . a1
thus G . a = (F | B1) . a by A41
.= F . a1 by ; :: thesis: verum
end;
let b, c be Object of B1; :: thesis: for b, c being Object of A1 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 (F,b,c)) . f

let b1, c1 be Object of A1; :: 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 (F,b1,c1)) . f )

assume that
A45: <^b,c^> <> {} and
A46: ( b1 = b & c1 = c ) ; :: thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
G . f9 = (Morph-Map (F,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 (F,b1,c1)) . f

let f1 be Morphism of b1,c1; :: thesis: ( f = f1 implies G . f = (Morph-Map (F,b1,c1)) . f1 )
assume A47: f = f1 ; :: thesis: G . f = (Morph-Map (F,b1,c1)) . f1
A48: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by ;
then A49: <^(F . b1),(F . c1)^> <> {} by FUNCTOR0:def 18;
thus G . f = (F | B1) . f by
.= F . f1 by
.= (Morph-Map (F,b1,c1)) . f1 by ; :: thesis: verum
end;