let A, B be category; :: thesis: for F, G being covariant Functor of A,B st ( for a being object of A holds F . a = G . a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #)
let F, G be covariant Functor of A,B; :: thesis: ( ( for a being object of A holds F . a = G . a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) implies FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #) )
assume that
A1:
for a being object of A holds F . a = G . a
and
A2:
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f
; :: thesis: FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #)
the ObjectMap of F is Covariant
by FUNCTOR0:def 13;
then consider ff being Function of the carrier of A,the carrier of B such that
A3:
the ObjectMap of F = [:ff,ff:]
by FUNCTOR0:def 2;
the ObjectMap of G is Covariant
by FUNCTOR0:def 13;
then consider gg being Function of the carrier of A,the carrier of B such that
A4:
the ObjectMap of G = [:gg,gg:]
by FUNCTOR0:def 2;
now let a,
b be
Element of
A;
:: thesis: the ObjectMap of F . a,b = the ObjectMap of G . a,breconsider x =
a,
y =
b as
object of
A ;
A5:
(
dom ff = the
carrier of
A &
dom gg = the
carrier of
A )
by FUNCT_2:def 1;
then
( the
ObjectMap of
F . x,
x = [(ff . x),(ff . x)] & the
ObjectMap of
F . y,
y = [(ff . y),(ff . y)] & the
ObjectMap of
G . x,
x = [(gg . x),(gg . x)] & the
ObjectMap of
G . y,
y = [(gg . y),(gg . y)] )
by A3, A4, FUNCT_3:def 9;
then A6:
(
F . x = ff . x &
F . y = ff . y &
G . x = gg . x &
G . y = gg . y )
by MCART_1:7;
A7:
(
F . x = G . x &
F . y = G . y )
by A1;
thus the
ObjectMap of
F . a,
b =
[(ff . a),(ff . b)]
by A3, A5, FUNCT_3:def 9
.=
the
ObjectMap of
G . a,
b
by A4, A5, A6, A7, FUNCT_3:def 9
;
:: thesis: verum end;
then A8:
the ObjectMap of F = the ObjectMap of G
by BINOP_1:2;
now let i be
set ;
:: thesis: ( i in [:the carrier of A,the carrier of A:] implies the MorphMap of F . i = the MorphMap of G . i )assume
i in [:the carrier of A,the carrier of A:]
;
:: thesis: the MorphMap of F . i = the MorphMap of G . ithen consider a,
b being
set such that A9:
(
a in the
carrier of
A &
b in the
carrier of
A &
i = [a,b] )
by ZFMISC_1:def 2;
reconsider x =
a,
y =
b as
object of
A by A9;
A10:
( (
<^x,y^> <> {} implies
<^(F . x),(F . y)^> <> {} ) & (
<^x,y^> <> {} implies
<^(G . x),(G . y)^> <> {} ) )
by FUNCTOR0:def 19;
then A11:
(
dom (Morph-Map F,x,y) = <^x,y^> &
dom (Morph-Map G,x,y) = <^x,y^> )
by FUNCT_2:def 1;
now let z be
set ;
:: thesis: ( z in <^x,y^> implies (Morph-Map F,x,y) . z = (Morph-Map G,x,y) . z )assume A12:
z in <^x,y^>
;
:: thesis: (Morph-Map F,x,y) . z = (Morph-Map G,x,y) . zthen reconsider f =
z as
Morphism of
x,
y ;
thus (Morph-Map F,x,y) . z =
F . f
by A10, A12, FUNCTOR0:def 16
.=
G . f
by A2, A12
.=
(Morph-Map G,x,y) . z
by A10, A12, FUNCTOR0:def 16
;
:: thesis: verum end; hence
the
MorphMap of
F . i = the
MorphMap of
G . i
by A9, A11, FUNCT_1:9;
:: thesis: verum end;
hence
FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #)
by A8, PBOOLE:3; :: thesis: verum