:: YELLOW20 semantic presentation

begin


theorem Th1: :: YELLOW20:1
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds
for a being object of A
for b being object of B holds
( F . a = b iff (F ") . b = a )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds
for a being object of A
for b being object of B holds
( F . a = b iff (F ") . b = a )
let F be reflexive feasible FunctorStr over A,B; ::_thesis: ( F is coreflexive & F is bijective implies for a being object of A
for b being object of B holds
( F . a = b iff (F ") . b = a ) )
assume A1: ( F is coreflexive & F is bijective ) ; ::_thesis: for a being object of A
for b being object of B holds
( F . a = b iff (F ") . b = a )
reconsider G = F " as reflexive feasible FunctorStr over B,A by A1, FUNCTOR0:35, FUNCTOR0:36;
let a be object of A; ::_thesis: for b being object of B holds
( F . a = b iff (F ") . b = a )
let b be object of B; ::_thesis: ( F . a = b iff (F ") . b = a )
 (F ") * F = id A by A1, FUNCTOR1:19;
then  a = ((F ") * F) . a by FUNCTOR0:29;
hence  ( F . a = b implies (F ") . b = a ) by FUNCTOR0:33; ::_thesis: ( (F ") . b = a implies F . a = b )
 F * G = id B by A1, FUNCTOR1:18;
then  b = (F * G) . b by FUNCTOR0:29;
hence  ( (F ") . b = a implies F . a = b ) by FUNCTOR0:33; ::_thesis: verum
end;

theorem Th2: :: YELLOW20:2
for A, B being non empty transitive with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
let F be feasible Covariant FunctorStr over A,B; ::_thesis: for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
let G be feasible Covariant FunctorStr over B,A; ::_thesis: ( F is bijective & G = F " implies for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f ) )
assume that
A1: F is bijective and
A2: G = F " ; ::_thesis: for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
let a1, a2 be object of A; ::_thesis: ( <^a1,a2^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f ) )
assume A3: <^a1,a2^> <> {} ; ::_thesis: for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
A4: <^(F . a1),(F . a2)^> <> {} by A3, FUNCTOR0:def_18;
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then  ( F is reflexive & F is coreflexive ) by FUNCTOR0:44;
then A5: ( G . (F . a1) = a1 & G . (F . a2) = a2 ) by A1, A2, Th1;
let f be Morphism of a1,a2; ::_thesis: for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
let g be Morphism of (F . a1),(F . a2); ::_thesis: ( F . f = g iff G . g = f )
 (F ") * F = id A by A1, FUNCTOR1:19;
then  f = (G * F) . f by A2, A3, FUNCTOR0:31;
hence  ( F . f = g implies G . g = f ) by A3, FUNCTOR3:6; ::_thesis: ( G . g = f implies F . f = g )
 F * G = id B by A1, A2, FUNCTOR1:18;
then  g = (F * G) . g by A4, FUNCTOR0:31;
hence  ( G . g = f implies F . f = g ) by A4, A5, FUNCTOR3:6; ::_thesis: verum
end;

theorem Th3: :: YELLOW20:3
for A, B being non empty transitive with_units AltCatStr
for F being feasible Contravariant FunctorStr over A,B
for G being feasible Contravariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being feasible Contravariant FunctorStr over A,B
for G being feasible Contravariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
let F be feasible Contravariant FunctorStr over A,B; ::_thesis: for G being feasible Contravariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
let G be feasible Contravariant FunctorStr over B,A; ::_thesis: ( F is bijective & G = F " implies for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f ) )
assume that
A1: F is bijective and
A2: G = F " ; ::_thesis: for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
let a1, a2 be object of A; ::_thesis: ( <^a1,a2^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f ) )
assume A3: <^a1,a2^> <> {} ; ::_thesis: for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
A4: <^(F . a2),(F . a1)^> <> {} by A3, FUNCTOR0:def_19;
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then  ( F is reflexive & F is coreflexive ) by FUNCTOR0:45;
then A5: ( G . (F . a1) = a1 & G . (F . a2) = a2 ) by A1, A2, Th1;
let f be Morphism of a1,a2; ::_thesis: for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
let g be Morphism of (F . a2),(F . a1); ::_thesis: ( F . f = g iff G . g = f )
 (F ") * F = id A by A1, FUNCTOR1:19;
then  f = (G * F) . f by A2, A3, FUNCTOR0:31;
hence  ( F . f = g implies G . g = f ) by A3, FUNCTOR3:7; ::_thesis: ( G . g = f implies F . f = g )
 F * G = id B by A1, A2, FUNCTOR1:18;
then  g = (F * G) . g by A4, FUNCTOR0:31;
hence  ( G . g = f implies F . f = g ) by A4, A5, FUNCTOR3:7; ::_thesis: verum
end;

theorem Th4: :: YELLOW20:4
for A, B being category
for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st F * G = id B holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st F * G = id B holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be Functor of A,B; ::_thesis: ( F is bijective implies for G being Functor of B,A st F * G = id B holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being Functor of B,A st F * G = id B holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
then reconsider FF = F " as feasible FunctorStr over B,A by FUNCTOR0:35;
A2: (F ") * F = id A by A1, FUNCTOR1:19;
let G be Functor of B,A; ::_thesis: ( F * G = id B implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume  F * G = id B ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
then (id A) * G = FF * (id B) by A2, FUNCTOR0:32
.= F " by FUNCTOR3:5 ;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by FUNCTOR3:4; ::_thesis: verum
end;

theorem Th5: :: YELLOW20:5
for A, B being category
for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be Functor of A,B; ::_thesis: ( F is bijective implies for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
then reconsider FF = F " as feasible FunctorStr over B,A by FUNCTOR0:35;
A2: F * FF = id B by A1, FUNCTOR1:18;
let G be Functor of B,A; ::_thesis: ( G * F = id A implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume  G * F = id A ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
then (id A) * FF = G * (id B) by A2, FUNCTOR0:32
.= FunctorStr(# the ObjectMap of G, the MorphMap of G #) by FUNCTOR3:5 ;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by FUNCTOR3:4; ::_thesis: verum
end;

theorem :: YELLOW20:6
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be covariant Functor of A,B; ::_thesis: ( F is bijective implies for G being covariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being covariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let G be covariant Functor of B,A; ::_thesis: ( ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume that
A2: for b being object of B holds F . (G . b) = b and
A3: for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
A4: now__::_thesis:_for_a,_b_being_object_of_B_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(F_*_G)_._f_=_(id_B)_._f
let a, b be object of B; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (F * G) . f = (id B) . f )
assume A5: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (F * G) . f = (id B) . f
let f be Morphism of a,b; ::_thesis: (F * G) . f = (id B) . f
thus (F * G) . f = F . (G . f) by A5, FUNCTOR3:6
.= f by A3, A5
.= (id B) . f by A5, FUNCTOR0:31 ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_object_of_B_holds_(F_*_G)_._b_=_(id_B)_._b
let b be object of B; ::_thesis: (F * G) . b = (id B) . b
thus (F * G) . b = F . (G . b) by FUNCTOR0:33
.= b by A2
.= (id B) . b by FUNCTOR0:29 ; ::_thesis: verum
end;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by A1, A4, Th4, YELLOW18:1; ::_thesis: verum
end;

theorem :: YELLOW20:7
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be contravariant Functor of A,B; ::_thesis: ( F is bijective implies for G being contravariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being contravariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let G be contravariant Functor of B,A; ::_thesis: ( ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume that
A2: for b being object of B holds F . (G . b) = b and
A3: for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
A4: now__::_thesis:_for_a,_b_being_object_of_B_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(F_*_G)_._f_=_(id_B)_._f
let a, b be object of B; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (F * G) . f = (id B) . f )
assume A5: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (F * G) . f = (id B) . f
let f be Morphism of a,b; ::_thesis: (F * G) . f = (id B) . f
thus (F * G) . f = F . (G . f) by A5, FUNCTOR3:7
.= f by A3, A5
.= (id B) . f by A5, FUNCTOR0:31 ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_object_of_B_holds_(F_*_G)_._b_=_(id_B)_._b
let b be object of B; ::_thesis: (F * G) . b = (id B) . b
thus (F * G) . b = F . (G . b) by FUNCTOR0:33
.= b by A2
.= (id B) . b by FUNCTOR0:29 ; ::_thesis: verum
end;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by A1, A4, Th4, YELLOW18:1; ::_thesis: verum
end;

theorem :: YELLOW20:8
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be covariant Functor of A,B; ::_thesis: ( F is bijective implies for G being covariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being covariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let G be covariant Functor of B,A; ::_thesis: ( ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume that
A2: for b being object of A holds G . (F . b) = b and
A3: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
A4: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(G_*_F)_._f_=_(id_A)_._f
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (G * F) . f = (id A) . f )
assume A5: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (G * F) . f = (id A) . f
let f be Morphism of a,b; ::_thesis: (G * F) . f = (id A) . f
thus (G * F) . f = G . (F . f) by A5, FUNCTOR3:6
.= f by A3, A5
.= (id A) . f by A5, FUNCTOR0:31 ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_object_of_A_holds_(G_*_F)_._b_=_(id_A)_._b
let b be object of A; ::_thesis: (G * F) . b = (id A) . b
thus (G * F) . b = G . (F . b) by FUNCTOR0:33
.= b by A2
.= (id A) . b by FUNCTOR0:29 ; ::_thesis: verum
end;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by A1, A4, Th5, YELLOW18:1; ::_thesis: verum
end;

theorem :: YELLOW20:9
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof
let A, B be category; ::_thesis: for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be contravariant Functor of A,B; ::_thesis: ( F is bijective implies for G being contravariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1: F is bijective ; ::_thesis: for G being contravariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let G be contravariant Functor of B,A; ::_thesis: ( ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume that
A2: for b being object of A holds G . (F . b) = b and
A3: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ; ::_thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
A4: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_(G_*_F)_._f_=_(id_A)_._f
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (G * F) . f = (id A) . f )
assume A5: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (G * F) . f = (id A) . f
let f be Morphism of a,b; ::_thesis: (G * F) . f = (id A) . f
thus (G * F) . f = G . (F . f) by A5, FUNCTOR3:7
.= f by A3, A5
.= (id A) . f by A5, FUNCTOR0:31 ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_object_of_A_holds_(G_*_F)_._b_=_(id_A)_._b
let b be object of A; ::_thesis: (G * F) . b = (id A) . b
thus (G * F) . b = G . (F . b) by FUNCTOR0:33
.= b by A2
.= (id A) . b by FUNCTOR0:29 ; ::_thesis: verum
end;
hence  FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by A1, A4, Th5, YELLOW18:1; ::_thesis: verum
end;

begin

definition
let A, B be AltCatStr ;
predA,B have_the_same_composition  means :Def1: :: YELLOW20:def 1
 for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3];
symmetry
 for A, B being AltCatStr st ( for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] ) holds
for a1, a2, a3 being set holds the Comp of B . [a1,a2,a3] tolerates the Comp of A . [a1,a2,a3] ;
end;

:: deftheorem Def1 defines have_the_same_composition YELLOW20:def_1_:_
 for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] );

theorem Th10: :: YELLOW20:10
for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
proof
let A, B be AltCatStr ; ::_thesis: ( A,B have_the_same_composition iff for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
hereby  ::_thesis: ( ( for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x ) implies A,B have_the_same_composition )
assume A1: A,B have_the_same_composition ; ::_thesis: for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x
let a1, a2, a3, x be set ; ::_thesis: ( x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) implies ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
assume  ( x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) ) ; ::_thesis: ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x
then A2: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) by XBOOLE_0:def_4;
 the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] by A1, Def1;
hence  ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A2, PARTFUN1:def_4; ::_thesis: verum
end;
assume A3: for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x ; ::_thesis: A,B have_the_same_composition
let a1, a2, a3, x be set ; :: according to PARTFUN1:def_4,YELLOW20:def_1 ::_thesis: ( not x in (proj1 ( the Comp of A . [a1,a2,a3])) /\ (proj1 ( the Comp of B . [a1,a2,a3])) or ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
assume  x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) ; ::_thesis: ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x
then  ( x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) ) by XBOOLE_0:def_4;
hence  ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A3; ::_thesis: verum
end;

theorem Th11: :: YELLOW20:11
for A, B being non empty transitive AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
proof
let A, B be non empty transitive AltCatStr ; ::_thesis: ( A,B have_the_same_composition iff for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
hereby  ::_thesis: ( ( for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 ) implies A,B have_the_same_composition )
assume A1: A,B have_the_same_composition ; ::_thesis: for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let a1, a2, a3 be object of A; ::_thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume A2: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) ; ::_thesis: for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let b1, b2, b3 be object of B; ::_thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume that
A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and
A4: ( b1 = a1 & b2 = a2 & b3 = a3 ) ; ::_thesis: for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let f1 be Morphism of a1,a2; ::_thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let g1 be Morphism of b1,b2; ::_thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume A5: g1 = f1 ; ::_thesis: for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let f2 be Morphism of a2,a3; ::_thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let g2 be Morphism of b2,b3; ::_thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )
assume A6: g2 = f2 ; ::_thesis: f2 * f1 = g2 * g1
 <^b1,b3^> <> {} by A3, ALTCAT_1:def_2;
then  dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def_1;
then A7: [g2,g1] in dom ( the Comp of B . (b1,b2,b3)) by A3, ZFMISC_1:def_2;
 <^a1,a3^> <> {} by A2, ALTCAT_1:def_2;
then  dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def_1;
then A8: [f2,f1] in dom ( the Comp of A . (a1,a2,a3)) by A2, ZFMISC_1:def_2;
A9: ( the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] & the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] ) by MULTOP_1:def_1;
thus f2 * f1 = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A2, ALTCAT_1:def_8
.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A1, A4, A5, A6, A9, A8, A7, Th10
.= g2 * g1 by A3, ALTCAT_1:def_8 ; ::_thesis: verum
end;
assume A10: for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 ; ::_thesis: A,B have_the_same_composition
let a1, a2, a3, x be set ; :: according to PARTFUN1:def_4,YELLOW20:def_1 ::_thesis: ( not x in (proj1 ( the Comp of A . [a1,a2,a3])) /\ (proj1 ( the Comp of B . [a1,a2,a3])) or ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
assume A11: x in (dom ( the Comp of A . [a1,a2,a3])) /\ (dom ( the Comp of B . [a1,a2,a3])) ; ::_thesis: ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x
then A12: x in dom ( the Comp of A . [a1,a2,a3]) by XBOOLE_0:def_4;
then  [a1,a2,a3] in dom the Comp of A by FUNCT_1:def_2, RELAT_1:38;
then A13: [a1,a2,a3] in [: the carrier of A, the carrier of A, the carrier of A:] ;
A14: x in dom ( the Comp of B . [a1,a2,a3]) by A11, XBOOLE_0:def_4;
then  [a1,a2,a3] in dom the Comp of B by FUNCT_1:def_2, RELAT_1:38;
then A15: [a1,a2,a3] in [: the carrier of B, the carrier of B, the carrier of B:] ;
reconsider a1 = a1, a2 = a2, a3 = a3 as object of A by A13, MCART_1:69;
reconsider b1 = a1, b2 = a2, b3 = a3 as object of B by A15, MCART_1:69;
A16: the Comp of A . (a1,a2,a3) = the Comp of A . [a1,a2,a3] by MULTOP_1:def_1;
then  ( [:<^a2,a3^>,<^a1,a2^>:] <> {} implies <^a1,a3^> <> {} ) by A11, XBOOLE_0:def_4;
then  dom ( the Comp of A . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] by FUNCT_2:def_1;
then consider f2, f1 being set  such that
A17: f2 in <^a2,a3^> and
A18: f1 in <^a1,a2^> and
A19: x = [f2,f1] by A12, A16, ZFMISC_1:def_2;
reconsider f1 = f1 as Morphism of a1,a2 by A18;
reconsider f2 = f2 as Morphism of a2,a3 by A17;
A20: the Comp of B . (b1,b2,b3) = the Comp of B . [b1,b2,b3] by MULTOP_1:def_1;
then  ( [:<^b2,b3^>,<^b1,b2^>:] <> {} implies <^b1,b3^> <> {} ) by A11, XBOOLE_0:def_4;
then A21: dom ( the Comp of B . (b1,b2,b3)) = [:<^b2,b3^>,<^b1,b2^>:] by FUNCT_2:def_1;
then A22: ( f1 in <^b1,b2^> & f2 in <^b2,b3^> ) by A14, A20, A19, ZFMISC_1:87;
reconsider g2 = f2 as Morphism of b2,b3 by A14, A20, A21, A19, ZFMISC_1:87;
reconsider g1 = f1 as Morphism of b1,b2 by A14, A20, A21, A19, ZFMISC_1:87;
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of A . (a1,a2,a3)) . (f2,f1) by A19, MULTOP_1:def_1
.= f2 * f1 by A17, A18, ALTCAT_1:def_8
.= g2 * g1 by A10, A17, A18, A22
.= ( the Comp of B . (b1,b2,b3)) . (g2,g1) by A22, ALTCAT_1:def_8 ;
hence  ( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x by A19, MULTOP_1:def_1; ::_thesis: verum
end;

theorem :: YELLOW20:12
for A, B being semi-functional para-functional category holds A,B have_the_same_composition
proof
let A, B be semi-functional para-functional category; ::_thesis: A,B have_the_same_composition
now__::_thesis:_for_a1,_a2,_a3_being_object_of_A_st_<^a1,a2^>_<>_{}_&_<^a2,a3^>_<>_{}_holds_
for_b1,_b2,_b3_being_object_of_B_st_<^b1,b2^>_<>_{}_&_<^b2,b3^>_<>_{}_&_b1_=_a1_&_b2_=_a2_&_b3_=_a3_holds_
for_f1_being_Morphism_of_a1,a2
for_g1_being_Morphism_of_b1,b2_st_g1_=_f1_holds_
for_f2_being_Morphism_of_a2,a3
for_g2_being_Morphism_of_b2,b3_st_g2_=_f2_holds_
f2_*_f1_=_g2_*_g1
let a1, a2, a3 be object of A; ::_thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume that
A1: <^a1,a2^> <> {} and
A2: <^a2,a3^> <> {} ; ::_thesis: for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let b1, b2, b3 be object of B; ::_thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume that
A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and
 b1 = a1 and
 b2 = a2 and
 b3 = a3 ; ::_thesis: for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let f1 be Morphism of a1,a2; ::_thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let g1 be Morphism of b1,b2; ::_thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
assume A4: g1 = f1 ; ::_thesis: for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
reconsider f = f1 as Function of (the_carrier_of a1),(the_carrier_of a2) by A1, YELLOW18:34;
let f2 be Morphism of a2,a3; ::_thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let g2 be Morphism of b2,b3; ::_thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )
assume A5: g2 = f2 ; ::_thesis: f2 * f1 = g2 * g1
A6: <^b1,b3^> <> {} by A3, ALTCAT_1:def_2;
reconsider g = f2 as Function of (the_carrier_of a2),(the_carrier_of a3) by A2, YELLOW18:34;
 <^a1,a3^> <> {} by A1, A2, ALTCAT_1:def_2;
hence f2 * f1 = g * f by A1, A2, ALTCAT_1:def_12
.= g2 * g1 by A3, A4, A5, A6, ALTCAT_1:def_12 ;
::_thesis: verum
end;
hence  A,B have_the_same_composition by Th11; ::_thesis: verum
end;

definition
let f, g be Function;
func Intersect (f,g) ->  Function means :Def2: :: YELLOW20:def 2
( dom it = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
it . x = (f . x) /\ (g . x) ) );
existence
 ex b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) )
proof
deffunc H1( set ) ->  set = (f . $1) /\ (g . $1);
thus  ex h being Function st
( dom h = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
h . x = H1(x) ) ) from FUNCT_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b2 . x = (f . x) /\ (g . x) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( dom f1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
f1 . x = (f . x) /\ (g . x) ) & dom f2 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
f2 . x = (f . x) /\ (g . x) ) implies f1 = f2 )
assume that
A1: dom f1 = (dom f) /\ (dom g) and
A2: for x being set st x in (dom f) /\ (dom g) holds
f1 . x = (f . x) /\ (g . x) and
A3: dom f2 = (dom f) /\ (dom g) and
A4: for x being set st x in (dom f) /\ (dom g) holds
f2 . x = (f . x) /\ (g . x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_(dom_f)_/\_(dom_g)_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f1 . x = f2 . x )
assume A5: x in (dom f) /\ (dom g) ; ::_thesis: f1 . x = f2 . x
then  f1 . x = (f . x) /\ (g . x) by A2;
hence  f1 . x = f2 . x by A4, A5; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
commutativity
 for b1, f, g being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) holds
( dom b1 = (dom g) /\ (dom f) & ( for x being set st x in (dom g) /\ (dom f) holds
b1 . x = (g . x) /\ (f . x) ) ) ;
end;

:: deftheorem Def2 defines Intersect YELLOW20:def_2_:_
 for f, g, b3 being Function holds
( b3 = Intersect (f,g) iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b3 . x = (f . x) /\ (g . x) ) ) );

theorem :: YELLOW20:13
for I being set
for A, B being ManySortedSet of I holds Intersect (A,B) = A /\ B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds Intersect (A,B) = A /\ B
let A, B be ManySortedSet of I; ::_thesis: Intersect (A,B) = A /\ B
A1: ( dom A = I & dom B = I ) by PARTFUN1:def_2;
then  dom (Intersect (A,B)) = I /\ I by Def2;
then reconsider AB = Intersect (A,B) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 I /\ I = I ;
then  for i being set st i in I holds
AB . i = (A . i) /\ (B . i) by A1, Def2;
hence  Intersect (A,B) = A /\ B by PBOOLE:def_5; ::_thesis: verum
end;

theorem Th14: :: YELLOW20:14
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J
proof
let I, J be set ; ::_thesis: for A being ManySortedSet of I
for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J
let A be ManySortedSet of I; ::_thesis: for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J
let B be ManySortedSet of J; ::_thesis: Intersect (A,B) is ManySortedSet of I /\ J
 ( dom A = I & dom B = J ) by PARTFUN1:def_2;
then  dom (Intersect (A,B)) = I /\ J by Def2;
hence  Intersect (A,B) is ManySortedSet of I /\ J by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum
end;

theorem Th15: :: YELLOW20:15
for I, J being set
for A being ManySortedSet of I
for B being Function
for C being ManySortedSet of J st C = Intersect (A,B) holds
C cc= A
proof
let I, J be set ; ::_thesis: for A being ManySortedSet of I
for B being Function
for C being ManySortedSet of J st C = Intersect (A,B) holds
C cc= A
let A be ManySortedSet of I; ::_thesis: for B being Function
for C being ManySortedSet of J st C = Intersect (A,B) holds
C cc= A
let B be Function; ::_thesis: for C being ManySortedSet of J st C = Intersect (A,B) holds
C cc= A
let C be ManySortedSet of J; ::_thesis: ( C = Intersect (A,B) implies C cc= A )
assume A1: C = Intersect (A,B) ; ::_thesis: C cc= A
A2: dom A = I by PARTFUN1:def_2;
 dom C = J by PARTFUN1:def_2;
then A3: J = I /\ (dom B) by A1, A2, Def2;
hence  J c= I by XBOOLE_1:17; :: according to ALTCAT_2:def_2 ::_thesis: for b1 being set holds
( not b1 in J or C . b1 c= A . b1 )
let i be set ; ::_thesis: ( not i in J or C . i c= A . i )
assume  i in J ; ::_thesis: C . i c= A . i
then  C . i = (A . i) /\ (B . i) by A1, A2, A3, Def2;
hence  C . i c= A . i by XBOOLE_1:17; ::_thesis: verum
end;

theorem Th16: :: YELLOW20:16
for I1, I2 being set
for A1, B1 being ManySortedSet of I1
for A2, B2 being ManySortedSet of I2
for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
proof
let I1, I2 be set ; ::_thesis: for A1, B1 being ManySortedSet of I1
for A2, B2 being ManySortedSet of I2
for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
let A1, B1 be ManySortedSet of I1; ::_thesis: for A2, B2 being ManySortedSet of I2
for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
let A2, B2 be ManySortedSet of I2; ::_thesis: for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
let A, B be ManySortedSet of I1 /\ I2; ::_thesis: ( A = Intersect (A1,A2) & B = Intersect (B1,B2) implies for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B )
assume A1: ( A = Intersect (A1,A2) & B = Intersect (B1,B2) ) ; ::_thesis: for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
let F be ManySortedFunction of A1,B1; ::_thesis: for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
let G be ManySortedFunction of A2,B2; ::_thesis: ( ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) implies Intersect (F,G) is ManySortedFunction of A,B )
assume A2: for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ; ::_thesis: Intersect (F,G) is ManySortedFunction of A,B
A3: ( dom B1 = I1 & dom B2 = I2 ) by PARTFUN1:def_2;
reconsider H = Intersect (F,G) as ManySortedSet of I1 /\ I2 by Th14;
A4: ( dom F = I1 & dom G = I2 ) by PARTFUN1:def_2;
A5: ( dom A1 = I1 & dom A2 = I2 ) by PARTFUN1:def_2;
 H is ManySortedFunction of A,B
proof
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I1 /\ I2 or H . i is M2( bool [:(A . i),(B . i):]) )
assume A6: i in I1 /\ I2 ; ::_thesis: H . i is M2( bool [:(A . i),(B . i):])
then A7: H . i = (F . i) /\ (G . i) by A4, Def2;
A8: i in I2 by A6, XBOOLE_0:def_4;
then A9: G . i is Function of (A2 . i),(B2 . i) by PBOOLE:def_15;
A10: ( A . i = (A1 . i) /\ (A2 . i) & B . i = (B1 . i) /\ (B2 . i) ) by A1, A5, A3, A6, Def2;
A11: i in I1 by A6, XBOOLE_0:def_4;
then  F . i is Function of (A1 . i),(B1 . i) by PBOOLE:def_15;
hence  H . i is M2( bool [:(A . i),(B . i):]) by A2, A4, A11, A8, A10, A7, A9, FUNCT_2:120; ::_thesis: verum
end;
hence  Intersect (F,G) is ManySortedFunction of A,B ; ::_thesis: verum
end;

theorem Th17: :: YELLOW20:17
for I, J being set
for F being ManySortedSet of [:I,I:]
for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
proof
let I, J be set ; ::_thesis: for F being ManySortedSet of [:I,I:]
for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
let F be ManySortedSet of [:I,I:]; ::_thesis: for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
let G be ManySortedSet of [:J,J:]; ::_thesis: ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
A1: [:(I /\ J),(I /\ J):] = [:I,I:] /\ [:J,J:] by ZFMISC_1:100;
then reconsider H = Intersect (F,G) as ManySortedSet of [:(I /\ J),(I /\ J):] by Th14;
 ( [:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:] ) by ZFMISC_1:def_3;
then A2: [:I,I,I:] /\ [:J,J,J:] = [:[:(I /\ J),(I /\ J):],(I /\ J):] by A1, ZFMISC_1:100
.= [:(I /\ J),(I /\ J),(I /\ J):] by ZFMISC_1:def_3 ;
A3: ( dom F = [:I,I:] & dom G = [:J,J:] ) by PARTFUN1:def_2;
A4: now__::_thesis:_for_x_being_set_st_x_in_[:I,I,I:]_/\_[:J,J,J:]_holds_
{|H|}_._x_=_({|F|}_._x)_/\_({|G|}_._x)
let x be set ; ::_thesis: ( x in [:I,I,I:] /\ [:J,J,J:] implies {|H|} . x = ({|F|} . x) /\ ({|G|} . x) )
assume A5: x in [:I,I,I:] /\ [:J,J,J:] ; ::_thesis: {|H|} . x = ({|F|} . x) /\ ({|G|} . x)
then A6: x in [:J,J,J:] by XBOOLE_0:def_4;
 x in [:I,I,I:] by A5, XBOOLE_0:def_4;
then consider a, b, c being set  such that
A7: a in I and
A8: b in I and
A9: c in I and
A10: x = [a,b,c] by MCART_1:68;
A11: c in J by A6, A10, MCART_1:69;
then A12: c in I /\ J by A9, XBOOLE_0:def_4;
A13: a in J by A6, A10, MCART_1:69;
then A14: a in I /\ J by A7, XBOOLE_0:def_4;
then A15: [a,c] in [:(I /\ J),(I /\ J):] by A12, ZFMISC_1:87;
A16: b in J by A6, A10, MCART_1:69;
then A17: {|G|} . (a,b,c) = G . (a,c) by A13, A11, ALTCAT_1:def_3;
A18: {|F|} . (a,b,c) = F . (a,c) by A7, A8, A9, ALTCAT_1:def_3;
 b in I /\ J by A8, A16, XBOOLE_0:def_4;
then  {|H|} . (a,b,c) = H . (a,c) by A14, A12, ALTCAT_1:def_3;
hence {|H|} . x = H . [a,c] by A10, MULTOP_1:def_1
.= (F . (a,c)) /\ (G . [a,c]) by A1, A3, A15, Def2
.= ({|F|} . x) /\ (G . (a,c)) by A10, A18, MULTOP_1:def_1
.= ({|F|} . x) /\ ({|G|} . x) by A10, A17, MULTOP_1:def_1 ;
::_thesis: verum
end;
take  H ; ::_thesis: ( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
thus  H = Intersect (F,G) ; ::_thesis: Intersect ({|F|},{|G|}) = {|H|}
A19: dom {|H|} = [:(I /\ J),(I /\ J),(I /\ J):] by PARTFUN1:def_2;
 ( dom {|F|} = [:I,I,I:] & dom {|G|} = [:J,J,J:] ) by PARTFUN1:def_2;
hence  Intersect ({|F|},{|G|}) = {|H|} by A19, A2, A4, Def2; ::_thesis: verum
end;

theorem Th18: :: YELLOW20:18
for I, J being set
for F1, F2 being ManySortedSet of [:I,I:]
for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
proof
let I, J be set ; ::_thesis: for F1, F2 being ManySortedSet of [:I,I:]
for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
let F1, F2 be ManySortedSet of [:I,I:]; ::_thesis: for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
let G1, G2 be ManySortedSet of [:J,J:]; ::_thesis: ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
A1: ( dom F2 = [:I,I:] & dom G2 = [:J,J:] ) by PARTFUN1:def_2;
A2: [:(I /\ J),(I /\ J):] = [:I,I:] /\ [:J,J:] by ZFMISC_1:100;
then reconsider H1 = Intersect (F1,G1), H2 = Intersect (F2,G2) as ManySortedSet of [:(I /\ J),(I /\ J):] by Th14;
 ( [:I,I,I:] = [:[:I,I:],I:] & [:J,J,J:] = [:[:J,J:],J:] ) by ZFMISC_1:def_3;
then A3: [:I,I,I:] /\ [:J,J,J:] = [:[:(I /\ J),(I /\ J):],(I /\ J):] by A2, ZFMISC_1:100
.= [:(I /\ J),(I /\ J),(I /\ J):] by ZFMISC_1:def_3 ;
A4: ( dom F1 = [:I,I:] & dom G1 = [:J,J:] ) by PARTFUN1:def_2;
A5: now__::_thesis:_for_x_being_set_st_x_in_[:I,I,I:]_/\_[:J,J,J:]_holds_
{|H1,H2|}_._x_=_({|F1,F2|}_._x)_/\_({|G1,G2|}_._x)
let x be set ; ::_thesis: ( x in [:I,I,I:] /\ [:J,J,J:] implies {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x) )
assume A6: x in [:I,I,I:] /\ [:J,J,J:] ; ::_thesis: {|H1,H2|} . x = ({|F1,F2|} . x) /\ ({|G1,G2|} . x)
then A7: x in [:J,J,J:] by XBOOLE_0:def_4;
 x in [:I,I,I:] by A6, XBOOLE_0:def_4;
then consider a, b, c being set  such that
A8: a in I and
A9: b in I and
A10: c in I and
A11: x = [a,b,c] by MCART_1:68;
A12: b in J by A7, A11, MCART_1:69;
then A13: b in I /\ J by A9, XBOOLE_0:def_4;
A14: c in J by A7, A11, MCART_1:69;
then A15: c in I /\ J by A10, XBOOLE_0:def_4;
then A16: [b,c] in [:(I /\ J),(I /\ J):] by A13, ZFMISC_1:87;
A17: a in J by A7, A11, MCART_1:69;
then A18: a in I /\ J by A8, XBOOLE_0:def_4;
then A19: [a,b] in [:(I /\ J),(I /\ J):] by A13, ZFMISC_1:87;
A20: {|F1,F2|} . (a,b,c) = [:(F2 . (b,c)),(F1 . (a,b)):] by A8, A9, A10, ALTCAT_1:def_4;
A21: {|G1,G2|} . (a,b,c) = [:(G2 . (b,c)),(G1 . (a,b)):] by A17, A12, A14, ALTCAT_1:def_4;
 {|H1,H2|} . (a,b,c) = [:(H2 . (b,c)),(H1 . (a,b)):] by A18, A13, A15, ALTCAT_1:def_4;
hence {|H1,H2|} . x = [:(H2 . (b,c)),(H1 . (a,b)):] by A11, MULTOP_1:def_1
.= [:((F2 . [b,c]) /\ (G2 . [b,c])),(H1 . (a,b)):] by A2, A1, A16, Def2
.= [:((F2 . [b,c]) /\ (G2 . [b,c])),((F1 . [a,b]) /\ (G1 . [a,b])):] by A2, A4, A19, Def2
.= [:(F2 . [b,c]),(F1 . [a,b]):] /\ [:(G2 . [b,c]),(G1 . [a,b]):] by ZFMISC_1:100
.= ({|F1,F2|} . x) /\ [:(G2 . [b,c]),(G1 . [a,b]):] by A11, A20, MULTOP_1:def_1
.= ({|F1,F2|} . x) /\ ({|G1,G2|} . x) by A11, A21, MULTOP_1:def_1 ;
::_thesis: verum
end;
take  H1 ; ::_thesis: ex H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
take  H2 ; ::_thesis: ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
thus  ( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) ) ; ::_thesis: Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|}
A22: dom {|H1,H2|} = [:(I /\ J),(I /\ J),(I /\ J):] by PARTFUN1:def_2;
 ( dom {|F1,F2|} = [:I,I,I:] & dom {|G1,G2|} = [:J,J,J:] ) by PARTFUN1:def_2;
hence  Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} by A22, A3, A5, Def2; ::_thesis: verum
end;

definition
let A, B be AltCatStr ;
assume B1: A,B have_the_same_composition ;
func Intersect (A,B) ->  strict AltCatStr  means :Def3: :: YELLOW20:def 3
( the carrier of it = the carrier of A /\ the carrier of B & the Arrows of it = Intersect ( the Arrows of A, the Arrows of B) & the Comp of it = Intersect ( the Comp of A, the Comp of B) );
existence
 ex b1 being strict AltCatStr st
( the carrier of b1 = the carrier of A /\ the carrier of B & the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b1 = Intersect ( the Comp of A, the Comp of B) )
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Comp_of_A_&_x_in_dom_the_Comp_of_B_holds_
the_Comp_of_A_._x_tolerates_the_Comp_of_B_._x
let x be set ; ::_thesis: ( x in dom the Comp of A & x in dom the Comp of B implies the Comp of A . x tolerates the Comp of B . x )
assume A2: x in dom the Comp of A ; ::_thesis: ( x in dom the Comp of B implies the Comp of A . x tolerates the Comp of B . x )
assume  x in dom the Comp of B ; ::_thesis: the Comp of A . x tolerates the Comp of B . x
 ex a1, a2, a3 being set st
( a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & x = [a1,a2,a3] ) by A2, MCART_1:68;
hence  the Comp of A . x tolerates the Comp of B . x by B1, Def1; ::_thesis: verum
end;
set Cr = the carrier of A /\ the carrier of B;
A3: [: the carrier of B, the carrier of B, the carrier of B:] = [:[: the carrier of B, the carrier of B:], the carrier of B:] by ZFMISC_1:def_3;
 ( [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] = [: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:] & [: the carrier of A, the carrier of A, the carrier of A:] = [:[: the carrier of A, the carrier of A:], the carrier of A:] ) by ZFMISC_1:100, ZFMISC_1:def_3;
then A4: [: the carrier of A, the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B, the carrier of B:] = [:[:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):],( the carrier of A /\ the carrier of B):] by A3, ZFMISC_1:100
.= [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] by ZFMISC_1:def_3 ;
consider Ar being ManySortedSet of [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] such that
A5: Ar = Intersect ( the Arrows of A, the Arrows of B) and
A6: Intersect ({| the Arrows of A|},{| the Arrows of B|}) = {|Ar|} by Th17;
 ex Ar1, Ar2 being ManySortedSet of [:( the carrier of A /\ the carrier of B),( the carrier of A /\ the carrier of B):] st
( Ar1 = Intersect ( the Arrows of A, the Arrows of B) & Ar2 = Intersect ( the Arrows of A, the Arrows of B) & Intersect ({| the Arrows of A, the Arrows of A|},{| the Arrows of B, the Arrows of B|}) = {|Ar1,Ar2|} ) by Th18;
then reconsider Cm = Intersect ( the Comp of A, the Comp of B) as ManySortedFunction of {|Ar,Ar|},{|Ar|} by A5, A6, A4, A1, Th16;
take  AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) ; ::_thesis: ( the carrier of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = the carrier of A /\ the carrier of B & the Arrows of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Arrows of A, the Arrows of B) & the Comp of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Comp of A, the Comp of B) )
thus  ( the carrier of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = the carrier of A /\ the carrier of B & the Arrows of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Arrows of A, the Arrows of B) & the Comp of AltCatStr(# ( the carrier of A /\ the carrier of B),Ar,Cm #) = Intersect ( the Comp of A, the Comp of B) ) by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict AltCatStr st the carrier of b1 = the carrier of A /\ the carrier of B & the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b1 = Intersect ( the Comp of A, the Comp of B) & the carrier of b2 = the carrier of A /\ the carrier of B & the Arrows of b2 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b2 = Intersect ( the Comp of A, the Comp of B) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines Intersect YELLOW20:def_3_:_
 for A, B being AltCatStr st A,B have_the_same_composition holds
for b3 being strict AltCatStr holds
( b3 = Intersect (A,B) iff ( the carrier of b3 = the carrier of A /\ the carrier of B & the Arrows of b3 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b3 = Intersect ( the Comp of A, the Comp of B) ) );

theorem :: YELLOW20:19
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) = Intersect (B,A)
proof
let A, B be AltCatStr ; ::_thesis: ( A,B have_the_same_composition implies Intersect (A,B) = Intersect (B,A) )
set AB = Intersect (A,B);
assume A1: A,B have_the_same_composition ; ::_thesis: Intersect (A,B) = Intersect (B,A)
then A2: the Comp of (Intersect (A,B)) = Intersect ( the Comp of A, the Comp of B) by Def3;
 ( the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B & the Arrows of (Intersect (A,B)) = Intersect ( the Arrows of A, the Arrows of B) ) by A1, Def3;
hence  Intersect (A,B) = Intersect (B,A) by A1, A2, Def3; ::_thesis: verum
end;

theorem Th20: :: YELLOW20:20
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is SubCatStr of A
proof
let A, B be AltCatStr ; ::_thesis: ( A,B have_the_same_composition implies Intersect (A,B) is SubCatStr of A )
set AB = Intersect (A,B);
assume A1: A,B have_the_same_composition ; ::_thesis: Intersect (A,B) is SubCatStr of A
then A2: the Comp of (Intersect (A,B)) = Intersect ( the Comp of A, the Comp of B) by Def3;
 ( the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B & the Arrows of (Intersect (A,B)) = Intersect ( the Arrows of A, the Arrows of B) ) by A1, Def3;
hence  ( the carrier of (Intersect (A,B)) c= the carrier of A & the Arrows of (Intersect (A,B)) cc= the Arrows of A & the Comp of (Intersect (A,B)) cc= the Comp of A ) by A2, Th15, XBOOLE_1:17; :: according to ALTCAT_2:def_11 ::_thesis: verum
end;

theorem Th21: :: YELLOW20:21
for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
proof
let A, B be AltCatStr ; ::_thesis: ( A,B have_the_same_composition implies for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A1: A,B have_the_same_composition ; ::_thesis: for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
 the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by A1, Def3;
then A2: [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] = [: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:] by ZFMISC_1:100;
let a1, a2 be object of A; ::_thesis: for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let b1, b2 be object of B; ::_thesis: for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let o1, o2 be object of (Intersect (A,B)); ::_thesis: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 implies <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A3: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; ::_thesis: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
A4: now__::_thesis:_(_the_carrier_of_A_<>_{}_&_the_carrier_of_B_<>_{}_implies_[o1,o2]_in_[:_the_carrier_of_(Intersect_(A,B)),_the_carrier_of_(Intersect_(A,B)):]_)
assume  ( the carrier of A <> {} & the carrier of B <> {} ) ; ::_thesis: [o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):]
then  ( [a1,a2] in [: the carrier of A, the carrier of A:] & [b1,b2] in [: the carrier of B, the carrier of B:] ) by ZFMISC_1:def_2;
hence  [o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] by A3, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
A5: ( dom the Arrows of A = [: the carrier of A, the carrier of A:] & dom the Arrows of B = [: the carrier of B, the carrier of B:] ) by PARTFUN1:def_2;
A6: now__::_thesis:_(_(_the_carrier_of_A_=_{}_or_the_carrier_of_B_=_{}_)_implies_(_(_the_Arrows_of_A_._[a1,a2])_/\_(_the_Arrows_of_B_._[b1,b2])_=_{}_&_the_Arrows_of_(Intersect_(A,B))_._[o1,o2]_=_{}_)_)
assume  ( the carrier of A = {} or the carrier of B = {} ) ; ::_thesis: ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} )
then A7: ( [: the carrier of A, the carrier of A:] = {} or [: the carrier of B, the carrier of B:] = {} ) by ZFMISC_1:90;
then  ( the Arrows of A . [a1,a2] = {} or the Arrows of B . [b1,b2] = {} ) ;
hence  ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} ) by A2, A7; ::_thesis: verum
end;
 the Arrows of (Intersect (A,B)) = Intersect ( the Arrows of A, the Arrows of B) by A1, Def3;
