theorem :: GROUP_4:25

for G being Group
for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 1)) = F