A7:
for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
proof
let a,
b be
Object of
F1();
( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a)) )
assume A8:
<^a,b^> <> {}
;
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
let f be
Morphism of
a,
b;
F4(a,b,f) in the Arrows of F2() . (F3(b),F3(a))
A9:
f = @ f
by A8, Def7;
then
P1[
a,
b,
f]
by A1, A8;
then A10:
(
F4(
a,
b,
f) is
Function of
F3(
b),
F3(
a) &
P2[
F3(
b),
F3(
a),
F4(
a,
b,
f)] )
by A4, A9;
(
F3(
a)
in the
carrier of
F2() &
F3(
b)
in the
carrier of
F2() )
by A3, A9;
hence
F4(
a,
b,
f)
in the
Arrows of
F2()
. (
F3(
b),
F3(
a))
by A2, A10;
verum
end;
A11:
now for a, b, c being Object of F1() 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 F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let a,
b,
c be
Object of
F1();
( <^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 F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 )assume that A12:
<^a,b^> <> {}
and A13:
<^b,c^> <> {}
;
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let f be
Morphism of
a,
b;
for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let g be
Morphism of
b,
c;
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let a9,
b9,
c9 be
Object of
F2();
( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9 )assume that A14:
a9 = F3(
a)
and A15:
b9 = F3(
b)
and A16:
c9 = F3(
c)
;
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let f9 be
Morphism of
b9,
a9;
for g9 being Morphism of c9,b9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = f9 * g9let g9 be
Morphism of
c9,
b9;
( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = f9 * g9 )assume A17:
(
f9 = F4(
a,
b,
f) &
g9 = F4(
b,
c,
g) )
;
F4(a,c,(g * f)) = f9 * g9A18:
F4(
a,
b,
f)
in the
Arrows of
F2()
. (
F3(
b),
F3(
a))
by A7, A12;
then A19:
@ f9 = f9
by A14, A15, Def7;
A20:
@ g = g
by A13, Def7;
then A21:
P1[
b,
c,
g]
by A1, A13;
A22:
F4(
b,
c,
g)
in the
Arrows of
F2()
. (
F3(
c),
F3(
b))
by A7, A13;
then A23:
@ g9 = g9
by A15, A16, Def7;
A24:
@ f = f
by A12, Def7;
then
P1[
a,
b,
f]
by A1, A12;
then F4(
a,
c,
((@ g) * (@ f))) =
F4(
a,
b,
f)
* F4(
b,
c,
g)
by A6, A24, A20, A21
.=
f9 * g9
by A14, A15, A16, A17, A18, A22, A19, A23, Th3
;
hence
F4(
a,
c,
(g * f))
= f9 * g9
by A12, A13, Th3;
verum end;
A27:
for a being Object of F1() holds F3(a) is Object of F2()
consider F being strict contravariant Functor of F1(),F2() such that
A28:
for a being Object of F1() holds F . a = F3(a)
and
A29:
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)
from YELLOW18:sch 9(A27, A7, A11, A25);
take
F
; ( ( for a being Object of F1() holds F . a = F3((latt a)) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
thus
for a being Object of F1() holds F . a = F3((latt a))
by A28; for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let a, b be Object of F1(); ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) )
assume A30:
<^a,b^> <> {}
; for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let f be Morphism of a,b; F . f = F4((latt a),(latt b),(@ f))
f = @ f
by A30, Def7;
hence
F . f = F4((latt a),(latt b),(@ f))
by A29, A30; verum