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(); :: 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 A11: <^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 ;
hence F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f by ; :: thesis: 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(); :: 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 A13: <^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 ;
hence F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) by ; :: thesis: 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(); :: thesis: ( 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)) ; :: thesis: ( 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; :: 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 ;
hence F8(a) " in <^b,a^> by A2, A15, A20, A16, A19; :: thesis: F8(a) is one-to-one
thus F8(a) is one-to-one by ; :: thesis: 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(); :: thesis: ( 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)) ; :: thesis: ( 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; :: 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 ;
hence F7(b) " in <^b,a^> by A1, A22, A27, A23, A26; :: thesis: F7(b) is one-to-one
thus F7(b) is one-to-one by ; :: thesis: 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); :: thesis: verum