defpred S₁[ set ] means verum;
deffunc H₁( FinSequence of (TOP-REAL 2), Nat) -> Element of bool the carrier of (TOP-REAL 2) = LSeg ($1,$2);
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } is finite
set Y = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } ;
set X = { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } ;
A1: for e being object holds
( e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } iff e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } )

proof

let e be object ; :: thesis: ( e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } iff e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } )
thus ( e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } implies e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } ) :: thesis: ( e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } implies e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } )

proof

assume e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } ; :: thesis: e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) }
then ex i being Nat st
( e = H₁(f,i) & 1 <= i & i <= len f & S₁[i] ) ;
hence e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } ; :: thesis: verum

end;

assume e in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } ; :: thesis: e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) }
then ex i being Nat st
( e = LSeg (f,i) & 1 <= i & i <= len f ) ;
hence e in { H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } ; :: thesis: verum

end;

{ H₁(f,i) where i is Nat : ( 1 <= i & i <= len f & S₁[i] ) } is finite from SPPOL_1:sch 2();
hence { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } is finite by A1, TARSKI:2; :: thesis: verum