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
( rng F c= ExtREAL & rng (F ^ <*r*>) c= ExtREAL ) by VALUED_0:def 2;
then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of ExtREAL by FINSEQ_1:def 4;
reconsider Ff1 = Ff as extreal-yielding FinSequence ;
Product (F ^ <*r*>) = multextreal $$ Fr by Def3;
then Product (F ^ <*r*>) = multextreal . (multextreal $$ Ff),r by FINSOP_1:5;
then Product (F ^ <*r*>) = multextreal . (Product Ff1),r by Def3;
hence Product (F ^ <*r*>) = (Product F) * r by Def2; :: thesis: verum