let k be Nat; 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); ( 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
; 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); ( f = f2 | (Seg k) implies f1,f are_in_general_position )
assume A3:
f = f2 | (Seg k)
; 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:16;
A6:
now for i being Nat st 1 <= i & i < len f holds
(L~ f1) /\ (LSeg (f,i)) is trivial let i be
Nat;
( 1 <= i & i < len f implies (L~ f1) /\ (LSeg (f,i)) is trivial )assume that A7:
1
<= i
and A8:
i < len f
;
(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;
verum end;
A14:
f2 is_in_general_position_wrt f1
by A1;
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; verum