let i1, i2 be Nat; :: thesis: for f being FinSequence of (TOP-REAL 2)
for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
let f be FinSequence of (TOP-REAL 2); :: thesis: for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
let M be Go-board; :: thesis: ( f is_sequence_on M implies mid (f,i1,i2) is_sequence_on M )
assume A1: f is_sequence_on M ; :: thesis: mid (f,i1,i2) is_sequence_on M

per cases ( i1 <= i2 or i1 > i2 ) ;

suppose A2: i1 <= i2 ; :: thesis: mid (f,i1,i2) is_sequence_on M

A3: f /^ (i1 -' 1) is_sequence_on M by A1, JORDAN8:2;
mid (f,i1,i2) = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1) by A2, FINSEQ_6:def 3;
hence mid (f,i1,i2) is_sequence_on M by A3, GOBOARD1:22; :: thesis: verum

end;

suppose A4: i1 > i2 ; :: thesis: mid (f,i1,i2) is_sequence_on M

f /^ (i2 -' 1) is_sequence_on M by A1, JORDAN8:2;
then A5: (f /^ (i2 -' 1)) | ((i1 -' i2) + 1) is_sequence_on M by GOBOARD1:22;
mid (f,i1,i2) = Rev ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1)) by A4, FINSEQ_6:def 3;
hence mid (f,i1,i2) is_sequence_on M by A5, JORDAN9:5; :: thesis: verum

end;

end;