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