environ
vocabularies HIDDEN, NUMBERS, FINSET_1, FUNCT_1, RELAT_1, CARD_3, GRAPH_1, SUBSET_1, TREES_2, FINSEQ_1, STRUCT_0, GRAPH_2, ARYTM_3, XXREAL_0, NAT_1, PARTFUN1, TARSKI, ORDINAL4, XBOOLE_0, CARD_1, WAYBEL_0, GLIB_000, RELAT_2, FUNCOP_1, ARYTM_1, TREES_4, TREES_1, MSUALG_1, PBOOLE, MSATERM, TREES_9, ZFMISC_1, MSAFREE, MSUALG_2, MSAFREE2, MSUALG_3, PRELAMB, REALSET1, GROUP_6, FUNCT_6, MARGREL1, UNIALG_2, DTCONSTR, TDGROUP, TREES_3, TREES_A, MSSCYC_1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, XCMPLX_0, CARD_1, ORDINAL1, NUMBERS, NAT_1, FINSEQ_2, STRUCT_0, CARD_3, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FUNCOP_1, FINSEQ_1, GRAPH_1, GRAPH_2, TREES_1, TREES_2, TREES_3, FUNCT_6, TREES_4, LANG1, DTCONSTR, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, TREES_9, MSATERM, XXREAL_0, PRE_POLY;
definitions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3, STRUCT_0;
theorems TARSKI, NAT_1, ZFMISC_1, GRAPH_1, GRAPH_2, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_6, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, CARD_1, CARD_3, TREES_1, TREES_3, TREES_4, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, MSATERM, EXTENS_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, RELAT_1, RELSET_1, XTUPLE_0;
schemes NAT_1, FRAENKEL, PBOOLE, DOMAIN_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, PRE_CIRC, TREES_9, STRUCT_0, MSUALG_1, MSAFREE, MSAFREE2, EXTENS_1, ORDINAL1, CARD_1, GRAPH_1, RELSET_1, TREES_1, MSATERM;
constructors HIDDEN, WELLORD2, FINSEQ_4, MSUALG_3, MSATERM, MSAFREE2, GRAPH_2, RELSET_1, PRE_POLY, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MSAFREE;
expansions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3;
Lm1:
for G being Graph
for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)