A7: for a being object of F₁() holds F₃(a) is object of F₂()

proof

let a be object of F₁(); :: thesis: F₃(a) is object of F₂()
( a is LATTICE & a in the carrier of F₁() ) by Def4;
hence F₃(a) is object of F₂() by A3; :: thesis: verum

end;

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

proof

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

end;

A11: now

let a, b, c be object of F₁(); :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a', b', c' being object of F₂() st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g' )
assume A12: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c
for a', b', c' being object of F₂() st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c
for a', b', c' being object of F₂() st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let g be Morphism of b,c; :: thesis: for a', b', c' being object of F₂() st a' = F₃(a) & b' = F₃(b) & c' = F₃(c) holds
for f' being Morphism of b',a'
for g' being Morphism of c',b' 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 F₂(); :: thesis: ( a' = F₃(a) & b' = F₃(b) & c' = F₃(c) implies for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g' )
assume A13: ( a' = F₃(a) & b' = F₃(b) & c' = F₃(c) ) ; :: thesis: for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let f' be Morphism of b',a'; :: thesis: for g' being Morphism of c',b' st f' = F₄(a,b,f) & g' = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f' * g'
let g' be Morphism of c',b'; :: thesis: ( f' = F₄(a,b,f) & g' = F₄(b,c,g) implies F₄(a,c,(g * f)) = f' * g' )
assume A14: ( f' = F₄(a,b,f) & g' = F₄(b,c,g) ) ; :: thesis: F₄(a,c,(g * f)) = f' * g'
A15: ( @ f = f & @ g = g ) by A12, Def7;
A16: ( latt a' = a' & latt b' = b' & latt c' = c' & F₄(a,b,f) in the Arrows of F₂() . F₃(b),F₃(a) & F₄(b,c,g) in the Arrows of F₂() . F₃(c),F₃(b) ) by A8, A12;
then A17: ( @ f' = f' & @ g' = g' ) by A13, Def7;
( P₁[a,b,f] & P₁[b,c,g] ) by A1, A12, A15;
then F₄(a,c,((@ g) * (@ f))) = F₄(a,b,f) * F₄(b,c,g) by A6, A15
.= f' * g' by A13, A14, A16, A17, Th3 ;
hence F₄(a,c,(g * f)) = f' * g' by A12, Th3; :: thesis: verum

end;

A18: now

let a be object of F₁(); :: thesis: for a' being object of F₂() st a' = F₃(a) holds
F₄(a,a,(idm a)) = idm a'
let a' be object of F₂(); :: thesis: ( a' = F₃(a) implies F₄(a,a,(idm a)) = idm a' )
assume a' = F₃(a) ; :: thesis: F₄(a,a,(idm a)) = idm a'
then ( a in the carrier of F₁() & latt a' = F₃(a) & latt a = a & idm a = id (latt a) ) by Th2;
hence F₄(a,a,(idm a)) = id (latt a') by A5
.= idm a' by Th2 ;
:: thesis: verum

end;

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