hence  <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A3, A2, A5, A4, A6, Def2; ::_thesis: verum
end;

theorem Th22: :: YELLOW20:22
for A, B being transitive AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is transitive
proof
let A, B be transitive AltCatStr ; ::_thesis: ( A,B have_the_same_composition implies Intersect (A,B) is transitive )
set AB = Intersect (A,B);
assume A1: A,B have_the_same_composition ; ::_thesis: Intersect (A,B) is transitive
then A2: the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by Def3;
let o1, o2, o3 be object of (Intersect (A,B)); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume that
A3: <^o1,o2^> <> {} and
A4: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
 ( dom the Arrows of (Intersect (A,B)) = [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] & [o1,o2] in dom the Arrows of (Intersect (A,B)) ) by A3, FUNCT_1:def_2, PARTFUN1:def_2;
then A5: o1 in the carrier of (Intersect (A,B)) by ZFMISC_1:87;
then reconsider A = A, B = B as non empty transitive AltCatStr by A2, XBOOLE_0:def_4;
reconsider b1 = o1, b2 = o2, b3 = o3 as object of B by A2, A5, XBOOLE_0:def_4;
reconsider a1 = o1, a2 = o2, a3 = o3 as object of A by A2, A5, XBOOLE_0:def_4;
set f = the Morphism of o1,o2;
set g = the Morphism of o2,o3;
A6: <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> by A1, Th21;
then A7: ( the Morphism of o2,o3 in <^a2,a3^> & the Morphism of o2,o3 in <^b2,b3^> ) by A4, XBOOLE_0:def_4;
A8: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;
then reconsider f1 = the Morphism of o1,o2 as Morphism of a1,a2 by A3, XBOOLE_0:def_4;
reconsider g2 = the Morphism of o2,o3 as Morphism of b2,b3 by A4, A6, XBOOLE_0:def_4;
reconsider g1 = the Morphism of o2,o3 as Morphism of a2,a3 by A4, A6, XBOOLE_0:def_4;
reconsider f2 = the Morphism of o1,o2 as Morphism of b1,b2 by A3, A8, XBOOLE_0:def_4;
 ( the Morphism of o1,o2 in <^a1,a2^> & the Morphism of o1,o2 in <^b1,b2^> ) by A3, A8, XBOOLE_0:def_4;
