environ
vocabularies HIDDEN, CLASSES2, CLASSES1, ORDINAL1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, CARD_3, CARD_1, FUNCT_2, PRALG_1, PBOOLE, SUBSET_1, RLVECT_2, STRUCT_0, FUNCOP_1, WAYBEL_3, YELLOW_1, ORDERS_2, WAYBEL_0, XXREAL_0, RELAT_2, ZFMISC_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, RCOMP_1, CONNSP_2, COMPTS_1, MCART_1, TOPS_1, SEQ_2, ORDINAL2, SETFAM_1, YELLOW_6;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_1, CARD_3, FUNCOP_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, STRUCT_0, TOPS_1, COMPTS_1, CONNSP_2, PRALG_1, ORDERS_2, LATTICE3, PRE_TOPC, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3;
definitions TARSKI, STRUCT_0, WAYBEL_0, PRALG_1, YELLOW_1, YELLOW_0, RELAT_1, PRE_TOPC, WAYBEL_3;
theorems CONNSP_2, TOPS_1, FUNCOP_1, WAYBEL_0, PRE_TOPC, ORDERS_2, RELAT_1, FUNCT_2, ZFMISC_1, FUNCT_1, TARSKI, PBOOLE, YELLOW_1, CARD_3, PRALG_1, YELLOW_3, RELSET_1, DOMAIN_1, YELLOW_0, CLASSES2, CLASSES1, CARD_2, FUNCT_6, LATTICE3, SUBSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, PARTFUN1;
schemes PBOOLE, FUNCT_7, SUBSET_1, RELSET_1, DOMAIN_1, MSSUBFAM, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, CARD_1, CLASSES1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, PCOMPS_1, LATTICE3, YELLOW_0, WAYBEL_0, PARTFUN1, YELLOW_1, YELLOW_3, WAYBEL_3, RELSET_1, TOPS_1, RELAT_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, CLASSES1, TOLER_1, CLASSES2, REALSET1, TOPS_1, COMPTS_1, CONNSP_2, LATTICE3, PRALG_1, YELLOW_3, WAYBEL_3, RELSET_1, PBOOLE, XTUPLE_0, WAYBEL_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0, WAYBEL_0, YELLOW_1, BINOP_1, SUBSET_1, WELLORD1;
expansions TARSKI, WAYBEL_0, YELLOW_0, RELAT_1, PRE_TOPC, WAYBEL_3;
Lm1:
for N being non empty RelStr holds
( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
Lm2:
for N being non empty RelStr holds
( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
Lm3:
for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
Lm4:
for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
Lm5:
for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
Lm6:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being constant net of S1 holds N is constant net of S2
Lm7:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
definition
let T be non
empty 1-sorted ;
let Y be
net of
T;
let J be
net_set of the
carrier of
Y,
T;
existence
ex b1 being strict net of T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) )
uniqueness
for b1, b2 being strict net of T st RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b2 . (i,f) = the mapping of (J . i) . (f . i) ) holds
b1 = b2
end;