let r be Element of ExtREAL ; :: thesis: Product <*r*> = r
reconsider r9 = r as Element of ExtREAL ;
reconsider F = <*r9*> as FinSequence of ExtREAL ;
multextreal $$ F = r by FINSOP_1:11;
hence Product <*r*> = r by Def2; :: thesis: verum