let f be Function; :: thesis: ( f * f = id (dom f) implies f is involutive )
assume A1: f * f = id (dom f) ; :: thesis: f is involutive
let x be set ; :: according to PARTIT_2:def 2 :: thesis: ( not x in dom f or f . (f . x) = x )
assume A2: x in dom f ; :: thesis: f . (f . x) = x
hence f . (f . x) = (f * f) . x by FUNCT_1:13
.= x by A1, A2, FUNCT_1:18 ;
:: thesis: verum