let a, a1 be set ; :: thesis: for f being Function st a in {a1,(f . a1)} & f is involutive & a1 in dom f holds
{a,(f . a)} = {a1,(f . a1)}
let f be Function; :: thesis: ( a in {a1,(f . a1)} & f is involutive & a1 in dom f implies {a,(f . a)} = {a1,(f . a1)} )
assume A1: ( a in {a1,(f . a1)} & f is involutive & a1 in dom f ) ; :: thesis: {a,(f . a)} = {a1,(f . a1)}

per cases ( a = a1 or a <> a1 ) ;

suppose a = a1 ; :: thesis: {a,(f . a)} = {a1,(f . a1)}

hence {a,(f . a)} = {a1,(f . a1)} ; :: thesis: verum

end;

suppose a <> a1 ; :: thesis: {a,(f . a)} = {a1,(f . a1)}

then a = f . a1 by A1, TARSKI:def 2;
hence {a,(f . a)} = {a1,(f . a1)} by A1, PARTIT_2:def 2; :: thesis: verum

end;

end;