let A1, A2 be category; :: thesis: for F being contravariant 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 <^b2,a2^> ) ) holds

B1,B2 are_anti-isomorphic_under F

let F be contravariant 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 <^b2,a2^> ) ) holds

B1,B2 are_anti-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 <^b2,a2^> ) ) holds

B1,B2 are_anti-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 <^b2,a2^> ) ) implies B1,B2 are_anti-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 <^b2,a2^> ) ; :: thesis: B1,B2 are_anti-isomorphic_under F

thus B1,B2 are_anti-isomorphic_under F :: thesis: verum

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 <^b2,a2^> ) ) holds

B1,B2 are_anti-isomorphic_under F

let F be contravariant 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 <^b2,a2^> ) ) holds

B1,B2 are_anti-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 <^b2,a2^> ) ) holds

B1,B2 are_anti-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 <^b2,a2^> ) ) implies B1,B2 are_anti-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 <^b2,a2^> ) ; :: thesis: B1,B2 are_anti-isomorphic_under F

thus B1,B2 are_anti-isomorphic_under F :: thesis: verum

proof

deffunc H_{1}( Object of B1, Object of B1, Morphism of $1,$2) -> M3(<^((F | B1) . $2),((F | B1) . $1)^>) = (F | B1) . $3;

deffunc H_{2}( 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

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )

