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:12;
hence Product <*r*> = r by Def3; :: thesis: verum