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