let f be involutive Function; :: thesis: ( rng f c= dom f implies f * f = id (dom f) )
assume rng f c= dom f ; :: thesis: f * f = id (dom f)
then A1: dom (f * f) = dom (id (dom f)) by RELAT_1:27;

now :: thesis: for x being object st x in dom (f * f) holds
(f * f) . x = (id (dom f)) . x

let x be object ; :: thesis: ( x in dom (f * f) implies (f * f) . x = (id (dom f)) . x )
assume A2: x in dom (f * f) ; :: thesis: (f * f) . x = (id (dom f)) . x
hence (f * f) . x = f . (f . x) by FUNCT_1:12
.= x by A1, A2, PARTIT_2:def 2
.= (id (dom f)) . x by A1, A2, FUNCT_1:18 ;
:: thesis: verum

end;

hence f * f = id (dom f) by A1, FUNCT_1:2; :: thesis: verum