for M being non empty set
for F, G being Function st F is_definable_in M & G is_definable_in M holds
F * G is_definable_in M