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