let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f,g are_in_general_position implies for k being Element of NAT holds (L~ f) /\ (LSeg g,k) is finite )
assume A1: f,g are_in_general_position ; :: thesis: for k being Element of NAT holds (L~ f) /\ (LSeg g,k) is finite
let k be Element of NAT ; :: thesis: (L~ f) /\ (LSeg g,k) is finite
A2: (L~ f) /\ (L~ g) is finite by A1, Th12;
((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:26, XBOOLE_1:28 ;
hence (L~ f) /\ (LSeg g,k) is finite by A2, FINSET_1:15; :: thesis: verum