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