environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ORDINAL4, ARYTM_3, CARD_1, CARD_3, REAL_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, PARTFUN1, FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, VALUED_0, GRAPH_5, FUNCOP_1, TREES_1, GLIB_001, FUNCT_4, FINSEQ_5, GLIB_003;
notations HIDDEN, TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, RELAT_1, PARTFUN1, FUNCT_1, PBOOLE, RELSET_1, FUNCT_2, VALUED_0, GRAPH_5, RVSUM_1, FINSEQ_5, FINSEQ_1, FINSET_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, RECDEF_1;
definitions ;
theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GRAPH_2, GRAPH_5, INT_1, NAT_1, POLYNOM3, RELAT_1, RELSET_1, RVSUM_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, ENUMSET1, ORDERS_1, ORDINAL1, FINSOP_1, VALUED_0, PARTFUN1, XTUPLE_0;
schemes NAT_1, FINSEQ_1, FUNCT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GRAPH_2, GLIB_002, INT_1, VALUED_0, CARD_1, FUNCT_2, PARTFUN1, RELSET_1;
constructors HIDDEN, DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5, GLIB_001, GLIB_002, RECDEF_1, RELSET_1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities GLIB_000, FUNCOP_1, RVSUM_1;
expansions GLIB_000;
Lm1:
for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G
Lm2:
for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G
Lm3:
for G being _Graph
for X being set holds
( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G )
Lm4:
for x, y, X, Y being set
for f being PartFunc of X,Y st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y