for Y being set
for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y)