let S be Subset of (TOP-REAL 2); (SpStSeq S) /. 5 = NW-corner S
set g = <*(NW-corner S),(NE-corner S),(SE-corner S)*>;
2 in {1,2}
by TARSKI:def 2;
then A1:
2 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) /. 5 =
(SpStSeq S) /. ((len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + 2)
.=
<*(SW-corner S),(NW-corner S)*> /. 2
by A1, FINSEQ_4:69
.=
NW-corner S
by FINSEQ_4:17
;
verum