A9:
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;
A10:
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;
A11:
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();
:: thesis: ( a = F4(F3(b)) implies ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) )
assume A12:
a = F4(
F3(
b))
;
:: thesis: ( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one )
A13:
(
latt a = a &
latt b = b )
;
consider f being
monotone Function of
F4(
F3(
b)),
(latt b) such that A14:
(
f = F7(
b) &
f is
isomorphic &
P1[
F4(
F3(
b)),
latt b,
f] &
P1[
latt b,
F4(
F3(
b)),
f " ] )
by A5;
thus
F7(
b)
in <^a,b^>
by A1, A12, A13, A14;
:: thesis: ( 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 A14, WAYBEL_0:def 38;
hence
F7(
b)
" in <^b,a^>
by A1, A12, A13, A14;
:: thesis: F7(b) is one-to-one
thus
F7(
b) is
one-to-one
by A14;
:: thesis: verum
end;
A15:
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();
:: thesis: ( b = F3(F4(a)) implies ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) )
assume A16:
b = F3(
F4(
a))
;
:: thesis: ( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one )
A17:
(
latt a = a &
latt b = b )
;
consider f being
monotone Function of
(latt a),
F3(
F4(
a))
such that A18:
(
f = F8(
a) &
f is
isomorphic &
P2[
latt a,
F3(
F4(
a)),
f] &
P2[
F3(
F4(
a)),
latt a,
f " ] )
by A6;
thus
F8(
a)
in <^a,b^>
by A2, A16, A17, A18;
:: thesis: ( 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 A18, WAYBEL_0:def 38;
hence
F8(
a)
" in <^b,a^>
by A2, A16, A17, A18;
:: thesis: F8(a) is one-to-one
thus
F8(
a) is
one-to-one
by A18;
:: thesis: verum
end;
A19:
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();
:: thesis: ( <^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 A20:
<^a,b^> <> {}
;
:: thesis: 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;
:: thesis: F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a)
@ f = f
by A20, Def7;
hence
F7(
b)
* F6(
F3(
a),
F3(
b),
F5(
a,
b,
f))
= f * F7(
a)
by A7, A20;
:: thesis: verum
end;
A21:
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();
:: thesis: ( <^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 A22:
<^a,b^> <> {}
;
:: thesis: 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;
:: thesis: F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f
@ f = f
by A22, Def7;
hence
F5(
F4(
a),
F4(
b),
F6(
a,
b,
f))
* F8(
a)
= F8(
b)
* f
by A8, A22;
:: thesis: verum
end;
thus
F1(),F2() are_equivalent
from YELLOW18:sch 22(A9, A10, A11, A15, A19, A21); :: thesis: verum