let m be Nat; :: thesis: for D being set
for f being FinSequence of D
for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let D be set ; :: thesis: for f being FinSequence of D
for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let f be FinSequence of D; :: thesis: for M being Matrix of D holds
( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
let M be Matrix of D; :: thesis: ( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) )
set g = f | m;
thus ( m in dom f implies 1 <= len (f | m) ) :: thesis: ( f is_sequence_on M implies f | m is_sequence_on M )

proof

assume m in dom f ; :: thesis: 1 <= len (f | m)
then ( 1 <= m & m <= len f ) by FINSEQ_3:25;
hence 1 <= len (f | m) by FINSEQ_1:59; :: thesis: verum

end;

assume A1: f is_sequence_on M ; :: thesis: f | m is_sequence_on M

per cases ( m < 1 or m >= len f or ( 1 <= m & m < len f ) ) ;

suppose A2: m < 1 ; :: thesis: f | m is_sequence_on M

m = 0 by A2, NAT_1:14;
hence f | m is_sequence_on M ; :: thesis: verum

end;

suppose m >= len f ; :: thesis: f | m is_sequence_on M

hence f | m is_sequence_on M by A1, FINSEQ_1:58; :: thesis: verum

end;

suppose A3: ( 1 <= m & m < len f ) ; :: thesis: f | m is_sequence_on M

A4: dom (f | m) = Seg (len (f | m)) by FINSEQ_1:def 3;
A5: ( m in dom f & len (f | m) = m ) by A3, FINSEQ_1:59, FINSEQ_3:25;

A6: now :: thesis: for n being Nat st n in dom (f | m) & n + 1 in dom (f | m) holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1

let n be Nat; :: thesis: ( n in dom (f | m) & n + 1 in dom (f | m) implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume A7: ( n in dom (f | m) & n + 1 in dom (f | m) ) ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
then A8: ( n in dom f & n + 1 in dom f ) by A4, A5, FINSEQ_4:71;
let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume A9: ( [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * (i1,i2) & (f | m) /. (n + 1) = M * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
( (f | m) /. n = f /. n & (f | m) /. (n + 1) = f /. (n + 1) ) by A4, A5, A7, FINSEQ_4:71;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A8, A9; :: thesis: verum

end;

now :: thesis: for n being Nat st n in dom (f | m) holds
ex i, j being Nat st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )

let n be Nat; :: thesis: ( n in dom (f | m) implies ex i, j being Nat st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) ) )
assume A10: n in dom (f | m) ; :: thesis: ex i, j being Nat st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
then n in dom f by A4, A5, FINSEQ_4:71;
then consider i, j being Nat such that
A11: ( [i,j] in Indices M & f /. n = M * (i,j) ) by A1;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices M & (f | m) /. n = M * (i,j) )
thus ( [i,j] in Indices M & (f | m) /. n = M * (i,j) ) by A4, A5, A10, A11, FINSEQ_4:71; :: thesis: verum

end;

hence f | m is_sequence_on M by A6; :: thesis: verum

end;

end;