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 :: thesis: for x being object st x in (P \/ Q) " Y holds
x in (P " Y) \/ (Q " Y)
let x be object ; :: 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 object such that
A1: ( [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 XBOOLE_0:def 3, A1;
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 A2: (P \/ Q) " Y c= (P " Y) \/ (Q " Y) ;
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 A2; :: thesis: verum