consider p being FinSequence such that
A1: rng p = T and
A2: p is one-to-one by FINSEQ_4:73;
reconsider p = p as FinSequence of V by A1, FINSEQ_1:def 4;
take Sum p ; :: thesis: ex F being FinSequence of V st
( rng F = T & F is one-to-one & Sum p = Sum F )
take p ; :: thesis: ( rng p = T & p is one-to-one & Sum p = Sum p )
thus ( rng p = T & p is one-to-one & Sum p = Sum p ) by A1, A2; :: thesis: verum