let A, B be set ; :: thesis:
let X be Subset of A; :: thesis:
let R1, R2 be Subset of [:A,B:]; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: y in (R1 .:^ X) \/ (R2 .:^ X) ; :: thesis:

per cases by A1, XBOOLE_0:def 3;

suppose A2: y in R1 .:^ X ; :: thesis:

then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A2;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)

proof

let x be set ; :: thesis:
assume x in X ; :: thesis:
then y in Im (R1,x) by A2, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th10; :: thesis:

end;

hence y in (R1 \/ R2) .:^ X by Th25; :: thesis:

end;

suppose A3: y in R2 .:^ X ; :: thesis:

then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A3;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)

proof

let x be set ; :: thesis:
assume x in X ; :: thesis:
then y in Im (R2,x) by A3, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def 3;
hence y in Im ((R1 \/ R2),x) by Th10; :: thesis:

end;

hence y in (R1 \/ R2) .:^ X by Th25; :: thesis:

end;

end;