let S be Subset of (TOP-REAL 2); (SpStSeq S) /. 4 = SW-corner S
set g = <*(NW-corner S),(NE-corner S),(SE-corner S)*>;
1 in {1,2}
by TARSKI:def 2;
then A1:
1 in dom <*(SW-corner S),(NW-corner S)*>
by FINSEQ_1:2, FINSEQ_1:89;
len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3
by FINSEQ_1:45;
hence (SpStSeq S) /. 4 =
(SpStSeq S) /. ((len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + 1)
.=
<*(SW-corner S),(NW-corner S)*> /. 1
by A1, FINSEQ_4:69
.=
SW-corner S
by FINSEQ_4:17
;
verum