:: deftheorem Def1 defines |^ GROUP_5:def 1 :
for G being Group
for F being FinSequence of the carrier of G
for a being Element of G
for b₄ being FinSequence of the carrier of G holds
( b₄ = F |^ a iff ( len b₄ = len F & ( for k being Nat st k in dom F holds
b₄ . k = (F /. k) |^ a ) ) );