consider p being FinSequence such that

A2: rng p = T and

A3: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def 4;

take Sum p ; :: thesis: ex F being FinSequence of the carrier 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 A2, A3; :: thesis: verum

A2: rng p = T and

A3: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def 4;

take Sum p ; :: thesis: ex F being FinSequence of the carrier 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 A2, A3; :: thesis: verum