environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, ORDINAL4, RELAT_1, CARD_1, SUBSET_1, XXREAL_0, RFINSEQ, ARYTM_1, ARYTM_3, JORDAN3, FUNCT_1, FINSEQ_5, NAT_1, PARTFUN1, FINSEQ_8, FILEREC1;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, RELAT_1, RFINSEQ, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_6, FINSEQ_5, FINSEQ_8;
definitions ;
theorems NAT_1, NAT_2, REVROT_1, JORDAN4, FINSEQ_1, FINSEQ_2, FINSEQ_5, FINSEQ_6, RFINSEQ, FUNCT_2, FINSEQ_8, GENEALG1, TOPREAL3, CALCUL_1, FINSEQ_3, XREAL_1, CARD_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_5, ORDINAL1, CARD_1, NAT_1;
constructors HIDDEN, NAT_1, RFINSEQ, NAT_D, FINSEQ_4, FINSEQ_5, CQC_LANG, FINSEQ_6, FINSEQ_8, REAL_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions ;
theorem Th1:
for
p,
q,
r,
s being
FinSequence holds
(
((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s &
((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) &
(p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) )