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;
per cases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def 2;
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;
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;
end;