then A9: g1 * f1 = g2 * f2 by A1, A7, Th11;
A10: <^b2,b3^> <> {} by A4, A6;
A11: <^a2,a3^> <> {} by A4, A6;
 <^b1,b2^> <> {} by A3, A8;
then A12: <^b1,b3^> <> {} by A10, ALTCAT_1:def_2;
 <^a1,a2^> <> {} by A3, A8;
then A13: <^a1,a3^> <> {} by A11, ALTCAT_1:def_2;
 <^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by A1, Th21;
hence  not <^o1,o3^> = {} by A13, A12, A9, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th23: :: YELLOW20:23
for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>
proof
let A, B be AltCatStr ; ::_thesis: ( A,B have_the_same_composition implies for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^> )
assume A1: A,B have_the_same_composition ; ::_thesis: for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>
let a1, a2 be object of A; ::_thesis: for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>
let b1, b2 be object of B; ::_thesis: for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>
let o1, o2 be object of (Intersect (A,B)); ::_thesis: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^> )
assume  ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; ::_thesis: ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^> )
then  <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;
hence  ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^> ) by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: YELLOW20:24
for A, B being non empty with_units AltCatStr st A,B have_the_same_composition holds
for a being object of A
for b being object of B
for o being object of (Intersect (A,B)) st o = a & o = b & idm a = idm b holds
idm a in <^o,o^> by Th23;

theorem :: YELLOW20:25
for A, B being category st A,B have_the_same_composition & not Intersect (A,B) is empty & ( for a being object of A
for b being object of B st a = b holds
idm a = idm b ) holds
Intersect (A,B) is subcategory of A
proof
let A, B be category; ::_thesis: ( A,B have_the_same_composition & not Intersect (A,B) is empty & ( for a being object of A
for b being object of B st a = b holds
idm a = idm b ) implies Intersect (A,B) is subcategory of A )
assume that
A1: A,B have_the_same_composition and
A2: not Intersect (A,B) is empty and
A3: for a being object of A
for b being object of B st a = b holds
idm a = idm b ; ::_thesis: Intersect (A,B) is subcategory of A
reconsider AB = Intersect (A,B) as non empty transitive SubCatStr of A by A1, A2, Th20, Th22;
A4: the carrier of AB = the carrier of A /\ the carrier of B by A1, Def3;
now__::_thesis:_for_o_being_object_of_AB
for_a_being_object_of_A_st_o_=_a_holds_
idm_a_in_<^o,o^>
let o be object of AB; ::_thesis: for a being object of A st o = a holds
idm a in <^o,o^>
let a be object of A; ::_thesis: ( o = a implies idm a in <^o,o^> )
reconsider b = o as object of B by A4, XBOOLE_0:def_4;
assume A5: o = a ; ::_thesis: idm a in <^o,o^>
then  idm a = idm b by A3;
hence  idm a in <^o,o^> by A1, A5, Th23; ::_thesis: verum
end;
hence  Intersect (A,B) is subcategory of A by ALTCAT_2:def_14; ::_thesis: verum
end;

begin

scheme :: YELLOW20:sch 1
SubcategoryUniq{ F1() ->  category, F2() ->  non empty subcategory of F1(), F3() ->  non empty subcategory of F1(), P1[ set ], P2[ set , set , set ] } :
 AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #)
provided
A1: for a being object of F1() holds
( a is object of F2() iff P1[a] ) and
A2: for a, b being object of F1()
for a9, b9 being object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] ) and
A3: for a being object of F1() holds
( a is object of F3() iff P1[a] ) and
A4: for a, b being object of F1()
for a9, b9 being object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
proof
A5: the carrier of F2() c= the carrier of F1() by ALTCAT_2:def_11;
A6: the carrier of F3() c= the carrier of F1() by ALTCAT_2:def_11;
A7: the carrier of F2() = the carrier of F3()
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of F3() c= the carrier of F2()
let x be set ; ::_thesis: ( x in the carrier of F2() implies x in the carrier of F3() )
assume A8: x in the carrier of F2() ; ::_thesis: x in the carrier of F3()
then reconsider a = x as object of F2() ;
reconsider a = a as object of F1() by A5, A8;
 P1[a] by A1;
then  a is object of F3() by A3;
hence  x in the carrier of F3() ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of F3() or x in the carrier of F2() )
assume A9: x in the carrier of F3() ; ::_thesis: x in the carrier of F2()
then reconsider a = x as object of F3() ;
reconsider a = a as object of F1() by A6, A9;
 P1[a] by A3;
