theorem lemonto: :: FIELD_5:27

for X being non empty set
for Z being set
for r being Renaming of X,Z holds r " is onto