let G be Go-board; :: thesis: for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2
let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) implies L~ f1 meets L~ f2 )
assume that
A1: 2 <= len f1 and
A2: 2 <= len f2 and
A3: ( f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) ) ; :: thesis: L~ f1 meets L~ f2
( 1 <= len f1 & 1 <= len f2 ) by A1, A2, XXREAL_0:2;
then rng f1 meets rng f2 by A3, Th1;
then consider x being object such that
A4: x in rng f1 and
A5: x in rng f2 by XBOOLE_0:3;
ex m being Element of NAT st
( m in dom f2 & f2 /. m = x ) by A5, PARTFUN2:2;
then A6: x in L~ f2 by A2, GOBOARD1:1;
ex n being Element of NAT st
( n in dom f1 & f1 /. n = x ) by A4, PARTFUN2:2;
then x in L~ f1 by A1, GOBOARD1:1;
hence L~ f1 meets L~ f2 by A6, XBOOLE_0:3; :: thesis: verum