( 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;

A41: for a being Object of B1 holds G . a = H_{2}(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_{1}(a,b,f)
from YELLOW18:sch 9(A13, A14, A22, A39);

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 ) )

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 ) )

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: ( 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 (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 A45, A46, ALTCAT_2:31;

then A49: <^(F . c1),(F . b1)^> <> {} by FUNCTOR0:def 19;

thus G . f = (F | B1) . f by A42, A45

.= F . f1 by A45, A46, A47, Th30

.= (Morph-Map (F,b1,c1)) . f1 by A48, A49, FUNCTOR0:def 16 ; :: thesis: verum

end;deffunc H

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

( b = H

proof

A12:
the carrier of B1 c= the carrier of A1
by ALTCAT_2:def 11;
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

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(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

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(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

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )

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: ( b1 = F . c1 & a1 = F . d1 ) and

A10: <^c1,d1^> <> {} and

A11: f1 = F . g1 by A4, A8, Th36;

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

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )

take d ; :: thesis: ex g being Morphism of c,d st

( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )

take g ; :: thesis: ( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )

g1 in <^c,d^> by A3, A7, A9, A10, A11;

hence ( b = H_{2}(c) & a = H_{2}(d) & <^c,d^> <> {} & f = H_{1}(c,d,g) )
by A9, A11, Th28, Th30; :: thesis: verum

end;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

( b = H

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

( b = H

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

( b = H

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: ( b1 = F . c1 & a1 = F . d1 ) and

A10: <^c1,d1^> <> {} and

A11: f1 = F . g1 by A4, A8, Th36;

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

( b = H

take d ; :: thesis: ex g being Morphism of c,d st

( b = H

take g ; :: thesis: ( b = H

g1 in <^c,d^> by A3, A7, A9, A10, A11;

hence ( b = H

A13: now :: thesis: for a being Object of B1 holds H_{2}(a) is Object of B2

let a be Object of B1; :: thesis: H_{2}(a) is Object of B2

reconsider b = a as Object of A1 by A12;

(F | B1) . a = F . b by Th28;

hence H_{2}(a) is Object of B2
by A2; :: thesis: verum

end;reconsider b = a as Object of A1 by A12;

(F | B1) . a = F . b by Th28;

hence H

A14: now :: thesis: for a, b being Object of B1 st <^a,b^> <> {} holds

for f being Morphism of a,b holds H_{1}(a,b,f) in the Arrows of B2 . (H_{2}(b),H_{2}(a))

thus
( B1 is subcategory of A1 & B2 is subcategory of A2 )
; :: according to YELLOW20:def 5 :: thesis: ex G being contravariant Functor of B1,B2 st for f being Morphism of a,b holds H

let a, b be Object of B1; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds H_{1}(a,b,f) in the Arrows of B2 . (H_{2}(b),H_{2}(a)) )

assume A15: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H_{1}(a,b,f) in the Arrows of B2 . (H_{2}(b),H_{2}(a))

let f be Morphism of a,b; :: thesis: H_{1}(a,b,f) in the Arrows of B2 . (H_{2}(b),H_{2}(a))

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, Th30;

then (F | B1) . f in <^b9,a9^> by A3, A16, A17;

hence H_{1}(a,b,f) in the Arrows of B2 . (H_{2}(b),H_{2}(a))
; :: thesis: verum

end;assume A15: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds H

let f be Morphism of a,b; :: thesis: H

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, Th30;

then (F | B1) . f in <^b9,a9^> by A3, A16, A17;

hence H

( 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 H_{1}(a,b,f) = H_{1}(a,b,g) holds

f = g

for f, g being Morphism of a,b st H

f = g

let a, b be Object of B1; :: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H_{1}(a,b,f) = H_{1}(a,b,g) holds

f = g )

assume A20: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st H_{1}(a,b,f) = H_{1}(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: ( H_{1}(a,b,f) = H_{1}(a,b,g) implies f = g )

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_{1}(a,b,f) = H_{1}(a,b,g)
; :: thesis: f = g

then F . f1 = (F | B1) . g by A20, Th30

.= F . g1 by A20, Th30 ;

hence f = g by A18, A21, Th35; :: thesis: verum

end;f = g )

assume A20: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st H

f = g

reconsider a1 = a, b1 = b as Object of A1 by A12;

let f, g be Morphism of a,b; :: thesis: ( H

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

then F . f1 = (F | B1) . g by A20, Th30

.= F . g1 by A20, Th30 ;

hence f = g by A18, A21, Th35; :: thesis: verum

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 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of B2 st a9 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

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 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9 )

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 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9

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 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9

let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of B2 st a9 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9

reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;

let a9, b9, c9 be Object of B2; :: thesis: ( a9 = H_{2}(a) & b9 = H_{2}(b) & c9 = H_{2}(c) implies for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9 )

assume that

A25: a9 = H_{2}(a)
and

A26: b9 = H_{2}(b)
and

A27: c9 = H_{2}(c)
; :: thesis: for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) holds

H_{1}(a,c,g * f) = f9 * g9

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

H_{1}(a,c,g * f) = f9 * g9

let g9 be Morphism of c9,b9; :: thesis: ( f9 = H_{1}(a,b,f) & g9 = H_{1}(b,c,g) implies H_{1}(a,c,g * f) = f9 * g9 )

assume that

A28: f9 = H_{1}(a,b,f)
and

A29: g9 = H_{1}(b,c,g)
; :: thesis: H_{1}(a,c,g * f) = f9 * g9

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, Th30;

then A36: g9 in <^c9,b9^> by A3, A31, A30, A32;

A37: f9 = F . f1 by A23, A28, Th30;

then A38: f9 in <^b9,a9^> 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 Th30;

hence H_{1}(a,c,g * f) =
(F . f1) * (F . g1)
by A33, A31, FUNCTOR0:def 24

.= f9 * g9 by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2:32 ;

:: thesis: verum

end;for g being Morphism of b,c

for a9, b9, c9 being Object of B2 st a9 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

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 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

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 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of B2 st a9 = H

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = H

H

reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;

let a9, b9, c9 be Object of B2; :: thesis: ( a9 = H

for g9 being Morphism of c9,b9 st f9 = H

H

assume that

A25: a9 = H

A26: b9 = H

A27: c9 = H

for g9 being Morphism of c9,b9 st f9 = H

H

let f9 be Morphism of b9,a9; :: thesis: for g9 being Morphism of c9,b9 st f9 = H

H

let g9 be Morphism of c9,b9; :: thesis: ( f9 = H

assume that

A28: f9 = H

A29: g9 = H

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, Th30;

then A36: g9 in <^c9,b9^> by A3, A31, A30, A32;

A37: f9 = F . f1 by A23, A28, Th30;

then A38: f9 in <^b9,a9^> 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 Th30;

hence H

.= f9 * g9 by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2:32 ;

:: thesis: verum

A39: now :: thesis: for a being Object of B1

for a9 being Object of B2 st a9 = H_{2}(a) holds

H_{1}(a,a, idm a) = idm a9

consider G being strict contravariant Functor of B1,B2 such that for a9 being Object of B2 st a9 = H

H

let a be Object of B1; :: thesis: for a9 being Object of B2 st a9 = H_{2}(a) holds

H_{1}(a,a, idm a) = idm a9

let a9 be Object of B2; :: thesis: ( a9 = H_{2}(a) implies H_{1}(a,a, idm a) = idm a9 )

assume A40: a9 = H_{2}(a)
; :: thesis: H_{1}(a,a, idm a) = idm a9

reconsider a1 = a as Object of A1 by A12;

thus H_{1}(a,a, idm a) =
F . (idm a1)
by Th30, ALTCAT_2:34

.= idm (F . a1) by ALTCAT_4:13

.= idm a9 by A40, Th28, ALTCAT_2:34 ; :: thesis: verum

end;H

let a9 be Object of B2; :: thesis: ( a9 = H

assume A40: a9 = H

reconsider a1 = a as Object of A1 by A12;

thus H

.= idm (F . a1) by ALTCAT_4:13

.= idm a9 by A40, Th28, ALTCAT_2:34 ; :: thesis: verum

A41: for a being Object of B1 holds G . a = H

A42: for a, b being Object of B1 st <^a,b^> <> {} holds

for f being Morphism of a,b holds G . f = H

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 H_{2}(a) = H_{2}(b) holds

a = b

thus
G is bijective
from YELLOW18:sch 12(A41, A42, A43, A19, A5); :: thesis: ( ( for a9 being Object of B1a = b

let a, b be Object of B1; :: thesis: ( H_{2}(a) = H_{2}(b) implies a = b )

reconsider a1 = a, b1 = b as Object of A1 by A12;

assume H_{2}(a) = H_{2}(b)
; :: thesis: a = b

then F . a1 = (F | B1) . b by Th28

.= F . b1 by Th28 ;

hence a = b by A18, Th34; :: thesis: verum

end;reconsider a1 = a, b1 = b as Object of A1 by A12;

assume H

then F . a1 = (F | B1) . b by Th28

.= F . b1 by Th28 ;

hence a = b by A18, Th34; :: thesis: verum

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 b, c be Object of B1; :: thesis: for b, c being Object of A1 st <^b,c^> <> {} & b = b & c = c holds 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 A44, Th28 ; :: thesis: verum

end;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 A44, Th28 ; :: thesis: verum

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: ( 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 (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 A45, A46, ALTCAT_2:31;

then A49: <^(F . c1),(F . b1)^> <> {} by FUNCTOR0:def 19;

thus G . f = (F | B1) . f by A42, A45

.= F . f1 by A45, A46, A47, Th30

.= (Morph-Map (F,b1,c1)) . f1 by A48, A49, FUNCTOR0:def 16 ; :: thesis: verum