let k be 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 and
A2: k + 1 <= len g and
A3: 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 A3;
then A4: L~ f misses rng g ;
A5: rng g c= the carrier of (TOP-REAL 2) by FINSEQ_1:def 4;
k < len g by A2, NAT_1:13;
then k in dom g by A1, FINSEQ_3:25;
then A6: g . k in rng g by FUNCT_1:3;
now :: thesis: g . k in (L~ f) `
assume not g . k in (L~ f) ` ; :: thesis: contradiction
then g . k in ((L~ f) `) ` by A6, A5, XBOOLE_0:def 5;
hence contradiction by A4, A6, XBOOLE_0:3; :: thesis: verum
end;
hence g . k in (L~ f) ` ; :: thesis: g . (k + 1) in (L~ f) `
1 <= k + 1 by A1, NAT_1:13;
then k + 1 in dom g by A2, FINSEQ_3:25;
then A7: g . (k + 1) in rng g by FUNCT_1:3;
now :: thesis: g . (k + 1) in (L~ f) `
assume not g . (k + 1) in (L~ f) ` ; :: thesis: contradiction
then g . (k + 1) in ((L~ f) `) ` by A5, A7, XBOOLE_0:def 5;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum
end;
hence g . (k + 1) in (L~ f) ` ; :: thesis: verum