let f be rectangular special_circular_sequence; :: thesis: SpStSeq (L~ f) = f
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
A1: f = SpStSeq D by SPRECT_1:def 2;
A2: 5 = len f by SPRECT_1:82;
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;
then A3: 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 FINSEQ_1:22
.= 3 + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:45
.= 3 + 2 by FINSEQ_1:44 ;
A4: 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 A5: i in dom f ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
then A6: 0 <> i by FINSEQ_3:25;
A7: i <= len f by A5, FINSEQ_3:25;
A8: f /. 1 = W-max (L~ f) by SPRECT_1:83
.= NW-corner D by A1, SPRECT_1:75
.= NW-corner (L~ f) by A1, SPRECT_1:62
.= (SpStSeq (L~ f)) /. 1 by SPRECT_1:35 ;
i <= 5 by A2, A7;
then not not i = 0 & ... & not i = 5 ;
per cases then ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 ) by A6;
suppose i = 1 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = (SpStSeq (L~ f)) /. i by A8; :: thesis: verum
end;
suppose A9: i = 2 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = E-max (L~ f) by SPRECT_1:84
.= NE-corner D by A1, SPRECT_1:79
.= NE-corner (L~ f) by A1, SPRECT_1:63
.= (SpStSeq (L~ f)) /. i by A9, SPRECT_1:36 ;
:: thesis: verum
end;
suppose A10: i = 3 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = E-min (L~ f) by SPRECT_1:85
.= SE-corner D by A1, SPRECT_1:78
.= SE-corner (L~ f) by A1, SPRECT_1:65
.= (SpStSeq (L~ f)) /. i by A10, SPRECT_1:37 ;
:: thesis: verum
end;
suppose A11: i = 4 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = W-min (L~ f) by SPRECT_1:86
.= SW-corner D by A1, SPRECT_1:74
.= SW-corner (L~ f) by A1, SPRECT_1:64
.= (SpStSeq (L~ f)) /. i by A11, SPRECT_1:38 ;
:: thesis: verum
end;
suppose A12: i = 5 ; :: thesis: f /. i = (SpStSeq (L~ f)) /. i
hence f /. i = f /. 1 by A2, FINSEQ_6:def 1
.= (SpStSeq (L~ f)) /. i by A3, A8, A12, FINSEQ_6:def 1 ;
:: thesis: verum
end;
end;
end;
dom f = dom (SpStSeq (L~ f)) by A2, A3, FINSEQ_3:29;
hence SpStSeq (L~ f) = f by A4, FINSEQ_5:12; :: thesis: verum