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

A4: now

let x be set ; :: thesis:
assume x in [:F₁(),F₁():] ; :: thesis:
then consider a, b being set 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₂[ set ] means P₁[a,b,$1];
consider y being set such that
A7: for f being set holds
( f in y iff ( f in MonFuncs a,b & S₂[f] ) ) from XBOOLE_0:sch 1();
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 set st x in [:F₁(),F₁():] holds
S₁[x,F . x] from CLASSES1:sch 1(A4);
defpred S₂[ set , set ] means for a being LATTICE st a = $1 holds
$2 = the carrier of a;

A9: now

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

end;

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

A11: now

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

hereby :: thesis:

assume A15: f in F . [a,b] ; :: thesis:
hence P₁[a,b,f] by A13, A14; :: thesis:
thus f in MonFuncs a,b by A13, A14, A15; :: 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 f in MonFuncs a,b by ORDERS_3:def 6;
hence ( P₁[a,b,f] implies f in F . [a,b] ) by A13, A14; :: thesis:

end;

A16: 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
A17: f in F . [a,b] and
A18: 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, A18;
reconsider f9 = f as monotone Function of x,y by A11, A17;
( P₁[x,y,f9] & P₁[y,z,g9] ) by A11, A17, A18;
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:14; :: thesis:

end;

deffunc H₂( set ) -> set = D . $1;
A19: 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 set ; :: 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;

A20: now

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
A21: the carrier of C = F₁() and
for a being object of C holds the_carrier_of a = H₂(a) and
A22: for a, b being object of C holds <^a,b^> = H₁(a,b) from YELLOW18:sch 16(A16, A19, A20);
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, A21; :: 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 A23: ( A = a & B = b ) ; :: thesis:
let f be set ; :: according to TARSKI:def 3 :: thesis:
<^a,b^> = F . [A,B] by A22, A23;
hence ( not f in <^a,b^> or f in MonFuncs A,B ) by A11, A21, A23; :: thesis:

end;

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

hereby :: thesis:

assume A24: f in the Arrows of C . a,b ; :: thesis:
then [a,b] in dom the Arrows of C by FUNCT_1:def 4;
then A25: [a,b] in [:F₁(),F₁():] by A21, PARTFUN1:def 4;
hence ( a in F₁() & b in F₁() ) by ZFMISC_1:106; :: thesis:
reconsider x = a, y = b as object of C by A21, A25, ZFMISC_1:106;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A22 ;
hence P₁[a,b,f] by A11, A21, A24; :: thesis:

end;

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