Product (<*> REAL) = 1 by BINOP_2:7, FINSOP_1:10;
hence for F being empty FinSequence holds Product F = 1 ; :: thesis: verum