let f be Function; :: thesis: ( f is involutive implies f * f c= id (dom f) )
assume f is involutive ; :: thesis: f * f c= id (dom f)
then reconsider ff = f as involutive Function ;
set g = ff * ff;
set df = dom ff;
set dg = dom (ff * ff);
set I = id (dom ff);

now :: thesis: for x being set st x in dom (ff * ff) holds
( x in dom (id (dom ff)) & (id (dom ff)) . x = (ff * ff) . x )

let x be set ; :: thesis: ( x in dom (ff * ff) implies ( x in dom (id (dom ff)) & (id (dom ff)) . x = (ff * ff) . x ) )
assume A1: x in dom (ff * ff) ; :: thesis: ( x in dom (id (dom ff)) & (id (dom ff)) . x = (ff * ff) . x )
then A2: x in dom ff by RELAT_1:25, TARSKI:def 3;
thus x in dom (id (dom ff)) by RELAT_1:25, TARSKI:def 3, A1; :: thesis: (id (dom ff)) . x = (ff * ff) . x
thus (id (dom ff)) . x = x by FUNCT_1:18, A2
.= f . (f . x) by A2, PARTIT_2:def 2
.= (ff * ff) . x by FUNCT_1:13, A2 ; :: thesis: verum

end;

hence f * f c= id (dom f) by Th51; :: thesis: verum