let y be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not y in rng <*d,s*> or y in SCM-Data-Loc \/ INT )
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
assume y in rng <*d,s*> ; :: thesis: y in SCM-Data-Loc \/ INT
then consider x being object such that
A2: x in dom <*d,s*> and
A3: <*d,s*> . x = y by FUNCT_1:def 3;

per cases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def 2;

suppose x = 1 ; :: thesis: y in SCM-Data-Loc \/ INT

then y = d by A3;
hence y in SCM-Data-Loc \/ INT by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A4: x = 2 ; :: thesis: y in SCM-Data-Loc \/ INT

A5: s in INT by INT_1:def 2;
y = s by A3, A4;
hence y in SCM-Data-Loc \/ INT by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;