Product (<*> ExtREAL ) = multextreal $$ (<*> ExtREAL ) by Def3;
hence Product (<*> ExtREAL ) = 1 by Th5, FINSOP_1:11; :: thesis: verum