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

now :: thesis: for y being object holds
( ( y in (R \/ S) .: X implies y in (R .: X) \/ (S .: X) ) & ( y in (R .: X) \/ (S .: X) implies y in (R \/ S) .: X ) )

let y be object ; :: thesis: ( ( y in (R \/ S) .: X implies y in (R .: X) \/ (S .: X) ) & ( y in (R .: X) \/ (S .: X) implies b₁ in (R \/ S) .: X ) )

hereby :: thesis: ( y in (R .: X) \/ (S .: X) implies b₁ in (R \/ S) .: X )

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

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

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

then y in R .: X by A1, RELAT_1:def 13;
hence y in (R .: X) \/ (S .: X) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then y in S .: X by A1, RELAT_1:def 13;
hence y in (R .: X) \/ (S .: X) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume y in (R .: X) \/ (S .: X) ; :: thesis: b₁ in (R \/ S) .: X

per cases then ( y in R .: X or y in S .: X ) by XBOOLE_0:def 3;

suppose y in R .: X ; :: thesis: b₁ in (R \/ S) .: X

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

end;

suppose y in S .: X ; :: thesis: b₁ in (R \/ S) .: X

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

end;

end;

end;

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