theorem Th8: :: HILBERT4:3

for f being Function st f * f = id (dom f) holds
f is involutive