defpred S_{1}[ 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_{1}[a,b,f] ) ) ) );

set A = F_{1}();

dom F = [:F_{1}(),F_{1}():]
and

A8: for x being object st x in [:F_{1}(),F_{1}():] holds

S_{1}[x,F . x]
from CLASSES1:sch 1(A4);

defpred S_{2}[ object , object ] means for a being LATTICE st a = $1 holds

$2 = the carrier of a;

dom D = F_{1}()
and

A10: for x being object st x in F_{1}() holds

S_{2}[x,D . x]
from CLASSES1:sch 1(A9);

deffunc H_{1}( set , set ) -> set = F . [$1,$2];

_{1}()

for f, g being Function st f in H_{1}(a,b) & g in H_{1}(b,c) holds

g * f in H_{1}(a,c)
_{2}( set ) -> set = D . $1;

A21: for a, b being Element of F_{1}() holds H_{1}(a,b) c= Funcs (H_{2}(a),H_{2}(b))

A23: the carrier of C = F_{1}()
and

for a being Object of C holds the_carrier_of a = H_{2}(a)
and

A24: for a, b being Object of C holds <^a,b^> = H_{1}(a,b)
from YELLOW18:sch 16(A18, A21, A22);

take C ; :: thesis: ( C is lattice-wise & the carrier of C = F_{1}() & ( 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 F_{1}() & b in F_{1}() & P_{1}[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 = F_{1}() & ( 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 F_{1}() & b in F_{1}() & P_{1}[a,b,f] ) ) ) )

thus for a being Object of C holds a is LATTICE by A1, A23; :: 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 = F_{1}() & ( 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 F_{1}() & b in F_{1}() & P_{1}[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 = F_{1}() & ( 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 F_{1}() & b in F_{1}() & P_{1}[a,b,f] ) ) ) )_{1}()
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 F_{1}() & b in F_{1}() & P_{1}[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 F_{1}() & b in F_{1}() & P_{1}[a,b,f] ) )

let f be monotone Function of a,b; :: thesis: ( f in the Arrows of C . (a,b) iff ( a in F_{1}() & b in F_{1}() & P_{1}[a,b,f] ) )

