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