theorem Th1: :: PENCIL_1:1

for f, g being Function st product f = product g & f is non-empty holds
g is non-empty