let F be VectorSpace-Sequence of K; :: thesis: F is AbGroup-yielding
for x being set st x in rng F holds
x is AbGroup by Def3;
hence F is AbGroup-yielding by PRVECT_1:def 10; :: thesis: verum