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:4, FINSEQ_3:29;
len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3
by FINSEQ_1:62;
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:84
.=
SW-corner S
by FINSEQ_4:26
;
verum