let f be Function; :: thesis: ( f is involutive implies f is one-to-one )
assume A1: f is involutive ; :: thesis: f is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then ( f . (f . x1) = x1 & f . (f . x2) = x2 ) by A1, PARTIT_2:def 2;
hence ( not f . x1 = f . x2 or x1 = x2 ) ; :: thesis: verum