deffunc H_{1}( set ) -> set = the carrier of (c_{1} as_1-sorted);

let C be category; :: thesis: ( C is lattice-wise implies ( C is concrete & C is carrier-underlaid ) )

assume that

A1: ( C is semi-functional & C is set-id-inheriting ) and

A2: for a being Object of C holds a is LATTICE and

A3: for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ; :: according to YELLOW21:def 4 :: thesis: ( C is concrete & C is carrier-underlaid )

consider F being ManySortedSet of C such that

A4: for i being Element of C holds F . i = H_{1}(i)
from PBOOLE:sch 5();

C is para-functional

let a be Object of C; :: according to YELLOW21:def 3 :: thesis: ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S )

reconsider S = a as LATTICE by A2;

( idm a in <^a,a^> & <^a,a^> c= MonFuncs (S,S) ) by A3;

then consider f being Function of S,S such that

A7: idm a = f and

A8: f in Funcs ( the carrier of S, the carrier of S) and

f is monotone by ORDERS_3:def 6;

take S ; :: thesis: ( a = S & the_carrier_of a = the carrier of S )

thus a = S ; :: thesis: the_carrier_of a = the carrier of S

thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:45

.= dom f by A1, A7

.= the carrier of S by A8, FUNCT_2:92 ; :: thesis: verum

let C be category; :: thesis: ( C is lattice-wise implies ( C is concrete & C is carrier-underlaid ) )

assume that

A1: ( C is semi-functional & C is set-id-inheriting ) and

A2: for a being Object of C holds a is LATTICE and

A3: for a, b being Object of C

for A, B being LATTICE st A = a & B = b holds

<^a,b^> c= MonFuncs (A,B) ; :: according to YELLOW21:def 4 :: thesis: ( C is concrete & C is carrier-underlaid )

consider F being ManySortedSet of C such that

A4: for i being Element of C holds F . i = H

C is para-functional

proof

hence
C is concrete
by A1; :: thesis: C is carrier-underlaid
take
F
; :: according to YELLOW18:def 7 :: thesis: for b_{1}, b_{2} being Element of the carrier of C holds <^b_{1},b_{2}^> c= Funcs ((F . b_{1}),(F . b_{2}))

let a, b be Object of C; :: thesis: <^a,b^> c= Funcs ((F . a),(F . b))

reconsider A = a, B = b as LATTICE by A2;

A5: <^a,b^> c= MonFuncs (A,B) by A3;

b as_1-sorted = B by Def1;

then A6: F . b = the carrier of B by A4;

a as_1-sorted = A by Def1;

then F . a = the carrier of A by A4;

then MonFuncs (A,B) c= Funcs ((F . a),(F . b)) by A6, ORDERS_3:11;

hence <^a,b^> c= Funcs ((F . a),(F . b)) by A5; :: thesis: verum

end;let a, b be Object of C; :: thesis: <^a,b^> c= Funcs ((F . a),(F . b))

reconsider A = a, B = b as LATTICE by A2;

A5: <^a,b^> c= MonFuncs (A,B) by A3;

b as_1-sorted = B by Def1;

then A6: F . b = the carrier of B by A4;

a as_1-sorted = A by Def1;

then F . a = the carrier of A by A4;

then MonFuncs (A,B) c= Funcs ((F . a),(F . b)) by A6, ORDERS_3:11;

hence <^a,b^> c= Funcs ((F . a),(F . b)) by A5; :: thesis: verum

let a be Object of C; :: according to YELLOW21:def 3 :: thesis: ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S )

reconsider S = a as LATTICE by A2;

( idm a in <^a,a^> & <^a,a^> c= MonFuncs (S,S) ) by A3;

then consider f being Function of S,S such that

A7: idm a = f and

A8: f in Funcs ( the carrier of S, the carrier of S) and

f is monotone by ORDERS_3:def 6;

take S ; :: thesis: ( a = S & the_carrier_of a = the carrier of S )

thus a = S ; :: thesis: the_carrier_of a = the carrier of S

thus the_carrier_of a = dom (id (the_carrier_of a)) by RELAT_1:45

.= dom f by A1, A7

.= the carrier of S by A8, FUNCT_2:92 ; :: thesis: verum