let i1, i2 be Element of 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 i1 <= i2 ; :: thesis: mid f,i1,i2 is_sequence_on M

then A2: mid f,i1,i2 = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1) by JORDAN3:def 1;
f /^ (i1 -' 1) is_sequence_on M by A1, JORDAN8:5;
hence mid f,i1,i2 is_sequence_on M by A2, GOBOARD1:38; :: thesis: verum

end;

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

then A3: mid f,i1,i2 = Rev ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1)) by JORDAN3:def 1;
f /^ (i2 -' 1) is_sequence_on M by A1, JORDAN8:5;
then (f /^ (i2 -' 1)) | ((i1 -' i2) + 1) is_sequence_on M by GOBOARD1:38;
hence mid f,i1,i2 is_sequence_on M by A3, JORDAN9:7; :: thesis: verum

end;

end;