environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_1, GROUP_1, FINSEQ_1, XCMPLX_0, CARD_1, XBOOLE_0, BINOP_2, FUNCT_1, BINOP_1, ARYTM_3, CARD_3, SETWISEO, RELAT_1, TARSKI, NAT_1, SETWOP_2, FINSEQ_2, NEWTON, STRUCT_0, ORDINAL4, QC_LANG1, GROUP_4, ARYTM_1, FINSET_1, XXREAL_0, GROUP_2, ALGSTR_0, ZFMISC_1, REALSET1, REAL_1, INT_2, RLSUB_1, GRAPH_1, GR_CY_1, MEMBERED, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, FINSET_1, BINOP_1, DOMAIN_1, INT_1, FINSEQ_1, FINSEQ_2, SETWISEO, SETWOP_2, BINOP_2, REALSET1, INT_2, NAT_1, NAT_D, MEMBERED, RVSUM_1, XXREAL_0, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4;
definitions FUNCT_1, TARSKI, STRUCT_0, GROUP_1;
theorems BINOP_1, INT_1, INT_2, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, ZFMISC_1, FUNCT_2, FUNCOP_1, GROUP_1, GROUP_2, GROUP_4, TARSKI, FUNCT_1, CARD_1, WELLORD2, FINSOP_1, RELSET_1, XBOOLE_0, RELAT_1, BINOP_2, NUMBERS, SETWISEO, XREAL_1, XXREAL_0, ORDINAL1, RVSUM_1, SETWOP_2, FINSEQ_3, NAT_D, STRUCT_0;
schemes BINOP_1, NAT_1, FINSEQ_1, FINSEQ_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, GROUP_2, VALUED_0, ALGSTR_0, CARD_1, FINSEQ_2, ZFMISC_1, ORDINAL1;
constructors HIDDEN, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2, FINSOP_1, SETWOP_2, RVSUM_1, REALSET1, GROUP_4, FUNCOP_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, REALSET1, FINSEQ_2, FINSEQ_1, STRUCT_0, GROUP_2, GROUP_4, SETWOP_2, CARD_1, ALGSTR_0, ORDINAL1;
expansions TARSKI, BINOP_1, STRUCT_0, GROUP_1;
Lm1:
for x being set
for n being Nat st x in Segm n holds
x is Element of NAT
;
Lm2:
for G being Group
for a being Element of G holds Product (((len (<*> INT)) |-> a) |^ (<*> INT)) = a |^ (Sum (<*> INT))
Lm3:
for G being Group
for a being Element of G
for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
Lm4:
for k being Nat holds (@' 1) |^ k = k
Lm5:
INT.Group = gr {(@' 1)}