environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, RLVECT_1, XBOOLE_0, ALGSTR_0, BINOP_1, FUNCT_1, ARYTM_3, RELAT_1, VECTSP_1, MESFUNC1, ALGSTR_1, SUPINF_2, SETWISEO, LATTICES, STRUCT_0, FUNCOP_1, ARYTM_1, FINSEQOP, FINSEQ_1, FINSEQ_2, TARSKI, RVSUM_1, ORDINAL4, XXREAL_0, NAT_1, CARD_3, FINSUB_1, FINSEQ_4, SETWOP_2, FINSET_1, CARD_1, PARTFUN1, FINSOP_1, GROUP_1, FVSUM_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1, FINSEQ_4, BINOP_1, FUNCOP_1, RLVECT_1, SETWISEO, FINSOP_1, FINSEQ_2, FINSEQOP, SETWOP_2, GROUP_1, ALGSTR_1, GROUP_4, VECTSP_1, FINSET_1, FINSUB_1, MATRIX_1, XXREAL_0;
definitions SETWISEO, ALGSTR_1;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_1, FUNCT_2, NAT_1, BINOP_1, FINSEQOP, VECTSP_1, FUNCOP_1, SETWOP_2, RLVECT_1, RELAT_1, SETWISEO, FINSEQ_3, ZFMISC_1, FINSEQ_4, ALGSTR_1, FINSOP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL1, GROUP_4, XXREAL_0, PARTFUN1, CARD_1;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, FINSUB_1, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, CARD_1, GROUP_1;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, FINSEQOP, FINSEQ_4, FINSOP_1, SETWOP_2, ALGSTR_1, GROUP_4, MATRIX_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities GROUP_4, ALGSTR_0;
expansions ;
Lm1:
for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
Lm2:
for i being Nat
for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
Lm3:
for i being Nat
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
Lm4:
for i being Nat
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R, R1, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
Lm5:
for K being non empty multMagma
for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
Lm6:
for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
:: Some Operations on the i-tuples on Element of K
::