deffunc H1( set ) -> set = the carrier of (c1 as_1-sorted);
let C be category; ( 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)
; YELLOW21:def 4 ( 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 = H1(i)
from PBOOLE:sch 5();
C is para-functional
proof
take
F
;
YELLOW18:def 7 for b1, b2 being Element of the carrier of C holds <^b1,b2^> c= Funcs ((F . b1),(F . b2))
let a,
b be
Object of
C;
<^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;
verum
end;
hence
C is concrete
by A1; C is carrier-underlaid
let a be Object of C; YELLOW21:def 3 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
; ( a = S & the_carrier_of a = the carrier of S )
thus
a = S
; 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
; verum