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 y be set ; :: thesis: ( y in R .: (X \/ Y) iff y in (R .: X) \/ (R .: Y) )

A1: now

A2: now

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

end;

A5: now

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

end;

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

end;

now

assume y in R .: (X \/ Y) ; :: thesis: y in (R .: X) \/ (R .: Y)
then consider x being set such that
A8: [x,y] in R and
A9: x in X \/ Y by Def13;
( x in X or x in Y ) by A9, XBOOLE_0:def 3;
then ( y in R .: X or y in R .: Y ) by A8, Def13;
hence y in (R .: X) \/ (R .: Y) by XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

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