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;

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

hence
f * f = id (dom f)
by A1, FUNCT_1:2; :: thesis: verum(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;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