then  a is object of F2() by A1;
hence  x in the carrier of F2() ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_Element_of_F2()_holds_the_Arrows_of_F2()_._(a,b)_=_the_Arrows_of_F3()_._(a,b)
let a, b be Element of F2(); ::_thesis: the Arrows of F2() . (a,b) = the Arrows of F3() . (a,b)
reconsider x1 = a, y1 = b as object of F2() ;
reconsider x2 = x1, y2 = y1 as object of F3() by A7;
 ( x1 in the carrier of F2() & y1 in the carrier of F2() ) ;
then reconsider a9 = a, b9 = b as object of F1() by A5;
A10: <^x2,y2^> c= <^a9,b9^> by ALTCAT_2:31;
A11: <^x2,y2^> c= <^x1,y1^>
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in <^x2,y2^> or f in <^x1,y1^> )
assume A12: f in <^x2,y2^> ; ::_thesis: f in <^x1,y1^>
then reconsider f = f as Morphism of a9,b9 by A10;
 P2[a9,b9,f] by A4, A10, A12;
hence  f in <^x1,y1^> by A2, A10, A12; ::_thesis: verum
end;
A13: <^x1,y1^> c= <^a9,b9^> by ALTCAT_2:31;
 <^x1,y1^> c= <^x2,y2^>
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in <^x1,y1^> or f in <^x2,y2^> )
assume A14: f in <^x1,y1^> ; ::_thesis: f in <^x2,y2^>
then reconsider f = f as Morphism of a9,b9 by A13;
 P2[a9,b9,f] by A2, A13, A14;
hence  f in <^x2,y2^> by A4, A13, A14; ::_thesis: verum
end;
hence  the Arrows of F2() . (a,b) = the Arrows of F3() . (a,b) by A11, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #) by A7, ALTCAT_1:7, ALTCAT_2:26; ::_thesis: verum
end;

theorem Th26: :: YELLOW20:26
for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
proof
let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A holds
( B is full iff for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
let B be non empty SubCatStr of A; ::_thesis: ( B is full iff for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
thus  ( B is full implies for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ) by ALTCAT_2:28; ::_thesis: ( ( for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ) implies B is full )
A1: the carrier of B c= the carrier of A by ALTCAT_2:def_11;
A2: dom the Arrows of B = [: the carrier of B, the carrier of B:] by PARTFUN1:def_2;
assume A3: for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ; ::_thesis: B is full
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Arrows_of_B_holds_
the_Arrows_of_B_._x_=_the_Arrows_of_A_._x
let x be set ; ::_thesis: ( x in dom the Arrows of B implies the Arrows of B . x = the Arrows of A . x )
assume  x in dom the Arrows of B ; ::_thesis: the Arrows of B . x = the Arrows of A . x
then consider b1, b2 being set  such that
A5: ( b1 in the carrier of B & b2 in the carrier of B ) and
A6: x = [b1,b2] by ZFMISC_1:def_2;
reconsider b1 = b1, b2 = b2 as object of B by A5;
reconsider a1 = b1, a2 = b2 as object of A by A1, A5;
thus  the Arrows of B . x = <^b1,b2^> by A6
.= <^a1,a2^> by A3
.= the Arrows of A . x by A6 ; ::_thesis: verum
end;
A7: dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
 [: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A1, XBOOLE_1:28, ZFMISC_1:96;
hence  the Arrows of B = the Arrows of A || the carrier of B by A7, A2, A4, FUNCT_1:46; :: according to ALTCAT_2:def_13 ::_thesis: verum
end;

scheme :: YELLOW20:sch 2
FullSubcategoryEx{ F1() ->  category, P1[ set ] } :
 ex B being non empty strict full subcategory of F1() st
for a being object of F1() holds
( a is object of B iff P1[a] )
provided
A1: ex a being object of F1() st P1[a]
proof
defpred S1[ set , set , set ] means verum;
A2: for a, b, c being object of F1() st P1[a] & P1[b] & P1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f] ;
A3: for a being object of F1() st P1[a] holds
S1[a,a, idm a] ;
A4: ex a being object of F1() st P1[a] by A1;
consider B being non empty strict subcategory of F1() such that
A5: for a being object of F1() holds
( a is object of B iff P1[a] ) and
A6: for a, b being object of F1()
for a9, b9 being object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) from YELLOW18:sch_7(A4, A2, A3);
now__::_thesis:_for_a1,_a2_being_object_of_F1()
for_b1,_b2_being_object_of_B_st_b1_=_a1_&_b2_=_a2_holds_
<^b1,b2^>_=_<^a1,a2^>
let a1, a2 be object of F1(); ::_thesis: for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>
let b1, b2 be object of B; ::_thesis: ( b1 = a1 & b2 = a2 implies <^b1,b2^> = <^a1,a2^> )
assume A7: ( b1 = a1 & b2 = a2 ) ; ::_thesis: <^b1,b2^> = <^a1,a2^>
A8: <^a1,a2^> c= <^b1,b2^>
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in <^a1,a2^> or f in <^b1,b2^> )
assume  f in <^a1,a2^> ; ::_thesis: f in <^b1,b2^>
hence  f in <^b1,b2^> by A6, A7; ::_thesis: verum
end;
 <^b1,b2^> c= <^a1,a2^> by A7, ALTCAT_2:31;
hence  <^b1,b2^> = <^a1,a2^> by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
then  B is full by Th26;
hence  ex B being non empty strict full subcategory of F1() st
for a being object of F1() holds
( a is object of B iff P1[a] ) by A5; ::_thesis: verum
end;

scheme :: YELLOW20:sch 3
FullSubcategoryUniq{ F1() ->  category, F2() ->  non empty full subcategory of F1(), F3() ->  non empty full subcategory of F1(), P1[ set ] } :
 AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #)
provided
A1: for a being object of F1() holds
( a is object of F2() iff P1[a] ) and
A2: for a being object of F1() holds
( a is object of F3() iff P1[a] )
proof
A3: for a being object of F1() holds
( a is object of F3() iff P1[a] ) by A2;
defpred S1[ set , set , set ] means verum;
A4: now__::_thesis:_for_a,_b_being_object_of_F1()
for_a9,_b9_being_object_of_F2()_st_a9_=_a_&_b9_=_b_&_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_
(_f_in_<^a9,b9^>_iff_S1[a,b,f]_)
let a, b be object of F1(); ::_thesis: for a9, b9 being object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )
let a9, b9 be object of F2(); ::_thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )
assume  ( a9 = a & b9 = b ) ; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )
then  <^a9,b9^> = <^a,b^> by Th26;
hence  ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) ) ; ::_thesis: verum
end;
A5: now__::_thesis:_for_a,_b_being_object_of_F1()
for_a9,_b9_being_object_of_F3()_st_a9_=_a_&_b9_=_b_&_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_
(_f_in_<^a9,b9^>_iff_S1[a,b,f]_)
let a, b be object of F1(); ::_thesis: for a9, b9 being object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )
let a9, b9 be object of F3(); ::_thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )
assume  ( a9 = a & b9 = b ) ; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )
then  <^a9,b9^> = <^a,b^> by Th26;
hence  ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) ) ; ::_thesis: verum
end;
A6: for a being object of F1() holds
( a is object of F2() iff P1[a] ) by A1;
thus  AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #) from YELLOW20:sch_1(A6, A4, A3, A5); ::_thesis: verum
end;

begin

registration
let f be Function-yielding Function;
let x, y be set ;
clusterf . (x,y) ->  Relation-like Function-like ;
coherence
 ( f . (x,y) is Relation-like & f . (x,y) is Function-like ) ;
end;

theorem Th27: :: YELLOW20:27
for A being category
for C being non empty subcategory of A
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
proof
let A be category; ::_thesis: for C being non empty subcategory of A
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
let C be non empty subcategory of A; ::_thesis: for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
let a, b be object of C; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (incl C) . f = f )
assume A1: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds (incl C) . f = f
let f be Morphism of a,b; ::_thesis: (incl C) . f = f
A2: ( the MorphMap of (incl C) = id the Arrows of C & [a,b] in [: the carrier of C, the carrier of C:] ) by FUNCTOR0:def_28, ZFMISC_1:def_2;
 <^((incl C) . a),((incl C) . b)^> <> {} by A1, FUNCTOR0:28, XBOOLE_1:3;
hence (incl C) . f = (Morph-Map ((incl C),a,b)) . f by A1, FUNCTOR0:def_15
.= (id ( the Arrows of C . (a,b))) . f by A2, MSUALG_3:def_1
.= f by A1, FUNCT_1:18 ;
::_thesis: verum
end;

registration
let A be category;
let C be non empty subcategory of A;
cluster incl C ->  id-preserving comp-preserving ;
coherence
 ( incl C is id-preserving & incl C is comp-preserving )
proof
thus  incl C is id-preserving ::_thesis: incl C is comp-preserving
proof
let a be object of C; :: according to FUNCTOR0:def_20 ::_thesis: (Morph-Map ((incl C),a,a)) . (idm a) = idm ((incl C) . a)
A1: (incl C) . a = a by FUNCTOR0:27;
thus (Morph-Map ((incl C),a,a)) . (idm a) = (incl C) . (idm a) by FUNCTOR0:def_15
.= idm a by Th27
.= idm ((incl C) . a) by A1, ALTCAT_2:34 ; ::_thesis: verum
end;
let o1, o2, o3 be object of C; :: according to FUNCTOR0:def_23 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (incl C) . (b2 * b1) = ((incl C) . b2) * ((incl C) . b1) )
assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; ::_thesis: for b1 being M2(<^o1,o2^>)
for b2 being M2(<^o2,o3^>) holds (incl C) . (b2 * b1) = ((incl C) . b2) * ((incl C) . b1)
let f be Morphism of o1,o2; ::_thesis: for b1 being M2(<^o2,o3^>) holds (incl C) . (b1 * f) = ((incl C) . b1) * ((incl C) . f)
let g be Morphism of o2,o3; ::_thesis: (incl C) . (g * f) = ((incl C) . g) * ((incl C) . f)
 <^o1,o3^> <> {} by A2, ALTCAT_1:def_2;
then A3: ( (incl C) . o3 = o3 & (incl C) . (g * f) = g * f ) by Th27, FUNCTOR0:27;
A4: ( (incl C) . o1 = o1 & (incl C) . o2 = o2 ) by FUNCTOR0:27;
 ( (incl C) . g = g & (incl C) . f = f ) by A2, Th27;
hence  (incl C) . (g * f) = ((incl C) . g) * ((incl C) . f) by A2, A4, A3, ALTCAT_2:32; ::_thesis: verum
end;
end;

registration
let A be category;
let C be non empty subcategory of A;
cluster incl C ->  Covariant ;
coherence
 incl C is Covariant ;
end;

definition
let A be category;
let C be non empty subcategory of A;
:: original: incl
redefine func incl C ->  strict covariant Functor of C,A;
coherence
 incl C is strict covariant Functor of C,A by FUNCTOR0:def_25;
end;

definition
let A, B be category;
let C be non empty subcategory of A;
let F be covariant Functor of A,B;
:: original: |
redefine funcF | C ->  strict covariant Functor of C,B;
coherence
 F | C is strict covariant Functor of C,B
proof
 F | C = F * (incl C) ;
hence  F | C is strict covariant Functor of C,B ; ::_thesis: verum
end;
end;

definition
let A, B be category;
let C be non empty subcategory of A;
let F be contravariant Functor of A,B;
:: original: |
redefine funcF | C ->  strict contravariant Functor of C,B;
coherence
 F | C is strict contravariant Functor of C,B
proof
 F | C = F * (incl C) ;
hence  F | C is strict contravariant Functor of C,B ; ::_thesis: verum
end;
end;

theorem Th28: :: YELLOW20:28
for A, B being category
for C being non empty subcategory of A
for F being FunctorStr over A,B
for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
proof
let A, B be category; ::_thesis: for C being non empty subcategory of A
for F being FunctorStr over A,B
for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
let C be non empty subcategory of A; ::_thesis: for F being FunctorStr over A,B
for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
let F be FunctorStr over A,B; ::_thesis: for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
let b be object of A; ::_thesis: for c being object of C st c = b holds
(F | C) . c = F . b
let a be object of C; ::_thesis: ( a = b implies (F | C) . a = F . b )
assume  a = b ; ::_thesis: (F | C) . a = F . b
then  (incl C) . a = b by FUNCTOR0:27;
hence  (F | C) . a = F . b by FUNCTOR0:33; ::_thesis: verum
end;

theorem Th29: :: YELLOW20:29
for A, B being category
for C being non empty subcategory of A
for F being covariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
proof
let A, B be category; ::_thesis: for C being non empty subcategory of A
for F being covariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let C be non empty subcategory of A; ::_thesis: for F being covariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let F be covariant Functor of A,B; ::_thesis: for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let a, b be object of A; ::_thesis: for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let c, d be object of C; ::_thesis: ( c = a & d = b & <^c,d^> <> {} implies for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f )
assume that
A1: ( c = a & d = b ) and
A2: <^c,d^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let f be Morphism of a,b; ::_thesis: for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let g be Morphism of c,d; ::_thesis: ( g = f implies (F | C) . g = F . f )
assume  g = f ; ::_thesis: (F | C) . g = F . f
then A3: (incl C) . g = f by A2, Th27;
 ( (incl C) . c = a & (incl C) . d = b ) by A1, FUNCTOR0:27;
hence  (F | C) . g = F . f by A2, A3, FUNCTOR3:6; ::_thesis: verum
end;

theorem Th30: :: YELLOW20:30
for A, B being category
for C being non empty subcategory of A
for F being contravariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
proof
let A, B be category; ::_thesis: for C being non empty subcategory of A
for F being contravariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let C be non empty subcategory of A; ::_thesis: for F being contravariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let F be contravariant Functor of A,B; ::_thesis: for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let a, b be object of A; ::_thesis: for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let c, d be object of C; ::_thesis: ( c = a & d = b & <^c,d^> <> {} implies for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f )
assume that
A1: ( c = a & d = b ) and
A2: <^c,d^> <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let f be Morphism of a,b; ::_thesis: for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let g be Morphism of c,d; ::_thesis: ( g = f implies (F | C) . g = F . f )
assume  g = f ; ::_thesis: (F | C) . g = F . f
then A3: (incl C) . g = f by A2, Th27;
 ( (incl C) . c = a & (incl C) . d = b ) by A1, FUNCTOR0:27;
hence  (F | C) . g = F . f by A2, A3, FUNCTOR3:8; ::_thesis: verum
end;

theorem Th31: :: YELLOW20:31
for A, B being non empty AltGraph
for F being BimapStr over A,B st F is Covariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proof
let A, B be non empty AltGraph ; ::_thesis: for F being BimapStr over A,B st F is Covariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
let F be BimapStr over A,B; ::_thesis: ( F is Covariant & F is one-to-one implies for a, b being object of A st F . a = F . b holds
a = b )
given f being Function of the carrier of A, the carrier of B such that A1: the ObjectMap of F = [:f,f:] ; :: according to FUNCTOR0:def_1,FUNCTOR0:def_12 ::_thesis: ( not F is one-to-one or for a, b being object of A st F . a = F . b holds
a = b )
assume  the ObjectMap of F is V7() ; :: according to FUNCTOR0:def_6 ::_thesis: for a, b being object of A st F . a = F . b holds
a = b
then A2: f is one-to-one by A1, FUNCTOR0:7;
let a, b be object of A; ::_thesis: ( F . a = F . b implies a = b )
assume A3: F . a = F . b ; ::_thesis: a = b
A4: ( [(f . a),(f . a)] `1 = f . a & [(f . b),(f . b)] `1 = f . b ) ;
 ( the ObjectMap of F . (a,a) = [(f . a),(f . a)] & the ObjectMap of F . (b,b) = [(f . b),(f . b)] ) by A1, FUNCT_3:75;
hence  a = b by A2, A3, A4, FUNCT_2:19; ::_thesis: verum
end;

