let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
left_cell f,k,G is closed
let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
left_cell f,k,G is closed
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies left_cell f,k,G is closed )
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G ; :: thesis: left_cell f,k,G is closed
consider i1, j1, i2, j2 being Element of NAT such that
A3: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) and
A4: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) and
A5: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, JORDAN8:6;
( ( i1 = i2 & j1 + 1 = j2 & left_cell f,k,G = cell G,(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,k,G = cell G,i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,k,G = cell G,i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,k,G = cell G,i1,j2 ) ) by A1, A2, A3, A4, A5, GOBRD13:def 3;
hence left_cell f,k,G is closed by GOBRD11:33; :: thesis: verum