theorem :: FOMODEL0:70

for a, a1 being set
for f being Function st a in {a1,(f . a1)} & f is involutive & a1 in dom f holds
{a,(f . a)} = {a1,(f . a1)} by Lm69;