theorem :: GROUP_4:26

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