defpred S1[ 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) & P1[a,b,f] ) ) ) );
set A = F1();
A4: now :: thesis: for x being object st x in [:F1(),F1():] holds
ex y being object st S1[x,y]
let x be object ; :: thesis: ( x in [:F1(),F1():] implies ex y being object st S1[x,y] )
assume x in [:F1(),F1():] ; :: thesis: ex y being object st S1[x,y]
then consider a, b being object such that
A5: ( a in F1() & b in F1() ) and
A6: x = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as LATTICE by A1, A5;
defpred S2[ object ] means P1[a,b,\$1];
consider y being set such that
A7: for f being object holds
( f in y iff ( f in MonFuncs (a,b) & S2[f] ) ) from reconsider y = y as object ;
take y = y; :: thesis: S1[x,y]
thus S1[x,y] by A6, A7; :: thesis: verum
end;
consider F being Function such that
dom F = [:F1(),F1():] and
A8: for x being object st x in [:F1(),F1():] holds
S1[x,F . x] from defpred S2[ object , object ] means for a being LATTICE st a = \$1 holds
\$2 = the carrier of a;
A9: now :: thesis: for x being object st x in F1() holds
ex b being object st S2[x,b]
let x be object ; :: thesis: ( x in F1() implies ex b being object st S2[x,b] )
assume x in F1() ; :: thesis: ex b being object st S2[x,b]
then reconsider a = x as LATTICE by A1;
reconsider b = the carrier of a as object ;
take b = b; :: thesis: S2[x,b]
thus S2[x,b] ; :: thesis: verum
end;
consider D being Function such that
dom D = F1() and
A10: for x being object st x in F1() holds
S2[x,D . x] from deffunc H1( set , set ) -> set = F . [\$1,\$2];
A11: now :: thesis: for a, b being LATTICE st a in F1() & b in F1() holds
for f being set holds
( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) )
let a, b be LATTICE; :: thesis: ( a in F1() & b in F1() implies for f being set holds
( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) ) )

assume ( a in F1() & b in F1() ) ; :: thesis: for f being set holds
( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) )

then [a,b] in [:F1(),F1():] by ZFMISC_1:87;
then S1[[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) & P1[a9,b9,f] ) ) ;
let f be set ; :: thesis: ( ( f in F . [a,b] implies ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b ) ) & ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] ) )
A15: ( a = a9 & b = b9 ) by ;
hereby :: thesis: ( f is monotone Function of a,b & P1[a,b,f] implies f in F . [a,b] )
assume A16: f in F . [a,b] ; :: thesis: ( P1[a,b,f] & f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
hence P1[a,b,f] by A14, A15, A12; :: thesis: ( f in MonFuncs (a,b) & f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
thus f in MonFuncs (a,b) by A14, A15, A16, A12; :: thesis: ( f in Funcs ( the carrier of a, the carrier of b) & f is monotone Function of a,b )
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: verum
end;
assume f is monotone Function of a,b ; :: thesis: ( P1[a,b,f] implies f in F . [a,b] )
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 P1[a,b,f] ; :: thesis: f in F . [a,b]
then f in c by ;
hence f in F . [a,b] by A12; :: thesis: verum
end;
A18: for a, b, c being Element of F1()
for f, g being Function st f in H1(a,b) & g in H1(b,c) holds
g * f in H1(a,c)
proof
let a, b, c be Element of F1(); :: thesis: for f, g being Function st f in H1(a,b) & g in H1(b,c) holds
g * f in H1(a,c)

let f, g be Function; :: thesis: ( f in H1(a,b) & g in H1(b,c) implies g * f in H1(a,c) )
assume that
A19: f in F . [a,b] and
A20: g in F . [b,c] ; :: thesis: g * f in H1(a,c)
reconsider x = a, y = b, z = c as LATTICE by A1;
reconsider g9 = g as monotone Function of y,z by ;
reconsider f9 = f as monotone Function of x,y by ;
( P1[x,y,f9] & P1[y,z,g9] ) by A11, A19, A20;
then P1[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 H1(a,c) by YELLOW_2:12; :: thesis: verum
end;
deffunc H2( set ) -> set = D . \$1;
A21: for a, b being Element of F1() holds H1(a,b) c= Funcs (H2(a),H2(b))
proof
let a, b be Element of F1(); :: thesis: H1(a,b) c= Funcs (H2(a),H2(b))
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in H1(a,b) or f in Funcs (H2(a),H2(b)) )
reconsider x = a, y = b as LATTICE by A1;
assume f in F . [a,b] ; :: thesis: f in Funcs (H2(a),H2(b))
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 (H2(a),H2(b)) by A10; :: thesis: verum
end;
A22: now :: thesis: for a being Element of F1() holds id H2(a) in H1(a,a)
let a be Element of F1(); :: thesis: id H2(a) in H1(a,a)
reconsider x = a as LATTICE by A1;
( id (D . a) = id x & P1[x,x, id x] ) by ;
hence id H2(a) in H1(a,a) by A11; :: thesis: verum
end;
consider C being strict concrete category such that
A23: the carrier of C = F1() and
for a being Object of C holds the_carrier_of a = H2(a) and
A24: for a, b being Object of C holds <^a,b^> = H1(a,b) from take C ; :: thesis: ( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )

thus ( C is semi-functional & C is set-id-inheriting ) ; :: according to YELLOW21:def 4 :: thesis: ( ( for a being Object of C holds a is LATTICE ) & ( for a, b being Object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )

thus for a being Object of C holds a is LATTICE by ; :: thesis: ( ( for a, b being Object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )

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: ( the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
proof
let a, b be Object of C; :: thesis: for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B)

let A, B be LATTICE; :: thesis: ( A = a & B = b implies <^a,b^> c= MonFuncs (A,B) )
assume A25: ( A = a & B = b ) ; :: thesis: <^a,b^> c= MonFuncs (A,B)
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in <^a,b^> or f in MonFuncs (A,B) )
<^a,b^> = F . [A,B] by ;
hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by ; :: thesis: verum
end;
thus the carrier of C = F1() by A23; :: thesis: for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )

let a, b be LATTICE; :: thesis: for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )

let f be monotone Function of a,b; :: thesis: ( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) )
hereby :: thesis: ( a in F1() & b in F1() & P1[a,b,f] implies f in the Arrows of C . (a,b) )
assume A26: f in the Arrows of C . (a,b) ; :: thesis: ( a in F1() & b in F1() & P1[a,b,f] )
then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
then A27: [a,b] in [:F1(),F1():] by A23;
hence ( a in F1() & b in F1() ) by ZFMISC_1:87; :: thesis: P1[a,b,f]
reconsider x = a, y = b as Object of C by ;
the Arrows of C . [a,b] = <^x,y^>
.= F . [x,y] by A24 ;
hence P1[a,b,f] by A11, A23, A26; :: thesis: verum
end;
assume A28: ( a in F1() & b in F1() ) ; :: thesis: ( not P1[a,b,f] or f in the Arrows of C . (a,b) )
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 P1[a,b,f] or f in the Arrows of C . (a,b) ) by ; :: thesis: verum