theorem unres (A F G: set): $ F u. G |` A == (F |` A) u. (G |` A) $;
(F u. G) i^i Xp A _V == F i^i Xp A _V u. G i^i Xp A _V
F u. G |` A == (F |` A) u. (G |` A)