let m be Nat; 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 ; 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; 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; ( ( 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) )
( f is_sequence_on M implies f | m is_sequence_on M )
assume A1:
f is_sequence_on M
; f | m is_sequence_on M
per cases
( m < 1 or m >= len f or ( 1 <= m & m < len f ) )
;
suppose A3:
( 1
<= m &
m < len f )
;
f | m is_sequence_on MA4:
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 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).| = 1let n be
Nat;
( 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) )
;
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).| = 1then A8:
(
n in dom f &
n + 1
in dom f )
by A4, A5, FINSEQ_4:71;
let i1,
i2,
j1,
j2 be
Nat;
( [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) )
;
|.(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;
verum end; now 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;
( 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)
;
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;
ex j being Nat st
( [i,j] in Indices M & (f | m) /. n = M * (i,j) )take j =
j;
( [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;
verum end; hence
f | m is_sequence_on M
by A6;
verum end; end;