let Y be set ; :: thesis: for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y)
let P, Q be Relation; :: thesis: (P \/ Q) " Y = (P " Y) \/ (Q " Y)
set R = P \/ Q;
set LH = (P \/ Q) " Y;
set RH = (P " Y) \/ (Q " Y);
reconsider PP = P null Q, QQ = Q null P as Subset of (P \/ Q) ;

now

let x be set ; :: thesis: ( x in (P \/ Q) " Y implies x in (P " Y) \/ (Q " Y) )
assume x in (P \/ Q) " Y ; :: thesis: x in (P " Y) \/ (Q " Y)
then consider y being set such that
C0: ( [x,y] in P \/ Q & y in Y ) by RELAT_1:def 14;
set z = [x,y];
( ( [x,y] in P & y in Y ) or ( [x,y] in Q & y in Y ) ) by C0, XBOOLE_0:def 3;
then ( x in P " Y or x in Q " Y ) by RELAT_1:def 14;
hence x in (P " Y) \/ (Q " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

then B0: (P \/ Q) " Y c= (P " Y) \/ (Q " Y) by TARSKI:def 3;
reconsider PX = PP " Y, QX = QQ " Y as Subset of ((P \/ Q) " Y) by RELAT_1:144;
PX \/ QX c= (P \/ Q) " Y ;
hence (P \/ Q) " Y = (P " Y) \/ (Q " Y) by B0, XBOOLE_0:def 10; :: thesis: verum