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

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

end;

now

assume A3: y in (R .: X) \/ (R .: Y) ; :: thesis: y in R .: (X \/ Y)

A4: now

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

end;

now

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

end;

hence y in R .: (X \/ Y) by A3, A4, 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