theorem Th1: :: YELLOW_6:1

for T being Universe
for f being Function st dom f in T & rng f c= T holds
product f in T