let D be non empty set ; :: thesis:
let M be Matrix of D; :: thesis:
let f be FinSequence of D; :: thesis:
let g be non empty FinSequence of D; :: thesis:
assume that
A1: f /. (len f) = g /. 1 and
A2: f is_sequence_on M and
A3: g is_sequence_on M ; :: thesis:
A4: (len (f ^' g)) + 1 = (len f) + (len g) by GRAPH_2:13;
thus for n being Element of NAT st n in dom (f ^' g) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (f ^' g) /. n = M * i,j ) :: according to GOBOARD1:def 11 :: thesis:

proof

let n be Element of NAT ; :: thesis:
assume A5: n in dom (f ^' g) ; :: thesis:

per cases ;

suppose A6: n <= len f ; :: thesis:

A7: 1 <= n by A5, FINSEQ_3:27;
then n in dom f by A6, FINSEQ_3:27;
then consider i, j being Element of NAT such that
A8: [i,j] in Indices M and
A9: f /. n = M * i,j by A2, GOBOARD1:def 11;
take i ; :: thesis:
take j ; :: thesis:
thus [i,j] in Indices M by A8; :: thesis:
thus (f ^' g) /. n = M * i,j by A6, A7, A9, GRAPH_2:61; :: thesis:

end;

suppose A10: n > len f ; :: thesis:

then consider k being Nat such that
A11: n = (len f) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
(len f) + 1 <= n by A10, NAT_1:13;
then A12: 1 <= k by A11, XREAL_1:8;
A13: 1 <= k + 1 by NAT_1:11;
n <= len (f ^' g) by A5, FINSEQ_3:27;
then n < (len f) + (len g) by A4, NAT_1:13;
then A14: k < len g by A11, XREAL_1:8;
then k + 1 <= len g by NAT_1:13;
then k + 1 in dom g by A13, FINSEQ_3:27;
then consider i, j being Element of NAT such that
A15: [i,j] in Indices M and
A16: g /. (k + 1) = M * i,j by A3, GOBOARD1:def 11;
take i ; :: thesis:
take j ; :: thesis:
thus [i,j] in Indices M by A15; :: thesis:
thus (f ^' g) /. n = M * i,j by A11, A12, A14, A16, GRAPH_2:62; :: thesis:

end;

let n be Element of NAT ; :: thesis:
assume that
A17: n in dom (f ^' g) and
A18: n + 1 in dom (f ^' g) ; :: thesis:
let m, k, i, j be Element of NAT ; :: thesis:
assume that
A19: [m,k] in Indices M and
A20: [i,j] in Indices M and
A21: (f ^' g) /. n = M * m,k and
A22: (f ^' g) /. (n + 1) = M * i,j ; :: thesis:

per cases by XXREAL_0:1;

suppose A23: n < len f ; :: thesis:

A24: 1 <= n by A17, FINSEQ_3:27;
then A25: n in dom f by A23, FINSEQ_3:27;
A26: n + 1 <= len f by A23, NAT_1:13;
1 <= n + 1 by NAT_1:11;
then A27: n + 1 in dom f by A26, FINSEQ_3:27;
A28: f /. n = M * m,k by A21, A23, A24, GRAPH_2:61;
f /. (n + 1) = M * i,j by A22, A26, GRAPH_2:61, NAT_1:11;
hence K142((m - i)) + K142((k - j)) = 1 by A2, A19, A20, A25, A27, A28, GOBOARD1:def 11; :: thesis:

end;

suppose A29: n > len f ; :: thesis:

then consider k0 being Nat such that
A30: n = (len f) + k0 by NAT_1:10;
reconsider k0 = k0 as Element of NAT by ORDINAL1:def 13;
(len f) + 1 <= n by A29, NAT_1:13;
then A31: 1 <= k0 by A30, XREAL_1:8;
A32: 1 <= k0 + 1 by NAT_1:11;
n <= len (f ^' g) by A17, FINSEQ_3:27;
then n < (len f) + (len g) by A4, NAT_1:13;
then A33: k0 < len g by A30, XREAL_1:8;
then k0 + 1 <= len g by NAT_1:13;
then A34: k0 + 1 in dom g by A32, FINSEQ_3:27;
A35: 1 <= (k0 + 1) + 1 by NAT_1:11;
n + 1 <= len (f ^' g) by A18, FINSEQ_3:27;
then (len f) + (k0 + 1) < (len f) + (len g) by A4, A30, NAT_1:13;
then A36: k0 + 1 < len g by XREAL_1:8;
then (k0 + 1) + 1 <= len g by NAT_1:13;
then A37: (k0 + 1) + 1 in dom g by A35, FINSEQ_3:27;
A38: g /. (k0 + 1) = M * m,k by A21, A30, A31, A33, GRAPH_2:62;
g /. ((k0 + 1) + 1) = (f ^' g) /. ((len f) + (k0 + 1)) by A36, GRAPH_2:62, NAT_1:11
.= M * i,j by A22, A30 ;
hence K142((m - i)) + K142((k - j)) = 1 by A3, A19, A20, A34, A37, A38, GOBOARD1:def 11; :: thesis:

end;

suppose A39: n = len f ; :: thesis:

1 <= n by A17, FINSEQ_3:27;
then A40: g /. 1 = M * m,k by A1, A21, A39, GRAPH_2:61;
n + 1 <= len (f ^' g) by A18, FINSEQ_3:27;
then (len f) + 1 < (len f) + (len g) by A4, A39, NAT_1:13;
then A41: 1 < len g by XREAL_1:8;
then 1 + 1 <= len g by NAT_1:13;
then A42: 1 + 1 in dom g by FINSEQ_3:27;
A43: 1 in dom g by FINSEQ_5:6;
g /. (1 + 1) = M * i,j by A22, A39, A41, GRAPH_2:62;
hence K142((m - i)) + K142((k - j)) = 1 by A3, A19, A20, A40, A42, A43, GOBOARD1:def 11; :: thesis:

end;