defpred S₁[ Nat] means for f being FinSequence of (TOP-REAL 2) st len f = f holds
L~ f is compact ;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: for f being FinSequence of (TOP-REAL 2) st len f = m holds
L~ f is compact ; :: thesis: S₁[m + 1]
let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f = m + 1 implies L~ f is compact )
assume A3: len f = m + 1 ; :: thesis: L~ f is compact
then consider q being FinSequence of (TOP-REAL 2), x being Point of (TOP-REAL 2) such that
A4: f = q ^ <*x*> by FINSEQ_2:19;
len f = (len q) + (len <*x*>) by A4, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
then A5: L~ q is compact by A2, A3;

per cases ( q is empty or not q is empty ) ;

suppose q is empty ; :: thesis: L~ f is compact

then L~ f = L~ <*x*> by A4, FINSEQ_1:34
.= {} (TOP-REAL 2) by SPPOL_2:12 ;
hence L~ f is compact ; :: thesis: verum

end;

suppose not q is empty ; :: thesis: L~ f is compact

then L~ f = ((L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1)))) \/ (L~ <*x*>) by A4, SPPOL_2:23
.= ((L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1)))) \/ {} by SPPOL_2:12
.= (L~ q) \/ (LSeg ((q /. (len q)),(<*x*> /. 1))) ;
hence L~ f is compact by A5, COMPTS_1:10; :: thesis: verum

end;

end;

end;

A6: S₁[ 0 ]

proof

let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f = 0 implies L~ f is compact )
assume len f = 0 ; :: thesis: L~ f is compact
then L~ f = {} (TOP-REAL 2) by TOPREAL1:22;
hence L~ f is compact ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A1);
hence L~ f is compact ; :: thesis: verum