let f be rectangular special_circular_sequence; :: thesis: SpStSeq (L~ f) = f
A1: SpStSeq (L~ f) = <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*> ^ <*(SW-corner (L~ f)),(NW-corner (L~ f))*> by SPRECT_1:def 1;
set C = L~ f;
set g = SpStSeq (L~ f);
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A2: f = SpStSeq D by SPRECT_1:def 2;
A3: 5 = len f by SPRECT_1:90;
A4: len (SpStSeq (L~ f)) = (len <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*>) + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by A1, FINSEQ_1:35
.= 3 + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:62
.= 3 + 2 by FINSEQ_1:61 ;
then A5: dom f = dom (SpStSeq (L~ f)) by A3, FINSEQ_3:31;
for i being Nat st i in dom f holds
f /. i = (SpStSeq (L~ f)) /. i

proof

let i be Nat; :: thesis: ( i in dom f implies f /. i = (SpStSeq (L~ f)) /. i )
assume i in dom f ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
then A6: ( 0 <> i & i <= len f ) by FINSEQ_3:27;
A7: f /. 1 = W-max (L~ f) by SPRECT_1:91
.= NW-corner D by A2, SPRECT_1:83
.= NW-corner (L~ f) by A2, SPRECT_1:70
.= (SpStSeq (L~ f)) /. 1 by SPRECT_1:37 ;

per cases ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 ) by A3, A6, NAT_1:30;

suppose i = 1 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i

hence f /. i = (SpStSeq (L~ f)) /. i by A7; :: thesis: verum

end;

suppose A8: i = 2 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i

hence f /. i = E-max (L~ f) by SPRECT_1:92
.= NE-corner D by A2, SPRECT_1:87
.= NE-corner (L~ f) by A2, SPRECT_1:71
.= (SpStSeq (L~ f)) /. i by A8, SPRECT_1:38 ;
:: thesis: verum

end;

suppose A9: i = 3 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i

hence f /. i = E-min (L~ f) by SPRECT_1:93
.= SE-corner D by A2, SPRECT_1:86
.= SE-corner (L~ f) by A2, SPRECT_1:73
.= (SpStSeq (L~ f)) /. i by A9, SPRECT_1:39 ;
:: thesis: verum

end;

suppose A10: i = 4 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i

hence f /. i = W-min (L~ f) by SPRECT_1:94
.= SW-corner D by A2, SPRECT_1:82
.= SW-corner (L~ f) by A2, SPRECT_1:72
.= (SpStSeq (L~ f)) /. i by A10, SPRECT_1:40 ;
:: thesis: verum

end;

suppose A11: i = 5 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i

hence f /. i = f /. 1 by A3, FINSEQ_6:def 1
.= (SpStSeq (L~ f)) /. i by A4, A7, A11, FINSEQ_6:def 1 ;
:: thesis: verum

end;

end;

end;

hence f = SpStSeq (L~ f) by A5, FINSEQ_5:13; :: thesis: verum