consider O being Function such that
A5:
dom O = the carrier of F1()
and
A6:
for x being object st x in the carrier of F1() holds
O . x = F3(x)
from FUNCT_1:sch 3();
rng O c= the carrier of F2()
then reconsider O = O as Function of the carrier of F1(), the carrier of F2() by A5, FUNCT_2:2;
reconsider OM = [:O,O:] as bifunction of the carrier of F1(), the carrier of F2() ;
defpred S1[ object , object , object ] means $1 = F4(($3 `1),($3 `2),$2);
A10:
for i being object st i in [: the carrier of F1(), the carrier of F1():] holds
for x being object st x in the Arrows of F1() . i holds
ex y being object st
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] )
proof
let i be
object ;
( i in [: the carrier of F1(), the carrier of F1():] implies for x being object st x in the Arrows of F1() . i holds
ex y being object st
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] ) )
assume A11:
i in [: the carrier of F1(), the carrier of F1():]
;
for x being object st x in the Arrows of F1() . i holds
ex y being object st
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] )
then consider a,
b being
object such that A12:
a in the
carrier of
F1()
and A13:
b in the
carrier of
F1()
and A14:
[a,b] = i
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Object of
F1()
by A12, A13;
let x be
object ;
( x in the Arrows of F1() . i implies ex y being object st
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] ) )
assume A15:
x in the
Arrows of
F1()
. i
;
ex y being object st
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] )
then reconsider f =
x as
Morphism of
a,
b by A14;
take y =
F4(
a,
b,
f);
( y in ( the Arrows of F2() * OM) . i & S1[y,x,i] )
A16:
y in the
Arrows of
F2()
. (
F3(
a),
F3(
b))
by A2, A14, A15;
A17:
F3(
a)
= O . a
by A6;
i in dom OM
by A5, A11, FUNCT_3:def 8;
then ( the Arrows of F2() * OM) . i =
the
Arrows of
F2()
. (OM . (a,b))
by A14, FUNCT_1:13
.=
the
Arrows of
F2()
. (
(O . a),
(O . b))
by A5, FUNCT_3:def 8
;
hence
y in ( the Arrows of F2() * OM) . i
by A6, A16, A17;
S1[y,x,i]
thus
S1[
y,
x,
i]
by A14;
verum
end;
consider M being ManySortedFunction of the Arrows of F1(), the Arrows of F2() * OM such that
A18:
for i being object st i in [: the carrier of F1(), the carrier of F1():] holds
ex f being Function of ( the Arrows of F1() . i),(( the Arrows of F2() * OM) . i) st
( f = M . i & ( for x being object st x in the Arrows of F1() . i holds
S1[f . x,x,i] ) )
from MSSUBFAM:sch 1(A10);
reconsider M = M as MSUnTrans of OM, the Arrows of F1(), the Arrows of F2() by FUNCTOR0:def 4;
FunctorStr(# OM,M #) is Covariant
then reconsider F = FunctorStr(# OM,M #) as Covariant FunctorStr over F1(),F2() ;
A19:
now for a being Object of F1() holds F . a = F3(a)end;
A20:
now for o1, o2 being Object of F1() st <^o1,o2^> <> {} holds
for g being Morphism of o1,o2 holds (Morph-Map (F,o1,o2)) . g = F4(o1,o2,g)let o1,
o2 be
Object of
F1();
( <^o1,o2^> <> {} implies for g being Morphism of o1,o2 holds (Morph-Map (F,o1,o2)) . g = F4(o1,o2,g) )assume A21:
<^o1,o2^> <> {}
;
for g being Morphism of o1,o2 holds (Morph-Map (F,o1,o2)) . g = F4(o1,o2,g)let g be
Morphism of
o1,
o2;
(Morph-Map (F,o1,o2)) . g = F4(o1,o2,g)
[o1,o2] in [: the carrier of F1(), the carrier of F1():]
by ZFMISC_1:def 2;
then consider f being
Function of
( the Arrows of F1() . [o1,o2]),
(( the Arrows of F2() * OM) . [o1,o2]) such that A22:
f = M . [o1,o2]
and A23:
for
x being
object st
x in the
Arrows of
F1()
. [o1,o2] holds
S1[
f . x,
x,
[o1,o2]]
by A18;
f . g =
F4(
([o1,o2] `1),
([o1,o2] `2),
g)
by A21, A23
.=
F4(
o1,
([o1,o2] `2),
g)
.=
F4(
o1,
o2,
g)
;
hence
(Morph-Map (F,o1,o2)) . g = F4(
o1,
o2,
g)
by A22;
verum end;
A24:
F is feasible
proof
let o1,
o2 be
Object of
F1();
FUNCTOR0:def 18 ( <^o1,o2^> = {} or not <^(F . o1),(F . o2)^> = {} )
set g = the
Morphism of
o1,
o2;
assume A25:
<^o1,o2^> <> {}
;
not <^(F . o1),(F . o2)^> = {}
then
(Morph-Map (F,o1,o2)) . the
Morphism of
o1,
o2 = F4(
o1,
o2, the
Morphism of
o1,
o2)
by A20;
then
(Morph-Map (F,o1,o2)) . the
Morphism of
o1,
o2 in the
Arrows of
F2()
. (
F3(
o1),
F3(
o2))
by A2, A25;
then
(Morph-Map (F,o1,o2)) . the
Morphism of
o1,
o2 in the
Arrows of
F2()
. (
(F . o1),
F3(
o2))
by A19;
hence
not
<^(F . o1),(F . o2)^> = {}
by A19;
verum
end;
A26:
now for o1, o2 being Object of F1() st <^o1,o2^> <> {} holds
for g being Morphism of o1,o2 holds F . g = F4(o1,o2,g)let o1,
o2 be
Object of
F1();
( <^o1,o2^> <> {} implies for g being Morphism of o1,o2 holds F . g = F4(o1,o2,g) )assume A27:
<^o1,o2^> <> {}
;
for g being Morphism of o1,o2 holds F . g = F4(o1,o2,g)let g be
Morphism of
o1,
o2;
F . g = F4(o1,o2,g)A28:
(Morph-Map (F,o1,o2)) . g = F4(
o1,
o2,
g)
by A20, A27;
<^(F . o1),(F . o2)^> <> {}
by A24, A27;
hence
F . g = F4(
o1,
o2,
g)
by A27, A28, FUNCTOR0:def 15;
verum end;
A29:
F is comp-preserving
proof
let o1,
o2,
o3 be
Object of
F1();
FUNCTOR0:def 21 ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being Element of <^o1,o2^>
for b2 being Element of <^o2,o3^> ex b3 being Element of <^(F . o1),(F . o2)^> ex b4 being Element of <^(F . o2),(F . o3)^> st
( b3 = (Morph-Map (F,o1,o2)) . b1 & b4 = (Morph-Map (F,o2,o3)) . b2 & (Morph-Map (F,o1,o3)) . (b2 * b1) = b4 * b3 ) )
assume that A30:
<^o1,o2^> <> {}
and A31:
<^o2,o3^> <> {}
;
for b1 being Element of <^o1,o2^>
for b2 being Element of <^o2,o3^> ex b3 being Element of <^(F . o1),(F . o2)^> ex b4 being Element of <^(F . o2),(F . o3)^> st
( b3 = (Morph-Map (F,o1,o2)) . b1 & b4 = (Morph-Map (F,o2,o3)) . b2 & (Morph-Map (F,o1,o3)) . (b2 * b1) = b4 * b3 )
let f be
Morphism of
o1,
o2;
for b1 being Element of <^o2,o3^> ex b2 being Element of <^(F . o1),(F . o2)^> ex b3 being Element of <^(F . o2),(F . o3)^> st
( b2 = (Morph-Map (F,o1,o2)) . f & b3 = (Morph-Map (F,o2,o3)) . b1 & (Morph-Map (F,o1,o3)) . (b1 * f) = b3 * b2 )let g be
Morphism of
o2,
o3;
ex b1 being Element of <^(F . o1),(F . o2)^> ex b2 being Element of <^(F . o2),(F . o3)^> st
( b1 = (Morph-Map (F,o1,o2)) . f & b2 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = b2 * b1 )
set a =
O . o1;
set b =
O . o2;
set c =
O . o3;
A32:
O . o1 = F3(
o1)
by A6;
A33:
O . o2 = F3(
o2)
by A6;
A34:
O . o3 = F3(
o3)
by A6;
reconsider f9 =
F4(
o1,
o2,
f) as
Morphism of
(O . o1),
(O . o2) by A2, A30, A32, A33;
reconsider g9 =
F4(
o2,
o3,
g) as
Morphism of
(O . o2),
(O . o3) by A2, A31, A33, A34;
A35:
O . o1 = F . o1
by A19, A32;
A36:
O . o2 = F . o2
by A19, A33;
A37:
O . o3 = F . o3
by A19, A34;
reconsider ff =
f9 as
Morphism of
(F . o1),
(F . o2) by A19, A32, A36;
reconsider gg =
g9 as
Morphism of
(F . o2),
(F . o3) by A19, A34, A36;
take
ff
;
ex b1 being Element of <^(F . o2),(F . o3)^> st
( ff = (Morph-Map (F,o1,o2)) . f & b1 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = b1 * ff )
take
gg
;
( ff = (Morph-Map (F,o1,o2)) . f & gg = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = gg * ff )
A38:
<^o1,o3^> <> {}
by A30, A31, ALTCAT_1:def 2;
F4(
o1,
o3,
(g * f))
= gg * ff
by A3, A30, A31, A32, A33, A34, A35, A36, A37;
hence
(
ff = (Morph-Map (F,o1,o2)) . f &
gg = (Morph-Map (F,o2,o3)) . g &
(Morph-Map (F,o1,o3)) . (g * f) = gg * ff )
by A20, A30, A31, A38;
verum
end;
F is Functor of F1(),F2()
then reconsider F = F as strict covariant Functor of F1(),F2() by A29;
take
F
; ( ( for a being Object of F1() holds F . a = F3(a) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
thus
( ( for a being Object of F1() holds F . a = F3(a) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
by A19, A26; verum