A9:
ex G being covariant Functor of F_{2}(),F_{1}() st

( ( for a being Object of F_{2}() holds G . a = F_{4}(a) ) & ( for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds G . f = F_{6}(a,b,f) ) )
by A4;

A10: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f
_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a)
_{2}() st b = F_{3}(F_{4}(a)) holds

( F_{8}(a) in <^a,b^> & F_{8}(a) " in <^b,a^> & F_{8}(a) is one-to-one )
_{1}() st a = F_{4}(F_{3}(b)) holds

( F_{7}(b) in <^a,b^> & F_{7}(b) " in <^b,a^> & F_{7}(b) is one-to-one )
_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{5}(a,b,f) ) )
by A3;

thus F_{1}(),F_{2}() are_equivalent
from YELLOW18:sch 22(A28, A9, A21, A14, A12, A10); :: thesis: verum

( ( for a being Object of F

for f being Morphism of a,b holds G . f = F

A10: for a, b being Object of F

for f being Morphism of a,b holds F

proof

A12:
for a, b being Object of F
let a, b be Object of F_{2}(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f )

assume A11: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f

let f be Morphism of a,b; :: thesis: F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f

@ f = f by A11, Def7;

hence F_{5}(F_{4}(a),F_{4}(b),F_{6}(a,b,f)) * F_{8}(a) = F_{8}(b) * f
by A8, A11; :: thesis: verum

end;assume A11: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F

let f be Morphism of a,b; :: thesis: F

@ f = f by A11, Def7;

hence F

for f being Morphism of a,b holds F

proof

A14:
for a, b being Object of F
let a, b be Object of F_{1}(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a) )

assume A13: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a)

let f be Morphism of a,b; :: thesis: F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a)

@ f = f by A13, Def7;

hence F_{7}(b) * F_{6}(F_{3}(a),F_{3}(b),F_{5}(a,b,f)) = f * F_{7}(a)
by A7, A13; :: thesis: verum

end;assume A13: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F

let f be Morphism of a,b; :: thesis: F

@ f = f by A13, Def7;

hence F

( F

proof

A21:
for a, b being Object of F
let a, b be Object of F_{2}(); :: thesis: ( b = F_{3}(F_{4}(a)) implies ( F_{8}(a) in <^a,b^> & F_{8}(a) " in <^b,a^> & F_{8}(a) is one-to-one ) )

assume A15: b = F_{3}(F_{4}(a))
; :: thesis: ( F_{8}(a) in <^a,b^> & F_{8}(a) " in <^b,a^> & F_{8}(a) is one-to-one )

consider f being monotone Function of (latt a),F_{3}(F_{4}(a)) such that

A16: f = F_{8}(a)
and

A17: f is isomorphic and

A18: P_{2}[ latt a,F_{3}(F_{4}(a)),f]
and

A19: P_{2}[F_{3}(F_{4}(a)), latt a,f " ]
by A6;

A20: latt b = b ;

hence F_{8}(a) in <^a,b^>
by A2, A15, A16, A18; :: thesis: ( F_{8}(a) " in <^b,a^> & F_{8}(a) is one-to-one )

ex g being Function of F_{3}(F_{4}(a)),(latt a) st

( g = f " & g is monotone ) by A17, WAYBEL_0:def 38;

hence F_{8}(a) " in <^b,a^>
by A2, A15, A20, A16, A19; :: thesis: F_{8}(a) is one-to-one

thus F_{8}(a) is one-to-one
by A16, A17; :: thesis: verum

end;assume A15: b = F

consider f being monotone Function of (latt a),F

A16: f = F

A17: f is isomorphic and

A18: P

A19: P

A20: latt b = b ;

hence F

ex g being Function of F

( g = f " & g is monotone ) by A17, WAYBEL_0:def 38;

hence F

thus F

( F

proof

A28:
ex F being covariant Functor of F
let a, b be Object of F_{1}(); :: thesis: ( a = F_{4}(F_{3}(b)) implies ( F_{7}(b) in <^a,b^> & F_{7}(b) " in <^b,a^> & F_{7}(b) is one-to-one ) )

assume A22: a = F_{4}(F_{3}(b))
; :: thesis: ( F_{7}(b) in <^a,b^> & F_{7}(b) " in <^b,a^> & F_{7}(b) is one-to-one )

consider f being monotone Function of F_{4}(F_{3}(b)),(latt b) such that

A23: f = F_{7}(b)
and

A24: f is isomorphic and

A25: P_{1}[F_{4}(F_{3}(b)), latt b,f]
and

A26: P_{1}[ latt b,F_{4}(F_{3}(b)),f " ]
by A5;

A27: latt a = a ;

hence F_{7}(b) in <^a,b^>
by A1, A22, A23, A25; :: thesis: ( F_{7}(b) " in <^b,a^> & F_{7}(b) is one-to-one )

ex g being Function of (latt b),F_{4}(F_{3}(b)) st

( g = f " & g is monotone ) by A24, WAYBEL_0:def 38;

hence F_{7}(b) " in <^b,a^>
by A1, A22, A27, A23, A26; :: thesis: F_{7}(b) is one-to-one

thus F_{7}(b) is one-to-one
by A23, A24; :: thesis: verum

end;assume A22: a = F

consider f being monotone Function of F

A23: f = F

A24: f is isomorphic and

A25: P

A26: P

A27: latt a = a ;

hence F

ex g being Function of (latt b),F

( g = f " & g is monotone ) by A24, WAYBEL_0:def 38;

hence F

thus F

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

thus F