let D be set ; :: thesis: for G being Matrix of D holds <*> D is_sequence_on G
let G be Matrix of D; :: thesis: <*> D is_sequence_on G
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 G & (<*> D) /. n = G * (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 G & [i,j] in Indices G & (<*> D) /. n = G * (m,k) & (<*> D) /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) ; :: according to GOBOARD1:def 9 :: thesis: verum