let g be RealNormSpace-yielding FinSequence; :: thesis: g is RealLinearSpace-yielding
for x being set st x in rng g holds
x is RealLinearSpace by Def10;
hence g is RealLinearSpace-yielding by Def3; :: thesis: verum