let y be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not y in proj2 <*d,s*> or y in SCM-Data-Loc \/ the carrier of S )

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 \/ the carrier of S

then consider x being object such that

A2: x in dom <*d,s*> and

A3: <*d,s*> . x = y by FUNCT_1:def 3;

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 \/ the carrier of S

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;

end;

suppose
x = 1
; :: thesis: y in SCM-Data-Loc \/ the carrier of S

then
y = d
by A3, FINSEQ_1:44;

hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def 3; :: thesis: verum

end;hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def 3; :: thesis: verum

suppose
x = 2
; :: thesis: y in SCM-Data-Loc \/ the carrier of S

then
y = s
by A3, FINSEQ_1:44;

hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def 3; :: thesis: verum

end;hence y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def 3; :: thesis: verum