defpred S₁[ object , object ] means ex a, b being LATTICE ex c being set st
( c = $2 & $1 = [a,b] & ( for f being object holds
( f in c iff ( f in MonFuncs (a,b) & P₁[a,b,f] ) ) ) );
set A = F₁();

let x be object ; :: thesis:
assume x in [:F₁(),F₁():] ; :: thesis:
then consider a, b being object such that
A5: ( a in F₁() & b in F₁() ) and
A6: x = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as LATTICE by A1, A5;
defpred S₂[ object ] means P₁[a,b,$1];
consider y being set such that
A7: for f being object holds
( f in y iff ( f in MonFuncs (a,b) & S₂[f] ) ) from XBOOLE_0:sch 1();
reconsider y = y as object ;
take y = y; :: thesis:
thus S₁[x,y] by A6, A7; :: thesis:

end;

consider F being Function such that
dom F = [:F₁(),F₁():] and
A8: for x being object st x in [:F₁(),F₁():] holds
S₁[x,F . x] from CLASSES1:sch 1(A4);
defpred S₂[ object , object ] means for a being LATTICE st a = $1 holds
$2 = the carrier of a;

A9: now :: thesis:

let x be object ; :: thesis:
assume x in F₁() ; :: thesis:
then reconsider a = x as LATTICE by A1;
reconsider b = the carrier of a as object ;
take b = b; :: thesis:
thus S₂[x,b] ; :: thesis:

end;

consider D being Function such that
dom D = F₁() and
A10: for x being object st x in F₁() holds
S₂[x,D . x] from CLASSES1:sch 1(A9);
deffunc H₁( set , set ) -> set = F . [$1,$2];

A11: now :: thesis:

let a, b be LATTICE; :: thesis:
assume ( a in F₁() & b in F₁() ) ; :: thesis:
then [a,b] in [:F₁(),F₁():] by ZFMISC_1:87;
then S₁[[a,b],F . [a,b]] by A8;
then consider a9, b9 being LATTICE, c being set such that
A12: c = F . [a,b] and
A13: [a,b] = [a9,b9] and
A14: for f being object holds
( f in c iff ( f in MonFuncs (a9,b9) & P₁[a9,b9,f] ) ) ;
let f be set ; :: thesis:
A15: ( a = a9 & b = b9 ) by A13, XTUPLE_0:1;

hereby :: thesis:

assume A16: f in F . [a,b] ; :: thesis:
hence P₁[a,b,f] by A14, A15, A12; :: thesis:
thus f in MonFuncs (a,b) by A14, A15, A16, A12; :: thesis:
then ex g being Function of a,b st
( f = g & g in Funcs ( the carrier of a, the carrier of b) & g is monotone ) by ORDERS_3:def 6;
hence ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ; :: thesis:

end;

assume f is monotone Function of a,b ; :: thesis:
then reconsider g = f as monotone Function of a,b ;
( the carrier of b <> {} implies ( dom g = the carrier of a & rng g c= the carrier of b ) ) by FUNCT_2:def 1;
then g in Funcs ( the carrier of a, the carrier of b) by FUNCT_2:def 2;
then A17: f in MonFuncs (a,b) by ORDERS_3:def 6;
assume P₁[a,b,f] ; :: thesis:
then f in c by A14, A15, A17;
hence f in F . [a,b] by A12; :: thesis:

end;

A18: for a, b, c being Element of F₁()
for f, g being Function st f in H₁(a,b) & g in H₁(b,c) holds
g * f in H₁(a,c)

proof

let a, b, c be Element of F₁(); :: thesis:
let f, g be Function; :: thesis:
assume that
A19: f in F . [a,b] and
A20: g in F . [b,c] ; :: thesis:
reconsider x = a, y = b, z = c as LATTICE by A1;
reconsider g9 = g as monotone Function of y,z by A11, A20;
reconsider f9 = f as monotone Function of x,y by A11, A19;
( P₁[x,y,f9] & P₁[y,z,g9] ) by A11, A19, A20;
then P₁[a,c,g9 * f9] by A2;
then ( g9 * f9 is monotone Function of x,z implies g9 * f9 in F . [x,z] ) by A11;
hence g * f in H₁(a,c) by YELLOW_2:12; :: thesis:

end;

deffunc H₂( set ) -> set = D . $1;
A21: for a, b being Element of F₁() holds H₁(a,b) c= Funcs (H₂(a),H₂(b))

proof

let a, b be Element of F₁(); :: thesis:
let f be object ; :: according to TARSKI:def 3 :: thesis:
reconsider x = a, y = b as LATTICE by A1;
assume f in F . [a,b] ; :: thesis:
then f in Funcs ( the carrier of x, the carrier of y) by A11;
then f in Funcs ((D . a), the carrier of y) by A10;
hence f in Funcs (H₂(a),H₂(b)) by A10; :: thesis:

end;

A22: now :: thesis:

let a be Element of F₁(); :: thesis:
reconsider x = a as LATTICE by A1;
( id (D . a) = id x & P₁[x,x, id x] ) by A3, A10;
hence id H₂(a) in H₁(a,a) by A11; :: thesis:

end;

consider C being strict concrete category such that
A23: the carrier of C = F₁() and
for a being Object of C holds the_carrier_of a = H₂(a) and
A24: for a, b being Object of C holds <^a,b^> = H₁(a,b) from YELLOW18:sch 16(A18, A21, A22);
take C ; :: thesis:
thus ( C is semi-functional & C is set-id-inheriting ) ; :: according to YELLOW21:def 4 :: thesis:
thus for a being Object of C holds a is LATTICE by A1, A23; :: thesis:
thus for a, b being Object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) :: thesis:

proof

let a, b be Object of C; :: thesis:
let A, B be LATTICE; :: thesis:
assume A25: ( A = a & B = b ) ; :: thesis:
let f be object ; :: according to TARSKI:def 3 :: thesis:
<^a,b^> = F . [A,B] by A24, A25;
hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by A11, A23, A25; :: thesis:

end;

thus the carrier of C = F₁() by A23; :: thesis:
let a, b be LATTICE; :: thesis:
let f be monotone Function of a,b; :: thesis:

hereby :: thesis:

assume A26: f in the Arrows of C . (a,b) ; :: thesis:
then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
then A27: [a,b] in [:F₁(),F₁():] by A23;
hence ( a in F₁() & b in F₁() ) by ZFMISC_1:87; :: thesis:
reconsider x = a, y = b as Object of C by A23, A27, ZFMISC_1:87;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A24 ;
hence P₁[a,b,f] by A11, A23, A26; :: thesis:

end;

assume A28: ( a in F₁() & b in F₁() ) ; :: thesis:
then reconsider x = a, y = b as Object of C by A23;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A24 ;
hence ( not P₁[a,b,f] or f in the Arrows of C . (a,b) ) by A11, A28; :: thesis: