let A1, A2 be category; :: thesis:
let F be covariant Functor of A1,A2; :: thesis:
let B1 be non empty subcategory of A1; :: thesis:
let B2 be non empty subcategory of A2; :: thesis:
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:
thus B1,B2 are_isomorphic_under F :: thesis:

deffunc H₁( Object of B1, Object of B1, Morphism of $1,$2) -> M3(<^((F | B1) . $1),((F | B1) . $2)^>) = (F | B1) . $3;
deffunc H₂( 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 = H₂(c) & b = H₂(d) & <^c,d^> <> {} & f = H₁(c,d,g) )

A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;
let a, b be Object of B2; :: thesis:
assume A7: <^a,b^> <> {} ; :: thesis:
reconsider a1 = a, b1 = b as Object of A2 by A6;
let f be Morphism of a,b; :: thesis:
A8: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A7, ALTCAT_2:31;
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:
take d ; :: thesis:
take g ; :: thesis:
g1 in <^c,d^> by A3, A7, A9, A10, A11;
hence ( a = H₂(c) & b = H₂(d) & <^c,d^> <> {} & f = H₁(c,d,g) ) by A9, A11, Th28, Th29; :: thesis:

end;

let a be Object of B1; :: thesis:
reconsider b = a as Object of A1 by A12;
(F | B1) . a = F . b by Th28;
hence H₂(a) is Object of B2 by A2; :: thesis:

end;

let a, b be Object of B1; :: thesis:
assume A15: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
reconsider c = a, d = b as Object of A1 by A12;
A16: ( <^a,b^> c= <^c,d^> & f in <^a,b^> ) by A15, ALTCAT_2:31;
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 A15, Th29;
then (F | B1) . f in <^a9,b9^> by A3, A16, A17;
hence H₁(a,b,f) in the Arrows of B2 . (H₂(a),H₂(b)) ; :: thesis:

end;

let a, b be Object of B1; :: thesis:
assume A20: <^a,b^> <> {} ; :: thesis:
reconsider a1 = a, b1 = b as Object of A1 by A12;
let f, g be Morphism of a,b; :: thesis:
A21: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A20, ALTCAT_2:31;
reconsider f1 = f, g1 = g as Morphism of a1,b1 by A21;
assume H₁(a,b,f) = H₁(a,b,g) ; :: thesis:
then F . f1 = (F | B1) . g by A20, Th29
.= F . g1 by A20, Th29 ;
hence f = g by A18, A21, Th32; :: thesis:

end;

let a, b, c be Object of B1; :: thesis:
assume that
A23: <^a,b^> <> {} and
A24: <^b,c^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;
let a9, b9, c9 be Object of B2; :: thesis:
assume that
A25: a9 = H₂(a) and
A26: b9 = H₂(b) and
A27: c9 = H₂(c) ; :: thesis:
let f9 be Morphism of a9,b9; :: thesis:
let g9 be Morphism of b9,c9; :: thesis:
assume that
A28: f9 = H₁(a,b,f) and
A29: g9 = H₁(b,c,g) ; :: thesis:
A30: b9 = F . b1 by A26, Th28;
A31: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by A24, ALTCAT_2:31;
then reconsider g1 = g as Morphism of b1,c1 ;
A32: c9 = F . c1 by A27, Th28;
A33: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A23, ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1 ;
A34: a9 = F . a1 by A25, Th28;
A35: g9 = F . g1 by A24, A29, Th29;
then A36: g9 in <^b9,c9^> by A3, A31, A30, A32;
A37: f9 = F . f1 by A23, A28, Th29;
then A38: f9 in <^a9,b9^> by A3, A33, A34, A30;
( <^a,c^> <> {} & g * f = g1 * f1 ) by A23, A24, ALTCAT_1:def 2, ALTCAT_2:32;
then (F | B1) . (g * f) = F . (g1 * f1) by Th29;
hence H₁(a,c,g * f) = (F . g1) * (F . f1) by A33, A31, FUNCTOR0:def 23
.= g9 * f9 by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2:32 ;
:: thesis:

end;

let a be Object of B1; :: thesis:
let a9 be Object of B2; :: thesis:
assume A40: a9 = H₂(a) ; :: thesis:
reconsider a1 = a as Object of A1 by A12;
thus H₁(a,a, idm a) = F . (idm a1) by Th29, ALTCAT_2:34
.= idm (F . a1) by FUNCTOR2:1
.= idm a9 by A40, Th28, ALTCAT_2:34 ; :: thesis:

end;

consider G being strict covariant Functor of B1,B2 such that
A41: for a being Object of B1 holds G . a = H₂(a) and
A42: for a, b being Object of B1 st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = H₁(a,b,f) from YELLOW18:sch 8(A13, A14, A22, A39);
take G ; :: thesis:

let a, b be Object of B1; :: thesis:
reconsider a1 = a, b1 = b as Object of A1 by A12;
assume H₂(a) = H₂(b) ; :: thesis:
then F . a1 = (F | B1) . b by Th28
.= F . b1 by Th28 ;
hence a = b by A18, Th31; :: thesis:

end;

let a be Object of B1; :: thesis:
let a1 be Object of A1; :: thesis:
assume A44: a = a1 ; :: thesis:
thus G . a = (F | B1) . a by A41
.= F . a1 by A44, Th28 ; :: thesis:

end;

let b, c be Object of B1; :: thesis:
let b1, c1 be Object of A1; :: thesis:
assume that
A45: <^b,c^> <> {} and
A46: ( b1 = b & c1 = c ) ; :: thesis:
let f be Morphism of b,c; :: thesis:
let f1 be Morphism of b1,c1; :: thesis:
assume A47: f = f1 ; :: thesis:
A48: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A45, A46, ALTCAT_2:31;
then A49: <^(F . b1),(F . c1)^> <> {} by FUNCTOR0:def 18;
thus G . f = (F | B1) . f by A42, A45
.= F . f1 by A45, A46, A47, Th29
.= (Morph-Map (F,b1,c1)) . f1 by A48, A49, FUNCTOR0:def 15 ; :: thesis:

end;