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