A7: for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
proof
let a, b be Object of F1(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) )
assume A8: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
let f be Morphism of a,b; :: thesis: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b))
A9: f = @ f by A8, Def7;
then P1[a,b,f] by A1, A8;
then A10: ( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) by A4, A9;
( F3(a) in the carrier of F2() & F3(b) in the carrier of F2() ) by A3, A9;
hence F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A2, A10; :: thesis: verum
end;
A11: now :: thesis: for a, b, c being Object of F1() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let a, b, c be Object of F1(); :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 )
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c
for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of F2() st a9 = F3(a) & b9 = F3(b) & c9 = F3(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let a9, b9, c9 be Object of F2(); :: thesis: ( a9 = F3(a) & b9 = F3(b) & c9 = F3(c) implies for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9 )
assume that
A14: a9 = F3(a) and
A15: b9 = F3(b) and
A16: c9 = F3(c) ; :: thesis: for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let f9 be Morphism of a9,b9; :: thesis: for g9 being Morphism of b9,c9 st f9 = F4(a,b,f) & g9 = F4(b,c,g) holds
F4(a,c,(g * f)) = g9 * f9
let g9 be Morphism of b9,c9; :: thesis: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) implies F4(a,c,(g * f)) = g9 * f9 )
assume A17: ( f9 = F4(a,b,f) & g9 = F4(b,c,g) ) ; :: thesis: F4(a,c,(g * f)) = g9 * f9
A18: F4(a,b,f) in the Arrows of F2() . (F3(a),F3(b)) by A7, A12;
then A19: @ f9 = f9 by A14, A15, Def7;
A20: @ g = g by A13, Def7;
then A21: P1[b,c,g] by A1, A13;
A22: F4(b,c,g) in the Arrows of F2() . (F3(b),F3(c)) by A7, A13;
then A23: @ g9 = g9 by A15, A16, Def7;
A24: @ f = f by A12, Def7;
then P1[a,b,f] by A1, A12;
then F4(a,c,((@ g) * (@ f))) = F4(b,c,g) * F4(a,b,f) by A6, A24, A20, A21
.= g9 * f9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;
hence F4(a,c,(g * f)) = g9 * f9 by A12, A13, Th3; :: thesis: verum
end;
A25: now :: thesis: for a being Object of F1()
for a9 being Object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
let a be Object of F1(); :: thesis: for a9 being Object of F2() st a9 = F3(a) holds
F4(a,a,(idm a)) = idm a9
let a9 be Object of F2(); :: thesis: ( a9 = F3(a) implies F4(a,a,(idm a)) = idm a9 )
assume A26: a9 = F3(a) ; :: thesis: F4(a,a,(idm a)) = idm a9
idm a = id (latt a) by Th2;
hence F4(a,a,(idm a)) = id (latt a9) by A5, A26
.= idm a9 by Th2 ;
:: thesis: verum
end;
A27: for a being Object of F1() holds F3(a) is Object of F2()
proof
let a be Object of F1(); :: thesis: F3(a) is Object of F2()
a is LATTICE by Def4;
hence F3(a) is Object of F2() by A3; :: thesis: verum
end;
consider F being strict covariant Functor of F1(),F2() such that
A28: for a being Object of F1() holds F . a = F3(a) and
A29: for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) from YELLOW18:sch 8(A27, A7, A11, A25);
 take F ; :: thesis: ( ( for a being Object of F1() holds F . a = F3((latt a)) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
thus for a being Object of F1() holds F . a = F3((latt a)) by A28; :: thesis: for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let a, b be Object of F1(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) )
assume A30: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f))
let f be Morphism of a,b; :: thesis: F . f = F4((latt a),(latt b),(@ f))
f = @ f by A30, Def7;
hence F . f = F4((latt a),(latt b),(@ f)) by A29, A30; :: thesis: verum