let g be Function; :: thesis: ( g is symmetric implies g is involutive )
set G = field g;
set D = dom g;
set C = rng g;
assume g is symmetric ; :: thesis: g is involutive
then A1: g is_symmetric_in field g by RELAT_2:def 11;
now :: thesis: for x being set st x in (dom g) null (rng g) holds
x = g . (g . x)
let x be set ; :: thesis: ( x in (dom g) null (rng g) implies x = g . (g . x) )
set y = g . x;
assume A2: x in (dom g) null (rng g) ; :: thesis: x = g . (g . x)
then ( g . x in (rng g) null (dom g) & [x,(g . x)] in g ) by FUNCT_1:3, FUNCT_1:def 2;
then [(g . x),x] in g by A2, A1, RELAT_2:def 3;
hence x = g . (g . x) by FUNCT_1:1; :: thesis: verum
end;
hence g is involutive by PARTIT_2:def 2; :: thesis: verum