set A9 = Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);
set sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ;
set f = the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);
the Arrows of B * the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) in { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum }
;
then reconsider sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } as non empty set ;
defpred S1[ object , object ] means ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st
( $1 = [f,m] & $2 = FunctorStr(# f,m #) & $2 is covariant Functor of A,B );
defpred S2[ object , object ] means ex AA being ManySortedSet of [: the carrier of A, the carrier of A:] st
( $1 = AA & $2 = Funcs ( the Arrows of A,AA) );
A1:
for x, y, z being object st S2[x,y] & S2[x,z] holds
y = z
;
consider XX being set such that
A2:
for x being object holds
( x in XX iff ex y being object st
( y in sAA & S2[y,x] ) )
from TARSKI:sch 1(A1);
A3:
for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
object ;
( S1[x,y] & S1[x,z] implies y = z )
given f being
Covariant bifunction of the
carrier of
A, the
carrier of
B,
m being
MSUnTrans of
f, the
Arrows of
A, the
Arrows of
B such that A4:
x = [f,m]
and A5:
y = FunctorStr(#
f,
m #)
and
y is
covariant Functor of
A,
B
;
( not S1[x,z] or y = z )
given f1 being
Covariant bifunction of the
carrier of
A, the
carrier of
B,
m1 being
MSUnTrans of
f1, the
Arrows of
A, the
Arrows of
B such that A6:
x = [f1,m1]
and A7:
z = FunctorStr(#
f1,
m1 #)
and
z is
covariant Functor of
A,
B
;
y = z
f = f1
by A4, A6, XTUPLE_0:1;
hence
y = z
by A4, A5, A6, A7, XTUPLE_0:1;
verum
end;
consider X being set such that
A8:
for x being object holds
( x in X iff ex y being object st
( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & S1[y,x] ) )
from TARSKI:sch 1(A3);
take
X
; for x being object holds
( x in X iff x is strict covariant Functor of A,B )
let x be object ; ( x in X iff x is strict covariant Functor of A,B )
thus
( x in X implies x is strict covariant Functor of A,B )
( x is strict covariant Functor of A,B implies x in X )proof
assume
x in X
;
x is strict covariant Functor of A,B
then
ex
y being
object st
(
y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & ex
f being
Covariant bifunction of the
carrier of
A, the
carrier of
B ex
m being
MSUnTrans of
f, the
Arrows of
A, the
Arrows of
B st
(
y = [f,m] &
x = FunctorStr(#
f,
m #) &
x is
covariant Functor of
A,
B ) )
by A8;
hence
x is
strict covariant Functor of
A,
B
;
verum
end;
assume
x is strict covariant Functor of A,B
; x in X
then reconsider F = x as strict covariant Functor of A,B ;
reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A, the carrier of B by FUNCTOR0:def 12;
reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the Arrows of B ;
reconsider y = [f,m] as set by TARSKI:1;
A9:
for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds
the Arrows of B . (f . (o1,o2)) <> {}
A11:
for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds
the Arrows of B . [(F . o1),(F . o2)] <> {}
y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):]
proof
set I =
[: the carrier of A, the carrier of A:];
reconsider AA = the
Arrows of
B * f as
ManySortedSet of
[: the carrier of A, the carrier of A:] ;
A13:
for
i being
set st
i in [: the carrier of A, the carrier of A:] & the
Arrows of
A . i <> {} holds
the
Arrows of
B . (f . i) <> {}
proof
let i be
set ;
( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (f . i) <> {} )
assume that A14:
i in [: the carrier of A, the carrier of A:]
and A15:
the
Arrows of
A . i <> {}
;
the Arrows of B . (f . i) <> {}
consider o1,
o2 being
object such that A16:
(
o1 in the
carrier of
A &
o2 in the
carrier of
A )
and A17:
i = [o1,o2]
by A14, ZFMISC_1:def 2;
reconsider a1 =
o1,
a2 =
o2 as
Object of
A by A16;
A18: the
Arrows of
B . (f . i) =
the
Arrows of
B . (f . (o1,o2))
by A17
.=
the
Arrows of
B . [(F . a1),(F . a2)]
by FUNCTOR0:22
;
the
Arrows of
A . (
o1,
o2)
<> {}
by A15, A17;
hence
the
Arrows of
B . (f . i) <> {}
by A11, A18;
verum
end;
for
i being
set st
i in [: the carrier of A, the carrier of A:] & the
Arrows of
A . i <> {} holds
AA . i <> {}
then
(
m is
ManySortedFunction of the
Arrows of
A,
AA & ( for
i being
set st
i in [: the carrier of A, the carrier of A:] &
AA . i = {} holds
the
Arrows of
A . i = {} ) )
by FUNCTOR0:def 4;
then A21:
m in Funcs ( the
Arrows of
A,
AA)
by Def9;
A22:
f in Funcs (
[: the carrier of A, the carrier of A:],
[: the carrier of B, the carrier of B:])
by FUNCT_2:8;
then
the
Arrows of
B * f in sAA
;
then
Funcs ( the
Arrows of
A,
AA)
in XX
by A2;
then
m in union XX
by A21, TARSKI:def 4;
hence
y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):]
by A22, ZFMISC_1:def 2;
verum
end;
hence
x in X
by A8; verum