begin
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)}