theorem Th32: :: YELLOW20:32
for A, B being non empty reflexive AltGraph
for F being feasible Covariant FunctorStr over A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
proof
let A, B be non empty reflexive AltGraph ; ::_thesis: for F being feasible Covariant FunctorStr over A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let F be feasible Covariant FunctorStr over A,B; ::_thesis: ( F is faithful implies for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A1: for i being set
for f being Function st i in dom the MorphMap of F & the MorphMap of F . i = f holds
f is one-to-one ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A2: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F . f = F . g holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( F . f = F . g implies f = g )
 ( dom the MorphMap of F = [: the carrier of A, the carrier of A:] & [a,b] in [: the carrier of A, the carrier of A:] ) by PARTFUN1:def_2, ZFMISC_1:def_2;
then A3: Morph-Map (F,a,b) is one-to-one by A1;
A4: <^(F . a),(F . b)^> <> {} by A2, FUNCTOR0:def_18;
then  ( F . f = (Morph-Map (F,a,b)) . f & F . g = (Morph-Map (F,a,b)) . g ) by A2, FUNCTOR0:def_15;
hence  ( F . f = F . g implies f = g ) by A2, A4, A3, FUNCT_2:19; ::_thesis: verum
end;

theorem Th33: :: YELLOW20:33
for A, B being non empty AltGraph
for F being Covariant FunctorStr over A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
proof
let A, B be non empty AltGraph ; ::_thesis: for F being Covariant FunctorStr over A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
let F be Covariant FunctorStr over A,B; ::_thesis: ( F is surjective implies for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )
given f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A1: ( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def_32,FUNCTOR0:def_34 ::_thesis: ( not F is onto or for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )
assume A2: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] ; :: according to FUNCTOR0:def_7,FUNCT_2:def_3 ::_thesis: for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
let a, b be object of B; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )
assume A3: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
 the ObjectMap of F is Covariant by FUNCTOR0:def_12;
then consider g being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = [:g,g:] by FUNCTOR0:def_1;
let f be Morphism of a,b; ::_thesis: ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
 ( dom the ObjectMap of F = [: the carrier of A, the carrier of A:] & [a,b] in rng the ObjectMap of F ) by A2, FUNCT_2:def_1, ZFMISC_1:def_2;
then consider x being set  such that
A5: x in [: the carrier of A, the carrier of A:] and
A6: [a,b] = the ObjectMap of F . x by FUNCT_1:def_3;
consider c, d being set  such that
A7: ( c in the carrier of A & d in the carrier of A ) and
A8: [c,d] = x by A5, ZFMISC_1:def_2;
reconsider c = c, d = d as object of A by A7;
 the ObjectMap of F . (d,d) = [(g . d),(g . d)] by A4, FUNCT_3:75;
then A9: F . d = g . d by MCART_1:7;
 the ObjectMap of F . (c,c) = [(g . c),(g . c)] by A4, FUNCT_3:75;
then  F . c = g . c by MCART_1:7;
then A10: the ObjectMap of F . (c,d) = [(F . c),(F . d)] by A4, A9, FUNCT_3:75;
rng (Morph-Map (F,c,d)) = ( the Arrows of B * the ObjectMap of F) . [c,d] by A1, A5, A8, MSUALG_3:def_3
.= <^a,b^> by A5, A6, A8, FUNCT_2:15 ;
then consider g being set  such that
A11: g in dom (Morph-Map (F,c,d)) and
A12: f = (Morph-Map (F,c,d)) . g by A3, FUNCT_1:def_3;
take  c ; ::_thesis: ex d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
take  d ; ::_thesis: ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
reconsider g = g as Morphism of c,d by A11;
take  g ; ::_thesis: ( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
thus  ( a = F . c & b = F . d & <^c,d^> <> {} ) by A6, A8, A10, A11, XTUPLE_0:1; ::_thesis: f = F . g
thus  f = F . g by A3, A6, A8, A10, A11, A12, FUNCTOR0:def_15; ::_thesis: verum
end;

theorem Th34: :: YELLOW20:34
for A, B being non empty AltGraph
for F being BimapStr over A,B st F is Contravariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proof
let A, B be non empty AltGraph ; ::_thesis: for F being BimapStr over A,B st F is Contravariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
let F be BimapStr over A,B; ::_thesis: ( F is Contravariant & F is one-to-one implies for a, b being object of A st F . a = F . b holds
a = b )
given f being Function of the carrier of A, the carrier of B such that A1: the ObjectMap of F = ~ [:f,f:] ; :: according to FUNCTOR0:def_2,FUNCTOR0:def_13 ::_thesis: ( not F is one-to-one or for a, b being object of A st F . a = F . b holds
a = b )
assume  the ObjectMap of F is V7() ; :: according to FUNCTOR0:def_6 ::_thesis: for a, b being object of A st F . a = F . b holds
a = b
then  [:f,f:] is V7() by A1, FUNCTOR0:9;
then A2: f is one-to-one by FUNCTOR0:7;
let a, b be object of A; ::_thesis: ( F . a = F . b implies a = b )
assume A3: F . a = F . b ; ::_thesis: a = b
A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
 [b,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
then  the ObjectMap of F . (b,b) = [:f,f:] . (b,b) by A1, A4, FUNCT_4:43;
then A5: the ObjectMap of F . (b,b) = [(f . b),(f . b)] by FUNCT_3:75;
 [a,a] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
then  the ObjectMap of F . (a,a) = [:f,f:] . (a,a) by A1, A4, FUNCT_4:43;
then A6: the ObjectMap of F . (a,a) = [(f . a),(f . a)] by FUNCT_3:75;
 ( [(f . a),(f . a)] `1 = f . a & [(f . b),(f . b)] `1 = f . b ) ;
hence  a = b by A2, A3, A6, A5, FUNCT_2:19; ::_thesis: verum
end;

theorem Th35: :: YELLOW20:35
for A, B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr over A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
proof
let A, B be non empty reflexive AltGraph ; ::_thesis: for F being feasible Contravariant FunctorStr over A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let F be feasible Contravariant FunctorStr over A,B; ::_thesis: ( F is faithful implies for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A1: for i being set
for f being Function st i in dom the MorphMap of F & the MorphMap of F . i = f holds
f is one-to-one ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A2: <^a,b^> <> {} ; ::_thesis: for f, g being Morphism of a,b st F . f = F . g holds
f = g
let f, g be Morphism of a,b; ::_thesis: ( F . f = F . g implies f = g )
 ( dom the MorphMap of F = [: the carrier of A, the carrier of A:] & [a,b] in [: the carrier of A, the carrier of A:] ) by PARTFUN1:def_2, ZFMISC_1:def_2;
then A3: Morph-Map (F,a,b) is one-to-one by A1;
A4: <^(F . b),(F . a)^> <> {} by A2, FUNCTOR0:def_19;
then  ( F . f = (Morph-Map (F,a,b)) . f & F . g = (Morph-Map (F,a,b)) . g ) by A2, FUNCTOR0:def_16;
hence  ( F . f = F . g implies f = g ) by A2, A4, A3, FUNCT_2:19; ::_thesis: verum
end;

theorem Th36: :: YELLOW20:36
for A, B being non empty AltGraph
for F being Contravariant FunctorStr over A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
proof
let A, B be non empty AltGraph ; ::_thesis: for F being Contravariant FunctorStr over A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
let F be Contravariant FunctorStr over A,B; ::_thesis: ( F is surjective implies for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g ) )
given f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A1: ( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def_32,FUNCTOR0:def_34 ::_thesis: ( not F is onto or for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g ) )
assume A2: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] ; :: according to FUNCTOR0:def_7,FUNCT_2:def_3 ::_thesis: for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
let a, b be object of B; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g ) )
assume A3: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
let f be Morphism of a,b; ::_thesis: ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
 ( dom the ObjectMap of F = [: the carrier of A, the carrier of A:] & [a,b] in rng the ObjectMap of F ) by A2, FUNCT_2:def_1, ZFMISC_1:def_2;
then consider x being set  such that
A4: x in [: the carrier of A, the carrier of A:] and
A5: [a,b] = the ObjectMap of F . x by FUNCT_1:def_3;
A6: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1;
 the ObjectMap of F is Contravariant by FUNCTOR0:def_13;
then consider g being Function of the carrier of A, the carrier of B such that
A7: the ObjectMap of F = ~ [:g,g:] by FUNCTOR0:def_2;
consider d, c being set  such that
A8: ( d in the carrier of A & c in the carrier of A ) and
A9: [d,c] = x by A4, ZFMISC_1:def_2;
reconsider c = c, d = d as object of A by A8;
 [c,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
then  the ObjectMap of F . (c,c) = [:g,g:] . (c,c) by A7, A6, FUNCT_4:43;
then  the ObjectMap of F . (c,c) = [(g . c),(g . c)] by FUNCT_3:75;
then A10: F . c = g . c by MCART_1:7;
 [d,d] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
then  the ObjectMap of F . (d,d) = [:g,g:] . (d,d) by A7, A6, FUNCT_4:43;
then  the ObjectMap of F . (d,d) = [(g . d),(g . d)] by FUNCT_3:75;
then A11: F . d = g . d by MCART_1:7;
 [d,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def_2;
then A12: the ObjectMap of F . (d,c) = [:g,g:] . (c,d) by A7, A6, FUNCT_4:43
.= [(F . c),(F . d)] by A10, A11, FUNCT_3:75 ;
rng (Morph-Map (F,d,c)) = ( the Arrows of B * the ObjectMap of F) . [d,c] by A1, A4, A9, MSUALG_3:def_3
.= <^a,b^> by A4, A5, A9, FUNCT_2:15 ;
then consider g being set  such that
A13: g in dom (Morph-Map (F,d,c)) and
A14: f = (Morph-Map (F,d,c)) . g by A3, FUNCT_1:def_3;
take  d ; ::_thesis: ex d being object of A ex g being Morphism of d,d st
( b = F . d & a = F . d & <^d,d^> <> {} & f = F . g )
take  c ; ::_thesis: ex g being Morphism of d,c st
( b = F . d & a = F . c & <^d,c^> <> {} & f = F . g )
reconsider g = g as Morphism of d,c by A13;
take  g ; ::_thesis: ( b = F . d & a = F . c & <^d,c^> <> {} & f = F . g )
thus  ( b = F . d & a = F . c & <^d,c^> <> {} ) by A5, A9, A12, A13, XTUPLE_0:1; ::_thesis: f = F . g
thus  f = F . g by A3, A5, A9, A12, A13, A14, FUNCTOR0:def_16; ::_thesis: verum
end;

begin

definition
let A, B be category;
let F be FunctorStr over A,B;
let A9, B9 be category;
predA9,B9 are_isomorphic_under F means :: YELLOW20:def 4
( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
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 (F,b,c)) . f ) ) );
predA9,B9 are_anti-isomorphic_under F means :: YELLOW20:def 5
( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
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 (F,b,c)) . f ) ) );
end;

:: deftheorem  defines are_isomorphic_under YELLOW20:def_4_:_
 for A, B being category
for F being FunctorStr over A,B
for A9, B9 being category holds
( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
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 (F,b,c)) . f ) ) ) );

:: deftheorem  defines are_anti-isomorphic_under YELLOW20:def_5_:_
 for A, B being category
for F being FunctorStr over A,B
for A9, B9 being category holds
( A9,B9 are_anti-isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
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 (F,b,c)) . f ) ) ) );

theorem :: YELLOW20:37
for A, B, A1, B1 being category
for F being FunctorStr over A,B st A1,B1 are_isomorphic_under F holds
A1,B1 are_isomorphic
proof
let A, B, A9, B9 be category; ::_thesis: for F being FunctorStr over A,B st A9,B9 are_isomorphic_under F holds
A9,B9 are_isomorphic
let F be FunctorStr over A,B; ::_thesis: ( A9,B9 are_isomorphic_under F implies A9,B9 are_isomorphic )
assume that
 A9 is subcategory of A and
 B9 is subcategory of B ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of A9,B9 holds
( not G is bijective or ex a9 being object of A9 ex a being object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of A9 ex b, c being object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or A9,B9 are_isomorphic )
given G being covariant Functor of A9,B9 such that A1: G is bijective and
 for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a and
 for b9, c9 being object of A9
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 (F,b,c)) . f ; ::_thesis: A9,B9 are_isomorphic
take  G ; :: according to FUNCTOR0:def_39 ::_thesis: ( G is bijective & G is covariant )
thus  ( G is bijective & G is covariant ) by A1; ::_thesis: verum
end;

theorem :: YELLOW20:38
for A, B, A1, B1 being category
for F being FunctorStr over A,B st A1,B1 are_anti-isomorphic_under F holds
A1,B1 are_anti-isomorphic
proof
let A, B, A9, B9 be category; ::_thesis: for F being FunctorStr over A,B st A9,B9 are_anti-isomorphic_under F holds
A9,B9 are_anti-isomorphic
let F be FunctorStr over A,B; ::_thesis: ( A9,B9 are_anti-isomorphic_under F implies A9,B9 are_anti-isomorphic )
assume that
 A9 is subcategory of A and
 B9 is subcategory of B ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of A9,B9 holds
( not G is bijective or ex a9 being object of A9 ex a being object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of A9 ex b, c being object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or A9,B9 are_anti-isomorphic )
given G being contravariant Functor of A9,B9 such that A1: G is bijective and
 for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a and
 for b9, c9 being object of A9
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 (F,b,c)) . f ; ::_thesis: A9,B9 are_anti-isomorphic
take  G ; :: according to FUNCTOR0:def_40 ::_thesis: ( G is bijective & G is contravariant )
thus  ( G is bijective & G is contravariant ) by A1; ::_thesis: verum
end;

theorem :: YELLOW20:39
for A, B being category
for F being covariant Functor of A,B st A,B are_isomorphic_under F holds
F is bijective
proof
let A, B be category; ::_thesis: for F being covariant Functor of A,B st A,B are_isomorphic_under F holds
F is bijective
let F be covariant Functor of A,B; ::_thesis: ( A,B are_isomorphic_under F implies F is bijective )
assume that
 A is subcategory of A and
 B is subcategory of B ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of A,B holds
( not G is bijective or ex a9, a being object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9, b, c being object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or F is bijective )
given G being covariant Functor of A,B such that A1: G is bijective and
A2: for a9, a being object of A st a9 = a holds
G . a9 = F . a and
A3: for b9, c9, 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 (F,b,c)) . f ; ::_thesis: F is bijective
 ( G is injective & G is surjective ) by A1, FUNCTOR0:def_35;
then A4: ( G is one-to-one & G is faithful & G is full & G is onto ) by FUNCTOR0:def_33, FUNCTOR0:def_34;
A5: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_F_._f_=_G_._f
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A6: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; ::_thesis: F . f = G . f
 <^(F . a),(F . b)^> <> {} by A6, FUNCTOR0:def_18;
hence F . f = (Morph-Map (F,a,b)) . f by A6, FUNCTOR0:def_15
.= G . f by A3, A6 ;
::_thesis: verum
end;
 for a being object of A holds F . a = G . a by A2;
then  FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #) by A5, YELLOW18:1;
hence  ( the ObjectMap of F is V7() & the MorphMap of F is "1-1" & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) & the ObjectMap of F is onto ) by A4, FUNCTOR0:def_6, FUNCTOR0:def_7, FUNCTOR0:def_30, FUNCTOR0:def_32; :: according to FUNCTOR0:def_6,FUNCTOR0:def_7,FUNCTOR0:def_30,FUNCTOR0:def_32,FUNCTOR0:def_33,FUNCTOR0:def_34,FUNCTOR0:def_35 ::_thesis: verum
end;

theorem :: YELLOW20:40
for A, B being category
for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective
proof
let A, B be category; ::_thesis: for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective
let F be contravariant Functor of A,B; ::_thesis: ( A,B are_anti-isomorphic_under F implies F is bijective )
assume that
 A is subcategory of A and
 B is subcategory of B ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of A,B holds
( not G is bijective or ex a9, a being object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9, b, c being object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or F is bijective )
given G being contravariant Functor of A,B such that A1: G is bijective and
A2: for a9, a being object of A st a9 = a holds
G . a9 = F . a and
A3: for b9, c9, 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 (F,b,c)) . f ; ::_thesis: F is bijective
 ( G is injective & G is surjective ) by A1, FUNCTOR0:def_35;
then A4: ( G is one-to-one & G is faithful & G is full & G is onto ) by FUNCTOR0:def_33, FUNCTOR0:def_34;
A5: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_F_._f_=_G_._f
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A6: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; ::_thesis: F . f = G . f
 <^(F . b),(F . a)^> <> {} by A6, FUNCTOR0:def_19;
hence F . f = (Morph-Map (F,a,b)) . f by A6, FUNCTOR0:def_16
.= G . f by A3, A6 ;
::_thesis: verum
end;
 for a being object of A holds F . a = G . a by A2;
