let R, S be Relation; :: thesis: for Y being set holds (R \/ S) " Y = (R " Y) \/ (S " Y)
let Y be set ; :: thesis: (R \/ S) " Y = (R " Y) \/ (S " Y)

now :: thesis: for x being object holds
( ( x in (R \/ S) " Y implies x in (R " Y) \/ (S " Y) ) & ( x in (R " Y) \/ (S " Y) implies x in (R \/ S) " Y ) )

let x be object ; :: thesis: ( ( x in (R \/ S) " Y implies x in (R " Y) \/ (S " Y) ) & ( x in (R " Y) \/ (S " Y) implies b₁ in (R \/ S) " Y ) )

hereby :: thesis: ( x in (R " Y) \/ (S " Y) implies b₁ in (R \/ S) " Y )

assume x in (R \/ S) " Y ; :: thesis: x in (R " Y) \/ (S " Y)
then consider y being object such that
A1: ( [x,y] in R \/ S & y in Y ) by RELAT_1:def 14;

per cases ( [x,y] in R or [x,y] in S ) by A1, XBOOLE_0:def 3;

suppose [x,y] in R ; :: thesis: x in (R " Y) \/ (S " Y)

then x in R " Y by A1, RELAT_1:def 14;
hence x in (R " Y) \/ (S " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose [x,y] in S ; :: thesis: x in (R " Y) \/ (S " Y)

then x in S " Y by A1, RELAT_1:def 14;
hence x in (R " Y) \/ (S " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume x in (R " Y) \/ (S " Y) ; :: thesis: b₁ in (R \/ S) " Y

per cases then ( x in R " Y or x in S " Y ) by XBOOLE_0:def 3;

suppose x in R " Y ; :: thesis: b₁ in (R \/ S) " Y

then consider y being object such that
A2: ( [x,y] in R & y in Y ) by RELAT_1:def 14;
[x,y] in R \/ S by A2, XBOOLE_0:def 3;
hence x in (R \/ S) " Y by A2, RELAT_1:def 14; :: thesis: verum

end;

suppose x in S " Y ; :: thesis: b₁ in (R \/ S) " Y

then consider y being object such that
A3: ( [x,y] in S & y in Y ) by RELAT_1:def 14;
[x,y] in R \/ S by A3, XBOOLE_0:def 3;
hence x in (R \/ S) " Y by A3, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

hence (R \/ S) " Y = (R " Y) \/ (S " Y) by TARSKI:2; :: thesis: verum