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