for a, a1 being set
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)} by Lm70;