let a, a1 be set ; :: thesis: for f being Function st ( a in {a1,(f . a1)} or f . a in {a1,(f . a1)} ) & f is involutive & a in dom f & a1 in dom f holds
{a,(f . a)} = {a1,(f . a1)}
let f be Function; :: thesis: ( ( a in {a1,(f . a1)} or f . a in {a1,(f . a1)} ) & f is involutive & a in dom f & a1 in dom f implies {a,(f . a)} = {a1,(f . a1)} )
set X1 = {a1,(f . a1)};
set X = {a,(f . a)};
assume A1: ( ( a in {a1,(f . a1)} or f . a in {a1,(f . a1)} ) & f is involutive & a in dom f & a1 in dom f ) ; :: thesis: {a,(f . a)} = {a1,(f . a1)}
assume A2: not {a,(f . a)} = {a1,(f . a1)} ; :: thesis: contradiction
then {a1,(f . a1)} = {(f . a),(f . (f . a))} by Lm69, A1
.= {(f . a),a} by A1, PARTIT_2:def 2 ;
hence contradiction by A2; :: thesis: verum