let k be Nat; for D being set
for f1, f2 being FinSequence of D
for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let D be set ; for f1, f2 being FinSequence of D
for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let f1, f2 be FinSequence of D; for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let G be Matrix of D; ( 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G implies f1 | (k + 1) = f2 | (k + 1) )
assume that
A1:
1 < k
and
A2:
k + 1 <= len f1
and
A3:
k + 1 <= len f2
and
A4:
f1 is_sequence_on G
and
A5:
f1 | k = f2 | k
and
A6:
f1 turns_right k -' 1,G
and
A7:
f2 turns_right k -' 1,G
; f1 | (k + 1) = f2 | (k + 1)
A8:
1 <= k -' 1
by A1, NAT_D:49;
A9:
k <= k + 1
by NAT_1:12;
then
k <= len (f1 | k)
by A2, FINSEQ_1:59, XXREAL_0:2;
then A10:
k in dom (f1 | k)
by A1, FINSEQ_3:25;
then A11:
f2 /. k = (f2 | k) /. k
by A5, FINSEQ_4:70;
k -' 1 <= k
by NAT_D:35;
then
k -' 1 <= len (f1 | k)
by A2, A9, FINSEQ_1:59, XXREAL_0:2;
then A12:
k -' 1 in dom (f1 | k)
by A8, FINSEQ_3:25;
then A13:
f2 /. (k -' 1) = (f2 | k) /. (k -' 1)
by A5, FINSEQ_4:70;
A14:
f1 /. k = (f1 | k) /. k
by A10, FINSEQ_4:70;
A15:
f1 /. (k -' 1) = (f1 | k) /. (k -' 1)
by A12, FINSEQ_4:70;
A16:
k = (k -' 1) + 1
by A1, XREAL_1:235;
k <= len f1
by A2, A9, XXREAL_0:2;
then consider i1, j1, i2, j2 being Nat such that
A17:
( [i1,j1] in Indices G & f1 /. (k -' 1) = G * (i1,j1) & [i2,j2] in Indices G & f1 /. k = G * (i2,j2) )
and
A18:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A4, A8, A16, JORDAN8:3;
A19:
( j1 + 1 > j1 & j2 + 1 > j2 )
by NAT_1:13;
A20:
( i1 + 1 > i1 & i2 + 1 > i2 )
by NAT_1:13;
now f1 /. (k + 1) = f2 /. (k + 1)per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A18;
suppose A21:
(
i1 = i2 &
j1 + 1
= j2 )
;
f1 /. (k + 1) = f2 /. (k + 1)hence f1 /. (k + 1) =
G * (
(i2 + 1),
j2)
by A6, A16, A17, A19
.=
f2 /. (k + 1)
by A5, A7, A16, A15, A14, A13, A11, A17, A19, A21
;
verum end; suppose A22:
(
i1 + 1
= i2 &
j1 = j2 )
;
f1 /. (k + 1) = f2 /. (k + 1)hence f1 /. (k + 1) =
G * (
i2,
(j2 -' 1))
by A6, A16, A17, A20
.=
f2 /. (k + 1)
by A5, A7, A16, A15, A14, A13, A11, A17, A20, A22
;
verum end; suppose A23:
(
i1 = i2 + 1 &
j1 = j2 )
;
f1 /. (k + 1) = f2 /. (k + 1)hence f1 /. (k + 1) =
G * (
i2,
(j2 + 1))
by A6, A16, A17, A20
.=
f2 /. (k + 1)
by A5, A7, A16, A15, A14, A13, A11, A17, A20, A23
;
verum end; suppose A24:
(
i1 = i2 &
j1 = j2 + 1 )
;
f1 /. (k + 1) = f2 /. (k + 1)hence f1 /. (k + 1) =
G * (
(i2 -' 1),
j2)
by A6, A16, A17, A19
.=
f2 /. (k + 1)
by A5, A7, A16, A15, A14, A13, A11, A17, A19, A24
;
verum end; end; end;
hence f1 | (k + 1) =
(f2 | k) ^ <*(f2 /. (k + 1))*>
by A2, A5, FINSEQ_5:82
.=
f2 | (k + 1)
by A3, FINSEQ_5:82
;
verum