let k be Element of 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 by Def2;
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 15;
then A5: len f <= len f2 by FINSEQ_5:18;

A6: now

let i be Element of 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:27;
then A9: f /. i = f2 /. i by A4, FINSEQ_4:85;
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:27;
then A13: f /. (i + 1) = f2 /. (i + 1) by A4, FINSEQ_4:85;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A7, A10, TOPREAL1:def 5
.= LSeg f2,i by A7, A11, A9, A13, TOPREAL1:def 5 ;
hence (L~ f1) /\ (LSeg f,i) is trivial by A2, A7, A12, Def1; :: thesis: verum

end;

A14: f2 is_in_general_position_wrt f1 by A1, Def2;

A15: now

let i be Element of 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, Def1;
(L~ f) /\ (LSeg f1,i) c= (L~ f2) /\ (LSeg f1,i) by A4, TOPREAL3:27, XBOOLE_1:26;
hence (L~ f) /\ (LSeg f1,i) is trivial by A16; :: thesis: verum

end;

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