now :: thesis: for S being set st S in rng <*G*> holds
S is AbGroup

let S be set ; :: thesis: ( S in rng <*G*> implies S is AbGroup )
assume S in rng <*G*> ; :: thesis: S is AbGroup
then consider i being object such that
A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A1;
dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then i = 1 by A1, TARSKI:def 1;
hence S is AbGroup by A1; :: thesis: verum

end;

hence for b₁ being FinSequence st b₁ = <*G*> holds
( not b₁ is empty & b₁ is AbGroup-yielding ) by PRVECT_1:def 10; :: thesis: verum