let k be Nat; :: thesis: for f, g being FinSequence of () 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 (); :: 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 () by FINSEQ_1:def 4;
k < len g by ;
then k in dom g by ;
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 ;
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 ;
then k + 1 in dom g by ;
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 ;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum
end;
hence g . (k + 1) in (L~ f) ` ; :: thesis: verum