begin
Lm1:
for x being set
for n being Element of NAT st x in Segm n holds
x is Element of NAT
;
:: deftheorem GR_CY_1:def 1 :
canceled;
:: deftheorem defines addint GR_CY_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th16:
:: deftheorem defines Sum GR_CY_1:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th22:
Lm2:
for G being Group
for a being Element of holds Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = a |^ (Sum (<*> INT ))
Lm3:
for G being Group
for a being Element of
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*>))
theorem
canceled;
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
:: deftheorem defines INT.Group GR_CY_1:def 4 :
:: deftheorem Def5 defines addint GR_CY_1:def 5 :
theorem Th34:
:: deftheorem Def6 defines INT.Group GR_CY_1:def 6 :
theorem Th35:
theorem Th36:
:: deftheorem GR_CY_1:def 7 :
canceled;
:: deftheorem defines @' GR_CY_1:def 8 :
theorem Th37:
theorem
canceled;
Lm4:
for k being Element of NAT holds (@' 1) |^ k = k
theorem Th39:
Lm5:
INT.Group = gr {(@' 1)}
:: deftheorem Def9 defines cyclic GR_CY_1:def 9 :
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem Th46:
theorem
theorem Th48:
theorem
theorem