then  FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #) by A5, YELLOW18:2;
hence  ( the ObjectMap of F is V7() & the MorphMap of F is "1-1" & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) & the ObjectMap of F is onto ) by A4, FUNCTOR0:def_6, FUNCTOR0:def_7, FUNCTOR0:def_30, FUNCTOR0:def_32; :: according to FUNCTOR0:def_6,FUNCTOR0:def_7,FUNCTOR0:def_30,FUNCTOR0:def_32,FUNCTOR0:def_33,FUNCTOR0:def_34,FUNCTOR0:def_35 ::_thesis: verum
end;

theorem :: YELLOW20:41
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
proof
let A, B be category; ::_thesis: for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
let F be covariant Functor of A,B; ::_thesis: ( F is bijective implies A,B are_isomorphic_under F )
assume A1: F is bijective ; ::_thesis: A,B are_isomorphic_under F
 ( the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B ) ;
hence  ( A is subcategory of A & B is subcategory of B ) by ALTCAT_2:20, ALTCAT_4:35; :: according to YELLOW20:def_4 ::_thesis: ex G being covariant Functor of A,B st
( G is bijective & ( for a9, a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9, 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 (F,b,c)) . f ) )
take  F ; ::_thesis: ( F is bijective & ( for a9, a being object of A st a9 = a holds
F . a9 = F . a ) & ( for b9, c9, 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
F . f9 = (Morph-Map (F,b,c)) . f ) )
thus  ( F is bijective & ( for a9, a being object of A st a9 = a holds
F . a9 = F . a ) ) by A1; ::_thesis: for b9, c9, 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
F . f9 = (Morph-Map (F,b,c)) . f
let b9, c9 be object of A; ::_thesis: 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
F . f9 = (Morph-Map (F,b,c)) . f
let b, c be object of A; ::_thesis: ( <^b9,c9^> <> {} & b9 = b & c9 = c implies for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f )
assume A2: ( <^b9,c9^> <> {} & b9 = b & c9 = c ) ; ::_thesis: for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f
then  <^(F . b),(F . c)^> <> {} by FUNCTOR0:def_18;
hence  for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f by A2, FUNCTOR0:def_15; ::_thesis: verum
end;

theorem :: YELLOW20:42
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
A,B are_anti-isomorphic_under F
proof
let A, B be category; ::_thesis: for F being contravariant Functor of A,B st F is bijective holds
A,B are_anti-isomorphic_under F
let F be contravariant Functor of A,B; ::_thesis: ( F is bijective implies A,B are_anti-isomorphic_under F )
assume A1: F is bijective ; ::_thesis: A,B are_anti-isomorphic_under F
 ( the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B ) ;
hence  ( A is subcategory of A & B is subcategory of B ) by ALTCAT_2:20, ALTCAT_4:35; :: according to YELLOW20:def_5 ::_thesis: ex G being contravariant Functor of A,B st
( G is bijective & ( for a9, a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9, 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 (F,b,c)) . f ) )
take  F ; ::_thesis: ( F is bijective & ( for a9, a being object of A st a9 = a holds
F . a9 = F . a ) & ( for b9, c9, 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
F . f9 = (Morph-Map (F,b,c)) . f ) )
thus  ( F is bijective & ( for a9, a being object of A st a9 = a holds
F . a9 = F . a ) ) by A1; ::_thesis: for b9, c9, 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
F . f9 = (Morph-Map (F,b,c)) . f
let b9, c9 be object of A; ::_thesis: 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
F . f9 = (Morph-Map (F,b,c)) . f
let b, c be object of A; ::_thesis: ( <^b9,c9^> <> {} & b9 = b & c9 = c implies for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f )
assume A2: ( <^b9,c9^> <> {} & b9 = b & c9 = c ) ; ::_thesis: for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f
then  <^(F . c),(F . b)^> <> {} by FUNCTOR0:def_19;
hence  for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f by A2, FUNCTOR0:def_16; ::_thesis: verum
end;

theorem :: YELLOW20:43
for A being category
for B being non empty subcategory of A holds B,B are_isomorphic_under id A
proof
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 ) )
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 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;
let b, c be object of B; ::_thesis: for b, c being object of A 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 ((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
end;

theorem Th44: :: YELLOW20:44
for f, g being Function st f c= g holds
~ f c= ~ g
proof
let f, g be Function; ::_thesis: ( f c= g implies ~ f c= ~ g )
assume A1: f c= g ; ::_thesis: ~ f c= ~ g
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in ~ f or [x,b1] in ~ g )
let y be set ; ::_thesis: ( not [x,y] in ~ f or [x,y] in ~ g )
assume A2: [x,y] in ~ f ; ::_thesis: [x,y] in ~ g
then  x in dom (~ f) by XTUPLE_0:def_12;
then consider z2, z1 being set  such that
A3: x = [z1,z2] and
A4: [z2,z1] in dom f by FUNCT_4:def_2;
y = (~ f) . (z1,z2) by A2, A3, FUNCT_1:1
.= f . (z2,z1) by A4, FUNCT_4:def_2 ;
then A5: [[z2,z1],y] in f by A4, FUNCT_1:1;
then A6: [z2,z1] in dom g by A1, FUNCT_1:1;
 y = g . (z2,z1) by A1, A5, FUNCT_1:1;
then A7: y = (~ g) . (z1,z2) by A6, FUNCT_4:def_2;
 x in dom (~ g) by A3, A6, FUNCT_4:def_2;
hence  [x,y] in ~ g by A3, A7, FUNCT_1:1; ::_thesis: verum
end;

theorem :: YELLOW20:45
for f, g being Function st dom f is Relation & ~ f c= ~ g holds
f c= g
proof
let f, g be Function; ::_thesis: ( dom f is Relation & ~ f c= ~ g implies f c= g )
assume  dom f is Relation ; ::_thesis: ( not ~ f c= ~ g or f c= g )
then reconsider R = dom f as Relation ;
 R c= [:(dom R),(rng R):] by RELAT_1:7;
then A1: ~ (~ f) = f by FUNCT_4:52;
assume  ~ f c= ~ g ; ::_thesis: f c= g
then  ( ~ (~ g) c= g & f c= ~ (~ g) ) by A1, Th44, FUNCT_4:51;
hence  f c= g by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th46: :: YELLOW20:46
for I, J being set
for A being ManySortedSet of [:I,I:]
for B being ManySortedSet of [:J,J:] st A cc= B holds
~ A cc= ~ B
proof
let I, J be set ; ::_thesis: for A being ManySortedSet of [:I,I:]
for B being ManySortedSet of [:J,J:] st A cc= B holds
~ A cc= ~ B
let A be ManySortedSet of [:I,I:]; ::_thesis: for B being ManySortedSet of [:J,J:] st A cc= B holds
~ A cc= ~ B
let B be ManySortedSet of [:J,J:]; ::_thesis: ( A cc= B implies ~ A cc= ~ B )
assume that
A1: [:I,I:] c= [:J,J:] and
A2: for x being set st x in [:I,I:] holds
A . x c= B . x ; :: according to ALTCAT_2:def_2 ::_thesis: ~ A cc= ~ B
thus  [:I,I:] c= [:J,J:] by A1; :: according to ALTCAT_2:def_2 ::_thesis: for b1 being set holds
( not b1 in [:I,I:] or (~ A) . b1 c= (~ B) . b1 )
let x be set ; ::_thesis: ( not x in [:I,I:] or (~ A) . x c= (~ B) . x )
assume  x in [:I,I:] ; ::_thesis: (~ A) . x c= (~ B) . x
then consider x1, x2 being set  such that
A3: ( x1 in I & x2 in I ) and
A4: x = [x1,x2] by ZFMISC_1:def_2;
A5: [x2,x1] in [:I,I:] by A3, ZFMISC_1:def_2;
 dom A = [:I,I:] by PARTFUN1:def_2;
then A6: (~ A) . (x1,x2) = A . (x2,x1) by A5, FUNCT_4:def_2;
 dom B = [:J,J:] by PARTFUN1:def_2;
then  (~ B) . (x1,x2) = B . (x2,x1) by A1, A5, FUNCT_4:def_2;
hence  (~ A) . x c= (~ B) . x by A2, A4, A5, A6; ::_thesis: verum
end;

theorem Th47: :: YELLOW20:47
for A being non empty transitive AltCatStr
for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp
proof
let A be non empty transitive AltCatStr ; ::_thesis: for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp
let B be non empty transitive SubCatStr of A; ::_thesis: B opp is SubCatStr of A opp
A1: B,B opp are_opposite by YELLOW18:def_4;
then A2: the carrier of (B opp) = the carrier of B by YELLOW18:def_3;
A3: the Arrows of (B opp) = ~ the Arrows of B by A1, YELLOW18:def_3;
A4: A,A opp are_opposite by YELLOW18:def_4;
then A5: the carrier of (A opp) = the carrier of A by YELLOW18:def_3;
hence  the carrier of (B opp) c= the carrier of (A opp) by A2, ALTCAT_2:def_11; :: according to ALTCAT_2:def_11 ::_thesis: ( the Arrows of (B opp) cc= the Arrows of (A opp) & the Comp of (B opp) cc= the Comp of (A opp) )
 ( the Arrows of B cc= the Arrows of A & the Arrows of (A opp) = ~ the Arrows of A ) by A4, ALTCAT_2:def_11, YELLOW18:def_3;
hence  the Arrows of (B opp) cc= the Arrows of (A opp) by A3, Th46; ::_thesis: the Comp of (B opp) cc= the Comp of (A opp)
A6: the carrier of B c= the carrier of A by ALTCAT_2:def_11;
hence  [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] c= [: the carrier of (A opp), the carrier of (A opp), the carrier of (A opp):] by A5, A2, MCART_1:73; :: according to ALTCAT_2:def_2 ::_thesis: for b1 being set holds
( not b1 in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] or the Comp of (B opp) . b1 c= the Comp of (A opp) . b1 )
let x be set ; ::_thesis: ( not x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] or the Comp of (B opp) . x c= the Comp of (A opp) . x )
assume  x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] ; ::_thesis: the Comp of (B opp) . x c= the Comp of (A opp) . x
then consider x1, x2, x3 being set  such that
A7: ( x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B ) and
A8: x = [x1,x2,x3] by A2, MCART_1:68;
reconsider a = x1, b = x2, c = x3 as object of B by A7;
reconsider a1 = a, b1 = b, c1 = c as object of A by A6, A7;
reconsider a19 = a1, b19 = b1, c19 = c1 as object of (A opp) by A4, YELLOW18:def_3;
A9: ( the Comp of B cc= the Comp of A & the Comp of B . (c,b,a) = the Comp of B . [c,b,a] ) by ALTCAT_2:def_11, MULTOP_1:def_1;
A10: the Comp of A . (c1,b1,a1) = the Comp of A . [c1,b1,a1] by MULTOP_1:def_1;
 [x3,x2,x1] in [: the carrier of B, the carrier of B, the carrier of B:] by A7, MCART_1:69;
then A11: the Comp of B . (c,b,a) c= the Comp of A . (c1,b1,a1) by A9, A10, ALTCAT_2:def_2;
reconsider a9 = a, b9 = b, c9 = c as object of (B opp) by A1, YELLOW18:def_3;
A12: ( the Comp of (B opp) . (a9,b9,c9) = the Comp of (B opp) . x & the Comp of (A opp) . (a19,b19,c19) = the Comp of (A opp) . x ) by A8, MULTOP_1:def_1;
A13: the Comp of (A opp) . (a19,b19,c19) = ~ ( the Comp of A . (c1,b1,a1)) by A4, YELLOW18:def_3;
 the Comp of (B opp) . (a9,b9,c9) = ~ ( the Comp of B . (c,b,a)) by A1, YELLOW18:def_3;
hence  the Comp of (B opp) . x c= the Comp of (A opp) . x by A13, A12, A11, Th44; ::_thesis: verum
end;

theorem Th48: :: YELLOW20:48
for A being category
for B being non empty subcategory of A holds B opp is subcategory of A opp
proof
let A be category; ::_thesis: for B being non empty subcategory of A holds B opp is subcategory of A opp
let B be non empty subcategory of A; ::_thesis: B opp is subcategory of A opp
reconsider BB = B opp as non empty transitive SubCatStr of A opp by Th47;
A1: A opp ,A are_opposite by YELLOW18:def_4;
A2: BB,B are_opposite by YELLOW18:def_4;
 BB is id-inheriting
proof
percases ( not BB is empty or BB is empty ) ;
:: according to ALTCAT_2:def_14
case not BB is empty ; ::_thesis: for b1 being M2( the carrier of BB)
for b2 being M2( the carrier of (A opp)) holds
( not b1 = b2 or idm b2 in <^b1,b1^> )
let o be object of BB; ::_thesis: for b1 being M2( the carrier of (A opp)) holds
( not o = b1 or idm b1 in <^o,o^> )
let o9 be object of (A opp); ::_thesis: ( not o = o9 or idm o9 in <^o,o^> )
reconsider a9 = o9 as object of A by A1, YELLOW18:def_3;
reconsider a = o as object of B by A2, YELLOW18:def_3;
assume  o = o9 ; ::_thesis: idm o9 in <^o,o^>
then  idm a9 in <^a,a^> by ALTCAT_2:def_14;
then  idm o9 in <^a,a^> by A1, YELLOW18:10;
hence  idm o9 in <^o,o^> by A2, YELLOW18:7; ::_thesis: verum
end;
case BB is empty ; ::_thesis: verum
end;
end;
end;
hence  B opp is subcategory of A opp ; ::_thesis: verum
end;

