let F be extreal-yielding FinSequence; :: thesis: for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r
let r be Element of ExtREAL ; :: thesis: Product (F ^ <*r*>) = (Product F) * r
A1: rng (F ^ <*r*>) c= ExtREAL by VALUED_0:def 2;
rng F c= ExtREAL by VALUED_0:def 2;
then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of ExtREAL by A1, FINSEQ_1:def 4;
reconsider Ff1 = Ff as extreal-yielding FinSequence ;
Product (F ^ <*r*>) = multextreal $$ Fr by Def2;
then Product (F ^ <*r*>) = multextreal . ((multextreal $$ Ff),r) by FINSOP_1:4;
then Product (F ^ <*r*>) = multextreal . ((Product Ff1),r) by Def2;
hence Product (F ^ <*r*>) = (Product F) * r by Def1; :: thesis: verum