let S be Subset of (TOP-REAL 2); :: thesis: (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 ;
:: thesis: verum