theorem :: YELLOW20:49
for A being category
for B being non empty subcategory of A holds B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))
proof
let A be category; ::_thesis: for B being non empty subcategory of A holds B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))
let B be non empty subcategory of A; ::_thesis: B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))
set F = dualizing-func (A,(A opp));
A1: B,B opp are_opposite by YELLOW18:def_4;
thus  ( B is subcategory of A & B opp is subcategory of A opp ) by Th48; :: according to YELLOW20:def_5 ::_thesis: ex G being contravariant Functor of B,B opp st
( G is bijective & ( for a9 being object of B
for a being object of A st a9 = a holds
G . a9 = (dualizing-func (A,(A opp))) . 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 ((dualizing-func (A,(A opp))),b,c)) . f ) )
take G = dualizing-func (B,(B opp)); ::_thesis: ( G is bijective & ( for a9 being object of B
for a being object of A st a9 = a holds
G . a9 = (dualizing-func (A,(A opp))) . 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 ((dualizing-func (A,(A opp))),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 = (dualizing-func (A,(A opp))) . 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 ((dualizing-func (A,(A opp))),b,c)) . f ) )
A2: A,A opp are_opposite by YELLOW18:def_4;
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 ((dualizing-func (A,(A opp))),b,c)) . f
let a be object of B; ::_thesis: for a1 being object of A st a = a1 holds
G . a = (dualizing-func (A,(A opp))) . a1
let a1 be object of A; ::_thesis: ( a = a1 implies G . a = (dualizing-func (A,(A opp))) . a1 )
assume  a = a1 ; ::_thesis: G . a = (dualizing-func (A,(A opp))) . a1
hence G . a = a1 by A1, YELLOW18:def_5
.= (dualizing-func (A,(A opp))) . a1 by A2, YELLOW18:def_5 ;
::_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 f9 being Morphism of b,c
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map ((dualizing-func (A,(A opp))),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 ((dualizing-func (A,(A opp))),b1,c1)) . f )
assume that
A3: <^b,c^> <> {} and
A4: ( 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 ((dualizing-func (A,(A opp))),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 ((dualizing-func (A,(A opp))),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies G . f = (Morph-Map ((dualizing-func (A,(A opp))),b1,c1)) . f1 )
assume A5: f = f1 ; ::_thesis: G . f = (Morph-Map ((dualizing-func (A,(A opp))),b1,c1)) . f1
A6: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A3, A4, ALTCAT_2:31;
then A7: <^((dualizing-func (A,(A opp))) . c1),((dualizing-func (A,(A opp))) . b1)^> <> {} by FUNCTOR0:def_19;
thus G . f = f by A1, A3, YELLOW18:def_5
.= (dualizing-func (A,(A opp))) . f1 by A2, A5, A6, YELLOW18:def_5
.= (Morph-Map ((dualizing-func (A,(A opp))),b1,c1)) . f1 by A6, A7, FUNCTOR0:def_16 ; ::_thesis: verum
end;

theorem :: YELLOW20:50
for A1, A2 being category
for F being covariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
proof
let A1, A2 be category; ::_thesis: for F being covariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
let F be covariant Functor of A1,A2; ::_thesis: ( F is bijective implies for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F " )
assume A1: F is bijective ; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then A2: F is coreflexive by FUNCTOR0:46;
 ex H being Functor of A2,A1 st
( H = F " & H is bijective & H is covariant ) by A1, FUNCTOR0:48;
then reconsider F9 = F " as covariant Functor of A2,A1 ;
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
let B2 be non empty subcategory of A2; ::_thesis: ( B1,B2 are_isomorphic_under F implies B2,B1 are_isomorphic_under F " )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or B2,B1 are_isomorphic_under F " )
given G being covariant Functor of B1,B2 such that A3: G is bijective and
A4: for a being object of B1
for a1 being object of A1 st a = a1 holds
G . a = F . a1 and
A5: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: B2,B1 are_isomorphic_under F "
 G is surjective by A3, FUNCTOR0:def_35;
then  G is onto by FUNCTOR0:def_34;
then A6: G is coreflexive by FUNCTOR0:46;
thus  ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def_4 ::_thesis: ex G being covariant Functor of B2,B1 st
( G is bijective & ( for a9 being object of B2
for a being object of A2 st a9 = a holds
G . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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 ) )
consider H being Functor of B2,B1 such that
A7: H = G " and
A8: ( H is bijective & H is covariant ) by A3, FUNCTOR0:48;
reconsider H = H as covariant Functor of B2,B1 by A8;
take  H ; ::_thesis: ( H is bijective & ( for a9 being object of B2
for a being object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
thus  H is bijective by A8; ::_thesis: ( ( for a9 being object of B2
for a being object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def_11;
hereby  ::_thesis: for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f
let a be object of B2; ::_thesis: for a1 being object of A2 st a = a1 holds
H . a = (F ") . a1
let a1 be object of A2; ::_thesis: ( a = a1 implies H . a = (F ") . a1 )
 H . a in the carrier of B1 ;
then reconsider Ha = H . a as object of A1 by A9;
 G . (H . a) = F . Ha by A4;
then A11: F . Ha = a by A3, A7, A6, Th1;
assume  a = a1 ; ::_thesis: H . a = (F ") . a1
hence  H . a = (F ") . a1 by A1, A2, A11, Th1; ::_thesis: verum
end;
let b, c be object of B2; ::_thesis: for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f
let b1, c1 be object of A2; ::_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
H . f9 = (Morph-Map ((F "),b1,c1)) . f )
assume that
A12: <^b,c^> <> {} and
A13: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
H . 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
H . f = (Morph-Map ((F "),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies H . f = (Morph-Map ((F "),b1,c1)) . f1 )
assume A14: f = f1 ; ::_thesis: H . f = (Morph-Map ((F "),b1,c1)) . f1
A15: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A12, A13, ALTCAT_2:31;
A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;
A17: <^(H . b),(H . c)^> <> {} by A12, FUNCTOR0:def_18;
then A18: H . f in <^(H . b),(H . c)^> ;
A19: ( F . ((F ") . b1) = b1 & F . ((F ") . c1) = c1 ) by A1, A2, Th1;
A20: ( H . b = (F ") . b1 & H . c = (F ") . c1 ) by A10, A13;
then A21: <^(H . b),(H . c)^> c= <^((F ") . b1),((F ") . c1)^> by ALTCAT_2:31;
then reconsider Hf = H . f as Morphism of ((F ") . b1),((F ") . c1) by A18;
G . (H . f) = (Morph-Map (F,((F ") . b1),((F ") . c1))) . Hf by A5, A20, A17
.= F . Hf by A21, A18, A15, A19, FUNCTOR0:def_15 ;
then  F . Hf = f by A3, A7, A17, A16, Th2;
hence H . f = F9 . f1 by A1, A14, A21, A18, A19, Th2
.= (Morph-Map ((F "),b1,c1)) . f1 by A21, A18, A15, FUNCTOR0:def_15 ;
::_thesis: verum
end;

theorem :: YELLOW20:51
for A1, A2 being category
for F being contravariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
proof
let A1, A2 be category; ::_thesis: for F being contravariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
let F be contravariant Functor of A1,A2; ::_thesis: ( F is bijective implies for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F " )
assume A1: F is bijective ; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then A2: F is coreflexive by FUNCTOR0:47;
 ex H being Functor of A2,A1 st
( H = F " & H is bijective & H is contravariant ) by A1, FUNCTOR0:49;
then reconsider F9 = F " as contravariant Functor of A2,A1 ;
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
let B2 be non empty subcategory of A2; ::_thesis: ( B1,B2 are_anti-isomorphic_under F implies B2,B1 are_anti-isomorphic_under F " )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or B2,B1 are_anti-isomorphic_under F " )
given G being contravariant Functor of B1,B2 such that A3: G is bijective and
A4: for a being object of B1
for a1 being object of A1 st a = a1 holds
G . a = F . a1 and
A5: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: B2,B1 are_anti-isomorphic_under F "
 G is surjective by A3, FUNCTOR0:def_35;
then  G is onto by FUNCTOR0:def_34;
then A6: G is coreflexive by FUNCTOR0:47;
thus  ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def_5 ::_thesis: ex G being contravariant Functor of B2,B1 st
( G is bijective & ( for a9 being object of B2
for a being object of A2 st a9 = a holds
G . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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 ) )
consider H being Functor of B2,B1 such that
A7: H = G " and
A8: ( H is bijective & H is contravariant ) by A3, FUNCTOR0:49;
reconsider H = H as contravariant Functor of B2,B1 by A8;
take  H ; ::_thesis: ( H is bijective & ( for a9 being object of B2
for a being object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
thus  H is bijective by A8; ::_thesis: ( ( for a9 being object of B2
for a being object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def_11;
hereby  ::_thesis: for b9, c9 being object of B2
for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f
let a be object of B2; ::_thesis: for a1 being object of A2 st a = a1 holds
H . a = (F ") . a1
let a1 be object of A2; ::_thesis: ( a = a1 implies H . a = (F ") . a1 )
 H . a in the carrier of B1 ;
then reconsider Ha = H . a as object of A1 by A9;
 G . (H . a) = F . Ha by A4;
then A11: F . Ha = a by A3, A7, A6, Th1;
assume  a = a1 ; ::_thesis: H . a = (F ") . a1
hence  H . a = (F ") . a1 by A1, A2, A11, Th1; ::_thesis: verum
end;
let b, c be object of B2; ::_thesis: for b, c being object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f
let b1, c1 be object of A2; ::_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
H . f9 = (Morph-Map ((F "),b1,c1)) . f )
assume that
A12: <^b,c^> <> {} and
A13: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
H . 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
H . f = (Morph-Map ((F "),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies H . f = (Morph-Map ((F "),b1,c1)) . f1 )
assume A14: f = f1 ; ::_thesis: H . f = (Morph-Map ((F "),b1,c1)) . f1
A15: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A12, A13, ALTCAT_2:31;
A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;
A17: <^(H . c),(H . b)^> <> {} by A12, FUNCTOR0:def_19;
then A18: H . f in <^(H . c),(H . b)^> ;
A19: ( F . ((F ") . b1) = b1 & F . ((F ") . c1) = c1 ) by A1, A2, Th1;
A20: ( H . b = (F ") . b1 & H . c = (F ") . c1 ) by A10, A13;
then A21: <^(H . c),(H . b)^> c= <^((F ") . c1),((F ") . b1)^> by ALTCAT_2:31;
then reconsider Hf = H . f as Morphism of ((F ") . c1),((F ") . b1) by A18;
G . (H . f) = (Morph-Map (F,((F ") . c1),((F ") . b1))) . Hf by A5, A20, A17
.= F . Hf by A21, A18, A15, A19, FUNCTOR0:def_16 ;
then  F . Hf = f by A3, A7, A17, A16, Th3;
hence H . f = F9 . f1 by A1, A14, A21, A18, A19, Th3
.= (Morph-Map ((F "),b1,c1)) . f1 by A21, A18, A15, FUNCTOR0:def_16 ;
::_thesis: verum
end;

theorem :: YELLOW20:52
for A1, A2, A3 being category
for F being covariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proof
let A1, A2, A3 be category; ::_thesis: for F being covariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let F be covariant Functor of A1,A2; ::_thesis: for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let G be covariant Functor of A2,A3; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B2 be non empty subcategory of A2; ::_thesis: for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B3 be non empty subcategory of A3; ::_thesis: ( B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G implies B1,B3 are_isomorphic_under G * F )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or not B2,B3 are_isomorphic_under G or B1,B3 are_isomorphic_under G * F )
given F1 being covariant Functor of B1,B2 such that A1: F1 is bijective and
A2: for a being object of B1
for a1 being object of A1 st a = a1 holds
F1 . a = F . a1 and
A3: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
F1 . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: ( not B2,B3 are_isomorphic_under G or B1,B3 are_isomorphic_under G * F )
assume that
 B2 is subcategory of A2 and
 B3 is subcategory of A3 ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of B2,B3 holds
( not G is bijective or ex a9 being object of B2 ex a being object of A2 st
( a9 = a & not G . a9 = G . a ) or ex b9, c9 being object of B2 ex b, c being object of A2 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (G,b,c)) . f ) ) ) or B1,B3 are_isomorphic_under G * F )
given G1 being covariant Functor of B2,B3 such that A4: G1 is bijective and
A5: for a being object of B2
for a1 being object of A2 st a = a1 holds
G1 . a = G . a1 and
A6: for b, c being object of B2
for b1, c1 being object of A2 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G1 . f = (Morph-Map (G,b1,c1)) . f1 ; ::_thesis: B1,B3 are_isomorphic_under G * F
thus  ( B1 is subcategory of A1 & B3 is subcategory of A3 ) ; :: according to YELLOW20:def_4 ::_thesis: ex G being covariant Functor of B1,B3 st
( G is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
G . a9 = (G * 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 ((G * F),b,c)) . f ) )
take  G1 * F1 ; ::_thesis: ( G1 * F1 is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f ) )
thus  G1 * F1 is bijective by A1, A4, FUNCTOR1:12; ::_thesis: ( ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f
let a be object of B1; ::_thesis: for b being object of A1 st a = b holds
(G1 * F1) . a = (G * F) . b
let b be object of A1; ::_thesis: ( a = b implies (G1 * F1) . a = (G * F) . b )
assume  a = b ; ::_thesis: (G1 * F1) . a = (G * F) . b
then  G1 . (F1 . a) = G . (F . b) by A2, A5;
hence (G1 * F1) . a = G . (F . b) by FUNCTOR0:33
.= (G * F) . b by FUNCTOR0:33 ;
::_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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:33;
let f be Morphism of b,c; ::_thesis: for f being Morphism of b1,c1 st f = f holds
(G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:31;
then A11: <^((G * F) . b1),((G * F) . c1)^> <> {} by FUNCTOR0:def_18;
A12: <^(F1 . b),(F1 . c)^> <> {} by A7, FUNCTOR0:def_18;
then A13: F1 . f in <^(F1 . b),(F1 . c)^> ;
A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;
then A15: <^(F1 . b),(F1 . c)^> c= <^(F . b1),(F . c1)^> by ALTCAT_2:31;
assume  f = f1 ; ::_thesis: (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1
then F1 . f = (Morph-Map (F,b1,c1)) . f1 by A3, A7, A8
.= F . f1 by A10, A13, A15, FUNCTOR0:def_15 ;
then  G1 . (F1 . f) = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A6, A12, A14;
hence (G1 * F1) . f = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A7, FUNCTOR3:6
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def_15
.= (G * F) . f1 by A10, FUNCTOR3:6
.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def_15 ;
::_thesis: verum
end;

theorem :: YELLOW20:53
for A1, A2, A3 being category
for F being contravariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proof
let A1, A2, A3 be category; ::_thesis: for F being contravariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let F be contravariant Functor of A1,A2; ::_thesis: for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let G be covariant Functor of A2,A3; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B2 be non empty subcategory of A2; ::_thesis: for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B3 be non empty subcategory of A3; ::_thesis: ( B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G implies B1,B3 are_anti-isomorphic_under G * F )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or not B2,B3 are_isomorphic_under G or B1,B3 are_anti-isomorphic_under G * F )
given F1 being contravariant Functor of B1,B2 such that A1: F1 is bijective and
A2: for a being object of B1
for a1 being object of A1 st a = a1 holds
F1 . a = F . a1 and
A3: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
F1 . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: ( not B2,B3 are_isomorphic_under G or B1,B3 are_anti-isomorphic_under G * F )
assume that
 B2 is subcategory of A2 and
 B3 is subcategory of A3 ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of B2,B3 holds
( not G is bijective or ex a9 being object of B2 ex a being object of A2 st
( a9 = a & not G . a9 = G . a ) or ex b9, c9 being object of B2 ex b, c being object of A2 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (G,b,c)) . f ) ) ) or B1,B3 are_anti-isomorphic_under G * F )
given G1 being covariant Functor of B2,B3 such that A4: G1 is bijective and
A5: for a being object of B2
for a1 being object of A2 st a = a1 holds
G1 . a = G . a1 and
A6: for b, c being object of B2
for b1, c1 being object of A2 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G1 . f = (Morph-Map (G,b1,c1)) . f1 ; ::_thesis: B1,B3 are_anti-isomorphic_under G * F
thus  ( B1 is subcategory of A1 & B3 is subcategory of A3 ) ; :: according to YELLOW20:def_5 ::_thesis: ex G being contravariant Functor of B1,B3 st
( G is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
G . a9 = (G * 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 ((G * F),b,c)) . f ) )
take  G1 * F1 ; ::_thesis: ( G1 * F1 is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f ) )
thus  G1 * F1 is bijective by A1, A4, FUNCTOR1:12; ::_thesis: ( ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f
let a be object of B1; ::_thesis: for b being object of A1 st a = b holds
(G1 * F1) . a = (G * F) . b
let b be object of A1; ::_thesis: ( a = b implies (G1 * F1) . a = (G * F) . b )
assume  a = b ; ::_thesis: (G1 * F1) . a = (G * F) . b
then  G1 . (F1 . a) = G . (F . b) by A2, A5;
hence (G1 * F1) . a = G . (F . b) by FUNCTOR0:33
.= (G * F) . b by FUNCTOR0:33 ;
::_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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:33;
let f be Morphism of b,c; ::_thesis: for f being Morphism of b1,c1 st f = f holds
(G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:31;
then A11: <^((G * F) . c1),((G * F) . b1)^> <> {} by FUNCTOR0:def_19;
A12: <^(F1 . c),(F1 . b)^> <> {} by A7, FUNCTOR0:def_19;
then A13: F1 . f in <^(F1 . c),(F1 . b)^> ;
A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;
then A15: <^(F1 . c),(F1 . b)^> c= <^(F . c1),(F . b1)^> by ALTCAT_2:31;
assume  f = f1 ; ::_thesis: (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1
then F1 . f = (Morph-Map (F,b1,c1)) . f1 by A3, A7, A8
.= F . f1 by A10, A13, A15, FUNCTOR0:def_16 ;
then  G1 . (F1 . f) = (Morph-Map (G,(F . c1),(F . b1))) . (F . f1) by A6, A12, A14;
hence (G1 * F1) . f = (Morph-Map (G,(F . c1),(F . b1))) . (F . f1) by A7, FUNCTOR3:9
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def_15
.= (G * F) . f1 by A10, FUNCTOR3:9
.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def_16 ;
::_thesis: verum
end;

theorem :: YELLOW20:54
for A1, A2, A3 being category
for F being covariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proof
let A1, A2, A3 be category; ::_thesis: for F being covariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let F be covariant Functor of A1,A2; ::_thesis: for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let G be contravariant Functor of A2,A3; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B2 be non empty subcategory of A2; ::_thesis: for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
let B3 be non empty subcategory of A3; ::_thesis: ( B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G implies B1,B3 are_anti-isomorphic_under G * F )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_4 ::_thesis: ( for G being covariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or not B2,B3 are_anti-isomorphic_under G or B1,B3 are_anti-isomorphic_under G * F )
given F1 being covariant Functor of B1,B2 such that A1: F1 is bijective and
A2: for a being object of B1
for a1 being object of A1 st a = a1 holds
F1 . a = F . a1 and
A3: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
F1 . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: ( not B2,B3 are_anti-isomorphic_under G or B1,B3 are_anti-isomorphic_under G * F )
assume that
 B2 is subcategory of A2 and
 B3 is subcategory of A3 ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of B2,B3 holds
( not G is bijective or ex a9 being object of B2 ex a being object of A2 st
( a9 = a & not G . a9 = G . a ) or ex b9, c9 being object of B2 ex b, c being object of A2 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (G,b,c)) . f ) ) ) or B1,B3 are_anti-isomorphic_under G * F )
given G1 being contravariant Functor of B2,B3 such that A4: G1 is bijective and
A5: for a being object of B2
for a1 being object of A2 st a = a1 holds
G1 . a = G . a1 and
A6: for b, c being object of B2
for b1, c1 being object of A2 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G1 . f = (Morph-Map (G,b1,c1)) . f1 ; ::_thesis: B1,B3 are_anti-isomorphic_under G * F
thus  ( B1 is subcategory of A1 & B3 is subcategory of A3 ) ; :: according to YELLOW20:def_5 ::_thesis: ex G being contravariant Functor of B1,B3 st
( G is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
G . a9 = (G * 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 ((G * F),b,c)) . f ) )
take  G1 * F1 ; ::_thesis: ( G1 * F1 is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f ) )
thus  G1 * F1 is bijective by A1, A4, FUNCTOR1:12; ::_thesis: ( ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f
let a be object of B1; ::_thesis: for b being object of A1 st a = b holds
(G1 * F1) . a = (G * F) . b
let b be object of A1; ::_thesis: ( a = b implies (G1 * F1) . a = (G * F) . b )
assume  a = b ; ::_thesis: (G1 * F1) . a = (G * F) . b
then  G1 . (F1 . a) = G . (F . b) by A2, A5;
hence (G1 * F1) . a = G . (F . b) by FUNCTOR0:33
.= (G * F) . b by FUNCTOR0:33 ;
::_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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:33;
let f be Morphism of b,c; ::_thesis: for f being Morphism of b1,c1 st f = f holds
(G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:31;
then A11: <^((G * F) . c1),((G * F) . b1)^> <> {} by FUNCTOR0:def_19;
A12: <^(F1 . b),(F1 . c)^> <> {} by A7, FUNCTOR0:def_18;
then A13: F1 . f in <^(F1 . b),(F1 . c)^> ;
A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;
then A15: <^(F1 . b),(F1 . c)^> c= <^(F . b1),(F . c1)^> by ALTCAT_2:31;
assume  f = f1 ; ::_thesis: (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1
then F1 . f = (Morph-Map (F,b1,c1)) . f1 by A3, A7, A8
.= F . f1 by A10, A13, A15, FUNCTOR0:def_15 ;
then  G1 . (F1 . f) = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A6, A12, A14;
hence (G1 * F1) . f = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A7, FUNCTOR3:8
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def_16
.= (G * F) . f1 by A10, FUNCTOR3:8
.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def_16 ;
::_thesis: verum
end;

theorem :: YELLOW20:55
for A1, A2, A3 being category
for F being contravariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proof
let A1, A2, A3 be category; ::_thesis: for F being contravariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let F be contravariant Functor of A1,A2; ::_thesis: for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let G be contravariant Functor of A2,A3; ::_thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B1 be non empty subcategory of A1; ::_thesis: for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B2 be non empty subcategory of A2; ::_thesis: for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B3 be non empty subcategory of A3; ::_thesis: ( B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G implies B1,B3 are_isomorphic_under G * F )
assume that
 B1 is subcategory of A1 and
 B2 is subcategory of A2 ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of B1,B2 holds
( not G is bijective or ex a9 being object of B1 ex a being object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of B1 ex b, c being object of A1 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or not B2,B3 are_anti-isomorphic_under G or B1,B3 are_isomorphic_under G * F )
given F1 being contravariant Functor of B1,B2 such that A1: F1 is bijective and
A2: for a being object of B1
for a1 being object of A1 st a = a1 holds
F1 . a = F . a1 and
A3: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
F1 . f = (Morph-Map (F,b1,c1)) . f1 ; ::_thesis: ( not B2,B3 are_anti-isomorphic_under G or B1,B3 are_isomorphic_under G * F )
assume that
 B2 is subcategory of A2 and
 B3 is subcategory of A3 ; :: according to YELLOW20:def_5 ::_thesis: ( for G being contravariant Functor of B2,B3 holds
( not G is bijective or ex a9 being object of B2 ex a being object of A2 st
( a9 = a & not G . a9 = G . a ) or ex b9, c9 being object of B2 ex b, c being object of A2 st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (G,b,c)) . f ) ) ) or B1,B3 are_isomorphic_under G * F )
given G1 being contravariant Functor of B2,B3 such that A4: G1 is bijective and
A5: for a being object of B2
for a1 being object of A2 st a = a1 holds
G1 . a = G . a1 and
A6: for b, c being object of B2
for b1, c1 being object of A2 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G1 . f = (Morph-Map (G,b1,c1)) . f1 ; ::_thesis: B1,B3 are_isomorphic_under G * F
thus  ( B1 is subcategory of A1 & B3 is subcategory of A3 ) ; :: according to YELLOW20:def_4 ::_thesis: ex G being covariant Functor of B1,B3 st
( G is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
G . a9 = (G * 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 ((G * F),b,c)) . f ) )
take  G1 * F1 ; ::_thesis: ( G1 * F1 is bijective & ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f ) )
thus  G1 * F1 is bijective by A1, A4, FUNCTOR1:12; ::_thesis: ( ( for a9 being object of B1
for a being object of A1 st a9 = a holds
(G1 * F1) . a9 = (G * 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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f
let a be object of B1; ::_thesis: for b being object of A1 st a = b holds
(G1 * F1) . a = (G * F) . b
let b be object of A1; ::_thesis: ( a = b implies (G1 * F1) . a = (G * F) . b )
assume  a = b ; ::_thesis: (G1 * F1) . a = (G * F) . b
then  G1 . (F1 . a) = G . (F . b) by A2, A5;
hence (G1 * F1) . a = G . (F . b) by FUNCTOR0:33
.= (G * F) . b by FUNCTOR0:33 ;
::_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
(G1 * F1) . f9 = (Morph-Map ((G * 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; ::_thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:33;
let f be Morphism of b,c; ::_thesis: for f being Morphism of b1,c1 st f = f holds
(G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f
let f1 be Morphism of b1,c1; ::_thesis: ( f = f1 implies (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:31;
then A11: <^((G * F) . b1),((G * F) . c1)^> <> {} by FUNCTOR0:def_18;
A12: <^(F1 . c),(F1 . b)^> <> {} by A7, FUNCTOR0:def_19;
then A13: F1 . f in <^(F1 . c),(F1 . b)^> ;
A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;
then A15: <^(F1 . c),(F1 . b)^> c= <^(F . c1),(F . b1)^> by ALTCAT_2:31;
assume  f = f1 ; ::_thesis: (G1 * F1) . f = (Morph-Map ((G * F),b1,c1)) . f1
then F1 . f = (Morph-Map (F,b1,c1)) . f1 by A3, A7, A8
.= F . f1 by A10, A13, A15, FUNCTOR0:def_16 ;
then  G1 . (F1 . f) = (Morph-Map (G,(F . c1),(F . b1))) . (F . f1) by A6, A12, A14;
hence (G1 * F1) . f = (Morph-Map (G,(F . c1),(F . b1))) . (F . f1) by A7, FUNCTOR3:7
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def_16
.= (G * F) . f1 by A10, FUNCTOR3:7
.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def_15 ;
::_thesis: verum
end;

theorem :: YELLOW20:56
for A1, A2 being category
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
proof
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) ->  M2(<^((F | B1) . $1),((F | B1) . $2)^>) = (F | B1) . $3;
deffunc H2( object of B1) ->  M2( the carrier of A2) = (F | B1) . $1;
A4: ( F is injective & F is surjective ) by A1, FUNCTOR0:def_35;
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) )
 ( a in the carrier of B2 & b in the carrier of B2 ) ;
then 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 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: 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 A9, A11, Th28, Th29; ::_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
 a in the carrier of B1 ;
then 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))
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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  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, FUNCTOR0:def_33;
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
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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 A20, ALTCAT_2:31;
 g in <^a,b^> by A20;
then 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 A20, Th29
.= F . g1 by A20, Th29 ;
hence  f = g by A18, A21, Th32; ::_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
A25: c in the carrier of B1 ;
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then reconsider a1 = a, b1 = b, c1 = c as object of A1 by A12, A25;
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
A26: a9 = H2(a) and
A27: b9 = H2(b) and
A28: 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
A29: f9 = H1(a,b,f) and
A30: g9 = H1(b,c,g) ; ::_thesis: H1(a,c,g * f) = g9 * f9
A31: b9 = F . b1 by A27, Th28;
A32: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by A24, ALTCAT_2:31;
then reconsider g1 = g as Morphism of b1,c1 ;
A33: c9 = F . c1 by A28, Th28;
A34: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A23, ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1 ;
A35: a9 = F . a1 by A26, Th28;
A36: g9 = F . g1 by A24, A30, Th29;
then A37: g9 in <^b9,c9^> by A3, A32, A31, A33;
A38: f9 = F . f1 by A23, A29, Th29;
then A39: f9 in <^a9,b9^> by A3, A34, A35, A31;
 ( <^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 H1(a,c,g * f) = (F . g1) * (F . f1) by A34, A32, FUNCTOR0:def_23
.= g9 * f9 by A35, A31, A33, A38, A36, A39, A37, ALTCAT_2:32 ;
::_thesis: verum
end;
A40: 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 A41: a9 = H2(a) ; ::_thesis: H1(a,a, idm a) = idm a9
 a in the carrier of B1 ;
then reconsider a1 = a as object of A1 by A12;
thus H1(a,a, idm a) = F . (idm a1) by Th29, ALTCAT_2:34
.= idm (F . a1) by FUNCTOR2:1
.= idm a9 by A41, Th28, ALTCAT_2:34 ; ::_thesis: verum
end;
consider G being strict covariant Functor of B1,B2 such that
A42: for a being object of B1 holds G . a = H2(a) and
A43: 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 YELLOW18:sch_8(A13, A14, A22, A40);
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 ) )
A44: 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 )
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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 A18, Th31; ::_thesis: verum
end;
thus  G is bijective from YELLOW18:sch_10(A42, A43, A44, A19, A5); ::_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 A45: a = a1 ; ::_thesis: G . a = F . a1
thus G . a = (F | B1) . a by A42
.= F . a1 by A45, Th28 ; ::_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
A46: <^b,c^> <> {} and
A47: ( 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 A48: f = f1 ; ::_thesis: G . f = (Morph-Map (F,b1,c1)) . f1
A49: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A46, A47, ALTCAT_2:31;
then A50: <^(F . b1),(F . c1)^> <> {} by FUNCTOR0:def_18;
thus G . f = (F | B1) . f by A43, A46
.= F . f1 by A46, A47, A48, Th29
.= (Morph-Map (F,b1,c1)) . f1 by A49, A50, FUNCTOR0:def_15 ; ::_thesis: verum
end;
end;

theorem :: YELLOW20:57
for A1, A2 being category
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
proof
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
proof
deffunc H1( object of B1, object of B1, Morphism of $1,$2) ->  M2(<^((F | B1) . $2),((F | B1) . $1)^>) = (F | B1) . $3;
deffunc H2( object of B1) ->  M2( the carrier of A2) = (F | B1) . $1;
A4: ( F is injective & F is surjective ) by A1, FUNCTOR0:def_35;
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 = H2(c) & a = 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
( b = H2(c) & a = 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
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
 ( a in the carrier of B2 & b in the carrier of B2 ) ;
then 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 = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(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 = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take  d ; ::_thesis: ex g being Morphism of c,d st
( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
take  g ; ::_thesis: ( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) )
 g1 in <^c,d^> by A3, A7, A9, A10, A11;
hence  ( b = H2(c) & a = H2(d) & <^c,d^> <> {} & f = H1(c,d,g) ) by A9, A11, Th28, Th30; ::_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
 a in the carrier of B1 ;
then 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(b),H2(a))
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(b),H2(a)) )
assume A15: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds H1(a,b,f) in the Arrows of B2 . (H2(b),H2(a))
let f be Morphism of a,b; ::_thesis: H1(a,b,f) in the Arrows of B2 . (H2(b),H2(a))
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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  H1(a,b,f) in the Arrows of B2 . (H2(b),H2(a)) ; ::_thesis: verum
end;
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
( 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, FUNCTOR0:def_33;
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
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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 A20, ALTCAT_2:31;
 g in <^a,b^> by A20;
then 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 A20, Th30
.= F . g1 by A20, Th30 ;
hence  f = g by A18, A21, Th35; ::_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_b9,a9
for_g9_being_Morphism_of_c9,b9_st_f9_=_H1(a,b,f)_&_g9_=_H1(b,c,g)_holds_
H1(a,c,g_*_f)_=_f9_*_g9
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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(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 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(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 = H2(a) & b9 = H2(b) & c9 = H2(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9
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 b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9
A25: c in the carrier of B1 ;
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then reconsider a1 = a, b1 = b, c1 = c as object of A1 by A12, A25;
let a9, b9, c9 be object of B2; ::_thesis: ( a9 = H2(a) & b9 = H2(b) & c9 = H2(c) implies for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9 )
assume that
A26: a9 = H2(a) and
A27: b9 = H2(b) and
A28: c9 = H2(c) ; ::_thesis: for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9
let f9 be Morphism of b9,a9; ::_thesis: for g9 being Morphism of c9,b9 st f9 = H1(a,b,f) & g9 = H1(b,c,g) holds
H1(a,c,g * f) = f9 * g9
let g9 be Morphism of c9,b9; ::_thesis: ( f9 = H1(a,b,f) & g9 = H1(b,c,g) implies H1(a,c,g * f) = f9 * g9 )
assume that
A29: f9 = H1(a,b,f) and
A30: g9 = H1(b,c,g) ; ::_thesis: H1(a,c,g * f) = f9 * g9
A31: b9 = F . b1 by A27, Th28;
A32: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by A24, ALTCAT_2:31;
then reconsider g1 = g as Morphism of b1,c1 ;
A33: c9 = F . c1 by A28, Th28;
A34: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A23, ALTCAT_2:31;
then reconsider f1 = f as Morphism of a1,b1 ;
A35: a9 = F . a1 by A26, Th28;
A36: g9 = F . g1 by A24, A30, Th30;
then A37: g9 in <^c9,b9^> by A3, A32, A31, A33;
A38: f9 = F . f1 by A23, A29, Th30;
then A39: f9 in <^b9,a9^> by A3, A34, A35, A31;
 ( <^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 H1(a,c,g * f) = (F . f1) * (F . g1) by A34, A32, FUNCTOR0:def_24
.= f9 * g9 by A35, A31, A33, A38, A36, A39, A37, ALTCAT_2:32 ;
::_thesis: verum
end;
A40: 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 A41: a9 = H2(a) ; ::_thesis: H1(a,a, idm a) = idm a9
 a in the carrier of B1 ;
then reconsider a1 = a as object of A1 by A12;
thus H1(a,a, idm a) = F . (idm a1) by Th30, ALTCAT_2:34
.= idm (F . a1) by ALTCAT_4:13
.= idm a9 by A41, Th28, ALTCAT_2:34 ; ::_thesis: verum
end;
consider G being strict contravariant Functor of B1,B2 such that
A42: for a being object of B1 holds G . a = H2(a) and
A43: 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 YELLOW18:sch_9(A13, A14, A22, A40);
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 ) )
A44: 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 )
 ( a in the carrier of B1 & b in the carrier of B1 ) ;
then 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 A18, Th34; ::_thesis: verum
end;
thus  G is bijective from YELLOW18:sch_12(A42, A43, A44, A19, A5); ::_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 A45: a = a1 ; ::_thesis: G . a = F . a1
thus G . a = (F | B1) . a by A42
.= F . a1 by A45, Th28 ; ::_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
A46: <^b,c^> <> {} and
A47: ( 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 A48: f = f1 ; ::_thesis: G . f = (Morph-Map (F,b1,c1)) . f1
A49: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A46, A47, ALTCAT_2:31;
then A50: <^(F . c1),(F . b1)^> <> {} by FUNCTOR0:def_19;
thus G . f = (F | B1) . f by A43, A46
.= F . f1 by A46, A47, A48, Th30
.= (Morph-Map (F,b1,c1)) . f1 by A49, A50, FUNCTOR0:def_16 ; ::_thesis: verum
end;
end;