theorem Th7: :: HILBERT4:2

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