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

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