let k be Element of NAT ; :: thesis: 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_left k -' 1,G & f2 turns_left k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let D be set ; :: thesis: 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_left k -' 1,G & f2 turns_left k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let f1, f2 be FinSequence of D; :: thesis: 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_left k -' 1,G & f2 turns_left k -' 1,G holds
f1 | (k + 1) = f2 | (k + 1)
let G be Matrix of D; :: thesis: ( 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_left k -' 1,G & f2 turns_left 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_left k -' 1,G and
A7: f2 turns_left k -' 1,G ; :: thesis: 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:80, XXREAL_0:2;
then A10: k in dom (f1 | k) by A1, FINSEQ_3:27;
then A11: f2 /. k = (f2 | k) /. k by A5, FINSEQ_4:85;
k -' 1 <= k by NAT_D:35;
then k -' 1 <= len (f1 | k) by A2, A9, FINSEQ_1:80, XXREAL_0:2;
then A12: k -' 1 in dom (f1 | k) by A8, FINSEQ_3:27;
then A13: f2 /. (k -' 1) = (f2 | k) /. (k -' 1) by A5, FINSEQ_4:85;
A14: f1 /. k = (f1 | k) /. k by A10, FINSEQ_4:85;
A15: f1 /. (k -' 1) = (f1 | k) /. (k -' 1) by A12, FINSEQ_4:85;
A16: k = (k -' 1) + 1 by A1, XREAL_1:237;
then A17: k + 1 = (k -' 1) + (1 + 1) ;
k <= len f1 by A2, A9, XXREAL_0:2;
then consider i1, j1, i2, j2 being Element of NAT such that
A18: ( [i1,j1] in Indices G & f1 /. (k -' 1) = G * i1,j1 & [i2,j2] in Indices G & f1 /. k = G * i2,j2 ) and
A19: ( ( 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:6;
A20: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A21: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

now

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 A19;

suppose A22: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: f1 /. (k + 1) = f2 /. (k + 1)

hence f1 /. (k + 1) = G * (i2 -' 1),j2 by A6, A16, A17, A18, A20, Def7
.= f2 /. (k + 1) by A5, A7, A16, A15, A14, A13, A11, A17, A18, A20, A22, Def7 ;
:: thesis: verum

end;

suppose A23: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: f1 /. (k + 1) = f2 /. (k + 1)

hence f1 /. (k + 1) = G * i2,(j2 + 1) by A6, A16, A17, A18, A21, Def7
.= f2 /. (k + 1) by A5, A7, A16, A15, A14, A13, A11, A17, A18, A21, A23, Def7 ;
:: thesis: verum

end;

suppose A24: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: f1 /. (k + 1) = f2 /. (k + 1)

hence f1 /. (k + 1) = G * i2,(j2 -' 1) by A6, A16, A17, A18, A21, Def7
.= f2 /. (k + 1) by A5, A7, A16, A15, A14, A13, A11, A17, A18, A21, A24, Def7 ;
:: thesis: verum

end;

suppose A25: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: f1 /. (k + 1) = f2 /. (k + 1)

hence f1 /. (k + 1) = G * (i2 + 1),j2 by A6, A16, A17, A18, A20, Def7
.= f2 /. (k + 1) by A5, A7, A16, A15, A14, A13, A11, A17, A18, A20, A25, Def7 ;
:: thesis: verum

end;

end;

end;

hence f1 | (k + 1) = (f2 | k) ^ <*(f2 /. (k + 1))*> by A2, A5, FINSEQ_5:85
.= f2 | (k + 1) by A3, FINSEQ_5:85 ;
:: thesis: verum