dom f = X by PARTFUN1:def 2;
hence ( f is involutive implies for x being Element of X holds f . (f . x) = x ) ; :: thesis: ( ( for x being Element of X holds f . (f . x) = x ) implies f is involutive )
assume A1: for x being Element of X holds f . (f . x) = x ; :: thesis: f is involutive
let x be set ; :: according to PARTIT_2:def 2 :: thesis: ( x in dom f implies f . (f . x) = x )
assume x in dom f ; :: thesis: f . (f . x) = x
hence f . (f . x) = x by A1; :: thesis: verum