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

now

let x be set ; :: thesis: ( x in R " (X \/ Y) iff x in (R " X) \/ (R " Y) )

A1: now

assume x in R " (X \/ Y) ; :: thesis: x in (R " X) \/ (R " Y)
then consider y being set such that
A2: ( [x,y] in R & y in X \/ Y ) by Def14;
( ( y in X or y in Y ) & [x,y] in R ) by A2, XBOOLE_0:def 3;
then ( x in R " X or x in R " Y ) by Def14;
hence x in (R " X) \/ (R " Y) by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume A3: x in (R " X) \/ (R " Y) ; :: thesis: x in R " (X \/ Y)

A4: now

assume x in R " X ; :: thesis: x in R " (X \/ Y)
then consider y being set such that
A5: ( [x,y] in R & y in X ) by Def14;
( y in X \/ Y & [x,y] in R ) by A5, XBOOLE_0:def 3;
hence x in R " (X \/ Y) by Def14; :: thesis: verum

end;

now

assume x in R " Y ; :: thesis: x in R " (X \/ Y)
then consider y being set such that
A6: ( [x,y] in R & y in Y ) by Def14;
( y in X \/ Y & [x,y] in R ) by A6, XBOOLE_0:def 3;
hence x in R " (X \/ Y) by Def14; :: thesis: verum

end;

hence x in R " (X \/ Y) by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( x in R " (X \/ Y) iff x in (R " X) \/ (R " Y) ) by A1; :: thesis: verum

end;

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