let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f,g are_in_general_position implies for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite )

assume f,g are_in_general_position ; :: thesis: for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite

then A1: (L~ f) /\ (L~ g) is finite by Th11;

let k be Nat; :: thesis: (L~ f) /\ (LSeg (g,k)) is finite

((L~ f) /\ (L~ g)) /\ (LSeg (g,k)) = (L~ f) /\ ((L~ g) /\ (LSeg (g,k))) by XBOOLE_1:16

.= (L~ f) /\ (LSeg (g,k)) by TOPREAL3:19, XBOOLE_1:28 ;

hence (L~ f) /\ (LSeg (g,k)) is finite by A1; :: thesis: verum

assume f,g are_in_general_position ; :: thesis: for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite

then A1: (L~ f) /\ (L~ g) is finite by Th11;

let k be Nat; :: thesis: (L~ f) /\ (LSeg (g,k)) is finite

((L~ f) /\ (L~ g)) /\ (LSeg (g,k)) = (L~ f) /\ ((L~ g) /\ (LSeg (g,k))) by XBOOLE_1:16

.= (L~ f) /\ (LSeg (g,k)) by TOPREAL3:19, XBOOLE_1:28 ;

hence (L~ f) /\ (LSeg (g,k)) is finite by A1; :: thesis: verum