let D be set ; :: thesis: for M being Matrix of D holds <*> D is_sequence_on M
let M be Matrix of D; :: thesis: <*> D is_sequence_on M
set f = <*> D;
thus ( ( for n being Element of NAT st n in dom (<*> D) holds
ex i, j being Element of NAT st
( [i,j] in Indices M & (<*> D) /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom (<*> D) & n + 1 in dom (<*> D) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (<*> D) /. n = M * (m,k) & (<*> D) /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) ; :: according to GOBOARD1:def 9 :: thesis: verum