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