:: deftheorem Def1 defines GoB GOBOARD2:def 1 :
for v1, v2 being FinSequence of REAL st v1 <> {} holds
for b₃ being Matrix of (TOP-REAL 2) holds
( b₃ = GoB (v1,v2) iff ( len b₃ = len v1 & width b₃ = len v2 & ( for n, m being Nat st [n,m] in Indices b₃ holds
b₃ * (n,m) = |[(v1 . n),(v2 . m)]| ) ) );