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

A2: now

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

end;

A5: now

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

end;

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

end;

now

assume x in R " (X \/ Y) ; :: thesis: x in (R " X) \/ (R " Y)
then consider y being set such that
A8: [x,y] in R and
A9: y in X \/ Y by Def14;
( y in X or y in Y ) by A9, XBOOLE_0:def 3;
then ( x in R " X or x in R " Y ) by A8, Def14;
hence x in (R " X) \/ (R " Y) by 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