theorem Th5: :: GLIBPRE1:5

for f being empty Function holds .: f = {} .--> {}