let G be Go-board; :: thesis: for f, g being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k < len f & f ^ g is_sequence_on G holds
( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )
let f, g be FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st 1 <= k & k < len f & f ^ g is_sequence_on G holds
( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )
let k be Nat; :: thesis: ( 1 <= k & k < len f & f ^ g is_sequence_on G implies ( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) ) )
assume that
A1: 1 <= k and
A2: k < len f and
A3: f ^ g is_sequence_on G ; :: thesis: ( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )
A4: k + 1 <= len f by A2, NAT_1:13;
A5: (f ^ g) | (len f) = f by FINSEQ_5:23;
len f <= (len f) + (len g) by NAT_1:11;
then len f <= len (f ^ g) by FINSEQ_1:22;
then k + 1 <= len (f ^ g) by A4, XXREAL_0:2;
hence ( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) ) by A1, A3, A5, A4, GOBRD13:31; :: thesis: verum