let k be Element of NAT ; :: thesis: for f, g being FinSequence of (TOP-REAL 2) st 1 <= k & k + 1 <= len g & f,g are_in_general_position holds
( g . k in (L~ f) ` & g . (k + 1) in (L~ f) ` )
let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= k & k + 1 <= len g & f,g are_in_general_position implies ( g . k in (L~ f) ` & g . (k + 1) in (L~ f) ` ) )
assume that
A1: ( 1 <= k & k + 1 <= len g ) and
A2: f,g are_in_general_position ; :: thesis: ( g . k in (L~ f) ` & g . (k + 1) in (L~ f) ` )
f is_in_general_position_wrt g by A2, Def2;
then A3: L~ f misses rng g by Def1;
A4: 1 <= k + 1 by A1, NAT_1:13;
k < len g by A1, NAT_1:13;
then A5: k in dom g by A1, FINSEQ_3:27;
A6: k + 1 in dom g by A1, A4, FINSEQ_3:27;
A7: g . k in rng g by A5, FUNCT_1:12;
A8: rng g c= the carrier of (TOP-REAL 2) by FINSEQ_1:def 4;
A9: g . (k + 1) in rng g by A6, FUNCT_1:12;

now

assume not g . k in (L~ f) ` ; :: thesis: contradiction
then g . k in ((L~ f) ` ) ` by A7, A8, XBOOLE_0:def 5;
hence contradiction by A3, A7, XBOOLE_0:3; :: thesis: verum

end;

hence g . k in (L~ f) ` ; :: thesis: g . (k + 1) in (L~ f) `

now

assume not g . (k + 1) in (L~ f) ` ; :: thesis: contradiction
then g . (k + 1) in ((L~ f) ` ) ` by A8, A9, XBOOLE_0:def 5;
hence contradiction by A3, A9, XBOOLE_0:3; :: thesis: verum

end;

hence g . (k + 1) in (L~ f) ` ; :: thesis: verum