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;

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;

( 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) `

hence
g . k in (L~ f) `
; :: thesis: g . (k + 1) 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;then g . k in ((L~ f) `) ` by A6, A5, XBOOLE_0:def 5;

hence contradiction by A4, A6, XBOOLE_0:3; :: thesis: verum

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) `

hence
g . (k + 1) in (L~ f) `
; :: thesis: verumassume
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;then g . (k + 1) in ((L~ f) `) ` by A5, A7, XBOOLE_0:def 5;

hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum