A7: for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a)

proof

let a, b be object of ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a) )
assume A8: <^a,b^> <> {} ; :: thesis: for f being Morphism of , holds F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a)
let f be Morphism of ,; :: thesis: F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a)
A9: f = @ f by A8, Def7;
then P₁[a,b,f] by A1, A8;
then A10: ( F₄(a,b,f) is Function of F₃(b),F₃(a) & P₂[F₃(b),F₃(a),F₄(a,b,f)] ) by A4, A9;
( F₃(a) in the carrier of F₂() & F₃(b) in the carrier of F₂() ) by A3, A9;
hence F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a) by A2, A10; :: thesis: verum

end;

A11: now

let a, b, c be object of ; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of ,
for a', b', c' being object of st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g' )
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; :: thesis: for f being Morphism of ,
for g being Morphism of ,
for a', b', c' being object of st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let f be Morphism of ,; :: thesis: for g being Morphism of ,
for a', b', c' being object of st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let g be Morphism of ,; :: thesis: for a', b', c' being object of st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let a', b', c' be object of ; :: thesis: ( a' = F₃(a) & b' = F₃(b) & c' = F₃(c) implies for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g' )
assume that
A14: a' = F₃(a) and
A15: b' = F₃(b) and
A16: c' = F₃(c) ; :: thesis: for f' being Morphism of ,
for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let f' be Morphism of ,; :: thesis: for g' being Morphism of , st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let g' be Morphism of ,; :: thesis: ( f' = F₄(a,b,f) & g' = F₄(b,c,g) implies F₄(a,c,(g * f)) = f' * g' )
assume A17: ( f' = F₄(a,b,f) & g' = F₄(b,c,g) ) ; :: thesis: F₄(a,c,(g * f)) = f' * g'
A18: F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a) by A7, A12;
then A19: @ f' = f' by A14, A15, Def7;
A20: @ g = g by A13, Def7;
then A21: P₁[b,c,g] by A1, A13;
A22: F₄(b,c,g) in the Arrows of F₂() . F₃(c),F₃(b) by A7, A13;
then A23: @ g' = g' by A15, A16, Def7;
A24: @ f = f by A12, Def7;
then P₁[a,b,f] by A1, A12;
then F₄(a,c,((@ g) * (@ f))) = F₄(a,b,f) * F₄(b,c,g) by A6, A24, A20, A21
.= f' * g' by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;
hence F₄(a,c,(g * f)) = f' * g' by A12, A13, Th3; :: thesis: verum

end;

A25: now

let a be object of ; :: thesis: for a' being object of st a' = F₃(a) holds
F₄(a,a,(idm a)) = idm a'
let a' be object of ; :: thesis: ( a' = F₃(a) implies F₄(a,a,(idm a)) = idm a' )
assume A26: a' = F₃(a) ; :: thesis: F₄(a,a,(idm a)) = idm a'
idm a = id (latt a) by Th2;
hence F₄(a,a,(idm a)) = id (latt a') by A5, A26
.= idm a' by Th2 ;
:: thesis: verum

end;

A27: for a being object of holds F₃(a) is object of

proof

let a be object of ; :: thesis: F₃(a) is object of
a is LATTICE by Def4;
hence F₃(a) is object of by A3; :: thesis: verum

end;

consider F being strict contravariant Functor of F₁(),F₂() such that
A28: for a being object of holds F . a = F₃(a) and
A29: for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds F . f = F₄(a,b,f) from YELLOW18:sch 9(A27, A7, A11, A25);
take F ; :: thesis: ( ( for a being object of holds F . a = F₃((latt a)) ) & ( for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds F . f = F₄((latt a),(latt b),(@ f)) ) )
thus for a being object of holds F . a = F₃((latt a)) by A28; :: thesis: for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds F . f = F₄((latt a),(latt b),(@ f))
let a, b be object of ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds F . f = F₄((latt a),(latt b),(@ f)) )
assume A30: <^a,b^> <> {} ; :: thesis: for f being Morphism of , holds F . f = F₄((latt a),(latt b),(@ f))
let f be Morphism of ,; :: thesis: F . f = F₄((latt a),(latt b),(@ f))
f = @ f by A30, Def7;
hence F . f = F₄((latt a),(latt b),(@ f)) by A29, A30; :: thesis: verum