_{1}() & b in F_{1}() )
; :: thesis: ( not P_{1}[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 P_{1}[a,b,f] or f in the Arrows of C . (a,b) )
by A11, A28; :: thesis: verum

( c = $2 & $1 = [a,b] & ( for f being object holds

( f in c iff ( f in MonFuncs (a,b) & P

set A = F

A4: now :: thesis: for x being object st x in [:F_{1}(),F_{1}():] holds

ex y being object st S_{1}[x,y]

consider F being Function such that ex y being object st S

let x be object ; :: thesis: ( x in [:F_{1}(),F_{1}():] implies ex y being object st S_{1}[x,y] )

assume x in [:F_{1}(),F_{1}():]
; :: thesis: ex y being object st S_{1}[x,y]

then consider a, b being object such that

A5: ( a in F_{1}() & b in F_{1}() )
and

A6: x = [a,b] by ZFMISC_1:def 2;

reconsider a = a, b = b as LATTICE by A1, A5;

defpred S_{2}[ object ] means P_{1}[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_{2}[f] ) )
from XBOOLE_0:sch 1();

reconsider y = y as object ;

take y = y; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A6, A7; :: thesis: verum

end;assume x in [:F

then consider a, b being object such that

A5: ( a in F

A6: x = [a,b] by ZFMISC_1:def 2;

reconsider a = a, b = b as LATTICE by A1, A5;

defpred S

consider y being set such that

A7: for f being object holds

( f in y iff ( f in MonFuncs (a,b) & S

reconsider y = y as object ;

take y = y; :: thesis: S

thus S

dom F = [:F

A8: for x being object st x in [:F

S

defpred S

$2 = the carrier of a;

A9: now :: thesis: for x being object st x in F_{1}() holds

ex b being object st S_{2}[x,b]

consider D being Function such that ex b being object st S

let x be object ; :: thesis: ( x in F_{1}() implies ex b being object st S_{2}[x,b] )

assume x in F_{1}()
; :: thesis: ex b being object st S_{2}[x,b]

then reconsider a = x as LATTICE by A1;

reconsider b = the carrier of a as object ;

take b = b; :: thesis: S_{2}[x,b]

thus S_{2}[x,b]
; :: thesis: verum

end;assume x in F

then reconsider a = x as LATTICE by A1;

reconsider b = the carrier of a as object ;

take b = b; :: thesis: S

thus S

dom D = F

A10: for x being object st x in F

S

deffunc H

A11: now :: thesis: for a, b being LATTICE st a in F_{1}() & b in F_{1}() holds

for f being set holds

( ( f in F . [a,b] implies ( P_{1}[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 & P_{1}[a,b,f] implies f in F . [a,b] ) )

A18:
for a, b, c being Element of Ffor f being set holds

( ( f in F . [a,b] implies ( P

let a, b be LATTICE; :: thesis: ( a in F_{1}() & b in F_{1}() implies for f being set holds

( ( f in F . [a,b] implies ( P_{1}[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 & P_{1}[a,b,f] implies f in F . [a,b] ) ) )

assume ( a in F_{1}() & b in F_{1}() )
; :: thesis: for f being set holds

( ( f in F . [a,b] implies ( P_{1}[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 & P_{1}[a,b,f] implies f in F . [a,b] ) )

then [a,b] in [:F_{1}(),F_{1}():]
by ZFMISC_1:87;

then S_{1}[[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_{1}[a9,b9,f] ) )
;

let f be set ; :: thesis: ( ( f in F . [a,b] implies ( P_{1}[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 & P_{1}[a,b,f] implies f in F . [a,b] ) )

A15: ( a = a9 & b = b9 ) by A13, XTUPLE_0:1;

_{1}[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 P_{1}[a,b,f]
; :: thesis: f in F . [a,b]

then f in c by A14, A15, A17;

hence f in F . [a,b] by A12; :: thesis: verum

end;( ( f in F . [a,b] implies ( P

assume ( a in F

( ( f in F . [a,b] implies ( P

then [a,b] in [:F

then S

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

let f be set ; :: thesis: ( ( f in F . [a,b] implies ( P

A15: ( a = a9 & b = b9 ) by A13, XTUPLE_0:1;

hereby :: thesis: ( f is monotone Function of a,b & P_{1}[a,b,f] implies f in F . [a,b] )

assume
f is monotone Function of a,b
; :: thesis: ( Passume A16:
f in F . [a,b]
; :: thesis: ( P_{1}[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 P_{1}[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;hence P

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

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

then f in c by A14, A15, A17;

hence f in F . [a,b] by A12; :: thesis: verum

for f, g being Function st f in H

g * f in H

proof

deffunc H
let a, b, c be Element of F_{1}(); :: thesis: for f, g being Function st f in H_{1}(a,b) & g in H_{1}(b,c) holds

g * f in H_{1}(a,c)

let f, g be Function; :: thesis: ( f in H_{1}(a,b) & g in H_{1}(b,c) implies g * f in H_{1}(a,c) )

assume that

A19: f in F . [a,b] and

A20: g in F . [b,c] ; :: thesis: g * f in H_{1}(a,c)

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_{1}[x,y,f9] & P_{1}[y,z,g9] )
by A11, A19, A20;

then P_{1}[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_{1}(a,c)
by YELLOW_2:12; :: thesis: verum

end;g * f in H

let f, g be Function; :: thesis: ( f in H

assume that

A19: f in F . [a,b] and

A20: g in F . [b,c] ; :: thesis: g * f in H

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

then P

then ( g9 * f9 is monotone Function of x,z implies g9 * f9 in F . [x,z] ) by A11;

hence g * f in H

A21: for a, b being Element of F

proof

let a, b be Element of F_{1}(); :: thesis: H_{1}(a,b) c= Funcs (H_{2}(a),H_{2}(b))

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in H_{1}(a,b) or f in Funcs (H_{2}(a),H_{2}(b)) )

reconsider x = a, y = b as LATTICE by A1;

assume f in F . [a,b] ; :: thesis: f in Funcs (H_{2}(a),H_{2}(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 (H_{2}(a),H_{2}(b))
by A10; :: thesis: verum

end;let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in H

reconsider x = a, y = b as LATTICE by A1;

assume f in F . [a,b] ; :: thesis: f in Funcs (H

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

A22: now :: thesis: for a being Element of F_{1}() holds id H_{2}(a) in H_{1}(a,a)

consider C being strict concrete category such that let a be Element of F_{1}(); :: thesis: id H_{2}(a) in H_{1}(a,a)

reconsider x = a as LATTICE by A1;

( id (D . a) = id x & P_{1}[x,x, id x] )
by A3, A10;

hence id H_{2}(a) in H_{1}(a,a)
by A11; :: thesis: verum

end;reconsider x = a as LATTICE by A1;

( id (D . a) = id x & P

hence id H

A23: the carrier of C = F

for a being Object of C holds the_carrier_of a = H

A24: for a, b being Object of C holds <^a,b^> = H

take C ; :: thesis: ( C is lattice-wise & the carrier of C = F

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in 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 = F

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in F

thus for a being Object of C holds a is LATTICE by A1, A23; :: 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 = F

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in 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 = F

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in F

proof

thus
the carrier of C = F
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 A24, A25;

hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by A11, A23, A25; :: thesis: verum

end;<^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 A24, A25;

hence ( not f in <^a,b^> or f in MonFuncs (A,B) ) by A11, A23, A25; :: thesis: verum

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in 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 F

let f be monotone Function of a,b; :: thesis: ( f in the Arrows of C . (a,b) iff ( a in F

hereby :: thesis: ( a in F_{1}() & b in F_{1}() & P_{1}[a,b,f] implies f in the Arrows of C . (a,b) )

assume A28:
( a in Fassume A26:
f in the Arrows of C . (a,b)
; :: thesis: ( a in F_{1}() & b in F_{1}() & P_{1}[a,b,f] )

then [a,b] in dom the Arrows of C by FUNCT_1:def 2;

then A27: [a,b] in [:F_{1}(),F_{1}():]
by A23;

hence ( a in F_{1}() & b in F_{1}() )
by ZFMISC_1:87; :: thesis: P_{1}[a,b,f]

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_{1}[a,b,f]
by A11, A23, A26; :: thesis: verum

end;then [a,b] in dom the Arrows of C by FUNCT_1:def 2;

then A27: [a,b] in [:F

hence ( a in F

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

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