let m be Element of 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:27;
hence 1 <= len (f | m) by FINSEQ_1:80; :: 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

A3: f | 0 = <*> D ;
m = 0 by A2, NAT_1:14;
hence f | m is_sequence_on M by A3, Lm2; :: 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:79; :: thesis: verum

end;

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

A5: dom (f | m) = Seg (len (f | m)) by FINSEQ_1:def 3;
A6: ( m in dom f & len (f | m) = m ) by A4, FINSEQ_1:80, FINSEQ_3:27;

A7: now

let n be Element of NAT ; :: thesis: ( n in dom (f | m) & n + 1 in dom (f | m) implies for i1, i2, j1, j2 being Element of 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
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A8: ( n in dom (f | m) & n + 1 in dom (f | m) ) ; :: thesis: for i1, i2, j1, j2 being Element of 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
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
then A9: ( n in dom f & n + 1 in dom f ) by A5, A6, FINSEQ_4:86;
let i1, i2, j1, j2 be Element of 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 (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A10: ( [i1,i2] in Indices M & [j1,j2] in Indices M & (f | m) /. n = M * i1,i2 & (f | m) /. (n + 1) = M * j1,j2 ) ; :: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
( (f | m) /. n = f /. n & (f | m) /. (n + 1) = f /. (n + 1) ) by A5, A6, A8, FINSEQ_4:86;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A9, A10, Def11; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ( n in dom (f | m) implies ex i, j being Element of NAT st
( [i,j] in Indices M & (f | m) /. n = M * i,j ) )
assume A11: n in dom (f | m) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices M & (f | m) /. n = M * i,j )
then n in dom f by A5, A6, FINSEQ_4:86;
then consider i, j being Element of NAT such that
A12: ( [i,j] in Indices M & f /. n = M * i,j ) by A1, Def11;
take i = i; :: thesis: ex j being Element of 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 A5, A6, A11, A12, FINSEQ_4:86; :: thesis: verum

end;

hence f | m is_sequence_on M by A7, Def11; :: thesis: verum

end;

end;