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

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