rng F c= ExtREAL by VALUED_0:def 2;
then reconsider f = F as FinSequence of ExtREAL by FINSEQ_1:def 4;
take multextreal $$ f ; :: thesis: ex f being FinSequence of ExtREAL st
( f = F & multextreal $$ f = multextreal $$ f )
thus ex f being FinSequence of ExtREAL st
( f = F & multextreal $$ f = multextreal $$ f ) ; :: thesis: verum