let x be set ; :: thesis: for R1, R2 being Relation holds Im (R1 \/ R2),x = (Im R1,x) \/ (Im R2,x)
let R1, R2 be Relation; :: thesis: Im (R1 \/ R2),x = (Im R1,x) \/ (Im R2,x)
thus Im (R1 \/ R2),x c= (Im R1,x) \/ (Im R2,x) :: according to XBOOLE_0:def 10 :: thesis: (Im R1,x) \/ (Im R2,x) c= Im (R1 \/ R2),x

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Im (R1 \/ R2),x or y in (Im R1,x) \/ (Im R2,x) )
assume y in Im (R1 \/ R2),x ; :: thesis: y in (Im R1,x) \/ (Im R2,x)
then [x,y] in R1 \/ R2 by Th9;
then ( [x,y] in R1 or [x,y] in R2 ) by XBOOLE_0:def 3;
then ( y in Im R1,x or y in Im R2,x ) by Th9;
hence y in (Im R1,x) \/ (Im R2,x) by XBOOLE_0:def 3; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Im R1,x) \/ (Im R2,x) or y in Im (R1 \/ R2),x )
assume A1: y in (Im R1,x) \/ (Im R2,x) ; :: thesis: y in Im (R1 \/ R2),x

per cases ( y in Im R1,x or y in Im R2,x ) by A1, XBOOLE_0:def 3;

suppose y in Im R1,x ; :: thesis: y in Im (R1 \/ R2),x

then [x,y] in R1 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def 3;
hence y in Im (R1 \/ R2),x by Th9; :: thesis: verum

end;

suppose y in Im R2,x ; :: thesis: y in Im (R1 \/ R2),x

then [x,y] in R2 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def 3;
hence y in Im (R1 \/ R2),x by Th9; :: thesis: verum

end;

end;