let S be set ; :: according to PRVECT_1:def 10 :: thesis: ( not S in rng (G ^ F) or S is addLoopStr )
assume S in rng (G ^ F) ; :: thesis: S is addLoopStr
then consider i being object such that
A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A1;

per cases ( i in dom G or ex n being Nat st
( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25;

suppose A2: i in dom G ; :: thesis: S is addLoopStr

then A3: (G ^ F) . i = G . i by FINSEQ_1:def 7;
G . i in rng G by A2, FUNCT_1:3;
hence S is AbGroup by A3, A1, PRVECT_1:def 10; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom F & i = (len G) + n ) ; :: thesis: S is addLoopStr

then consider n being Nat such that
A4: ( n in dom F & i = (len G) + n ) ;
A5: (G ^ F) . i = F . n by A4, FINSEQ_1:def 7;
F . n in rng F by A4, FUNCT_1:3;
hence S is AbGroup by A5, A1, PRVECT_1:def 10; :: thesis: verum

end;

end;