consider p being FinSequence such that

A1: rng p = T and

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

reconsider p = p as FinSequence of the carrier of INT.Ring by A1, FINSEQ_1:def 4;

INT = the carrier of INT.Ring by INT_3:def 3;

then reconsider F = p as FinSequence of INT ;

reconsider Sp = Sum F as Element of INT.Ring by INT_3:def 3;

take Sp ; :: thesis: ex F being FinSequence of INT st

( rng F = T & F is one-to-one & Sp = Sum F )

take F ; :: thesis: ( rng F = T & F is one-to-one & Sp = Sum F )

thus ( rng F = T & F is one-to-one & Sum F = Sp ) by A1, A2; :: thesis: verum

A1: rng p = T and

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

reconsider p = p as FinSequence of the carrier of INT.Ring by A1, FINSEQ_1:def 4;

INT = the carrier of INT.Ring by INT_3:def 3;

then reconsider F = p as FinSequence of INT ;

reconsider Sp = Sum F as Element of INT.Ring by INT_3:def 3;

take Sp ; :: thesis: ex F being FinSequence of INT st

( rng F = T & F is one-to-one & Sp = Sum F )

take F ; :: thesis: ( rng F = T & F is one-to-one & Sp = Sum F )

thus ( rng F = T & F is one-to-one & Sum F = Sp ) by A1, A2; :: thesis: verum