A9:
ex G being covariant Functor of F2(),F1() st
( ( for a being Object of F2() holds G . a = F4(a) ) & ( for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) )
by A4;
A10:
for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
proof
let a,
b be
Object of
F2();
( <^a,b^> <> {} implies for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f )
assume A11:
<^a,b^> <> {}
;
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
let f be
Morphism of
a,
b;
F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
@ f = f
by A11, Def7;
hence
F5(
F4(
a),
F4(
b),
F6(
a,
b,
f))
* F8(
a)
= F8(
b)
* f
by A8, A11;
verum
end;
A12:
for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
proof
let a,
b be
Object of
F1();
( <^a,b^> <> {} implies for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) )
assume A13:
<^a,b^> <> {}
;
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
let f be
Morphism of
a,
b;
F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
@ f = f
by A13, Def7;
hence
F7(
b)
* F6(
F3(
a),
F3(
b),
F5(
a,
b,
f))
= f * F7(
a)
by A7, A13;
verum
end;
A14:
for a, b being Object of F2() st b = F3(F4(a)) holds
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one )
proof
let a,
b be
Object of
F2();
( b = F3(F4(a)) implies ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) )
assume A15:
b = F3(
F4(
a))
;
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one )
consider f being
monotone Function of
(latt a),
F3(
F4(
a))
such that A16:
f = F8(
a)
and A17:
f is
isomorphic
and A18:
P2[
latt a,
F3(
F4(
a)),
f]
and A19:
P2[
F3(
F4(
a)),
latt a,
f " ]
by A6;
A20:
latt b = b
;
hence
F8(
a)
in <^a,b^>
by A2, A15, A16, A18;
( F8(a) " in <^b,a^> & F8(a) is one-to-one )
ex
g being
Function of
F3(
F4(
a)),
(latt a) st
(
g = f " &
g is
monotone )
by A17, WAYBEL_0:def 38;
hence
F8(
a)
" in <^b,a^>
by A2, A15, A20, A16, A19;
F8(a) is one-to-one
thus
F8(
a) is
one-to-one
by A16, A17;
verum
end;
A21:
for a, b being Object of F1() st a = F4(F3(b)) holds
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one )
proof
let a,
b be
Object of
F1();
( a = F4(F3(b)) implies ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) )
assume A22:
a = F4(
F3(
b))
;
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one )
consider f being
monotone Function of
F4(
F3(
b)),
(latt b) such that A23:
f = F7(
b)
and A24:
f is
isomorphic
and A25:
P1[
F4(
F3(
b)),
latt b,
f]
and A26:
P1[
latt b,
F4(
F3(
b)),
f " ]
by A5;
A27:
latt a = a
;
hence
F7(
b)
in <^a,b^>
by A1, A22, A23, A25;
( F7(b) " in <^b,a^> & F7(b) is one-to-one )
ex
g being
Function of
(latt b),
F4(
F3(
b)) st
(
g = f " &
g is
monotone )
by A24, WAYBEL_0:def 38;
hence
F7(
b)
" in <^b,a^>
by A1, A22, A27, A23, A26;
F7(b) is one-to-one
thus
F7(
b) is
one-to-one
by A23, A24;
verum
end;
A28:
ex F being covariant Functor of F1(),F2() st
( ( 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 = F5(a,b,f) ) )
by A3;
thus
F1(),F2() are_equivalent
from YELLOW18:sch 22(A28, A9, A21, A14, A12, A10); verum