let k be Nat; :: thesis: for f1, f2 being FinSequence of (TOP-REAL 2) st f1,f2 are_in_general_position holds
for f being FinSequence of (TOP-REAL 2) st f = f2 | (Seg k) holds
f1,f are_in_general_position
let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1,f2 are_in_general_position implies for f being FinSequence of (TOP-REAL 2) st f = f2 | (Seg k) holds
f1,f are_in_general_position )
assume A1: f1,f2 are_in_general_position ; :: thesis: for f being FinSequence of (TOP-REAL 2) st f = f2 | (Seg k) holds
f1,f are_in_general_position
then A2: f1 is_in_general_position_wrt f2 ;
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f = f2 | (Seg k) implies f1,f are_in_general_position )
assume A3: f = f2 | (Seg k) ; :: thesis: f1,f are_in_general_position
A4: f = f2 | k by A3, FINSEQ_1:def 16;
then A5: len f <= len f2 by FINSEQ_5:16;

A6: now :: thesis: for i being Nat st 1 <= i & i < len f holds
(L~ f1) /\ (LSeg (f,i)) is trivial

let i be Nat; :: thesis: ( 1 <= i & i < len f implies (L~ f1) /\ (LSeg (f,i)) is trivial )
assume that
A7: 1 <= i and
A8: i < len f ; :: thesis: (L~ f1) /\ (LSeg (f,i)) is trivial
i in dom (f2 | k) by A4, A7, A8, FINSEQ_3:25;
then A9: f /. i = f2 /. i by A4, FINSEQ_4:70;
A10: i + 1 <= len f by A8, NAT_1:13;
then A11: i + 1 <= len f2 by A5, XXREAL_0:2;
then A12: i < len f2 by NAT_1:13;
1 <= i + 1 by A7, NAT_1:13;
then i + 1 in dom (f2 | k) by A4, A10, FINSEQ_3:25;
then A13: f /. (i + 1) = f2 /. (i + 1) by A4, FINSEQ_4:70;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A7, A10, TOPREAL1:def 3
.= LSeg (f2,i) by A7, A11, A9, A13, TOPREAL1:def 3 ;
hence (L~ f1) /\ (LSeg (f,i)) is trivial by A2, A7, A12; :: thesis: verum

end;

A14: f2 is_in_general_position_wrt f1 by A1;

A15: now :: thesis: for i being Nat st 1 <= i & i < len f1 holds
(L~ f) /\ (LSeg (f1,i)) is trivial

let i be Nat; :: thesis: ( 1 <= i & i < len f1 implies (L~ f) /\ (LSeg (f1,i)) is trivial )
assume ( 1 <= i & i < len f1 ) ; :: thesis: (L~ f) /\ (LSeg (f1,i)) is trivial
then A16: (L~ f2) /\ (LSeg (f1,i)) is trivial by A14;
(L~ f) /\ (LSeg (f1,i)) c= (L~ f2) /\ (LSeg (f1,i)) by A4, TOPREAL3:20, XBOOLE_1:26;
hence (L~ f) /\ (LSeg (f1,i)) is trivial by A16; :: thesis: verum

end;

L~ f2 misses rng f1 by A14;
then L~ f misses rng f1 by A4, TOPREAL3:20, XBOOLE_1:63;
then A17: f is_in_general_position_wrt f1 by A15;
L~ f1 misses rng f2 by A2;
then rng f misses L~ f1 by A3, RELAT_1:70, XBOOLE_1:63;
then f1 is_in_general_position_wrt f by A6;
hence f1,f are_in_general_position by A17; :: thesis: verum