:: deftheorem Def1 defines canMat MATGRP_0:def 1 :
for R being non empty ZeroOneStr
for I, K, i, k being Nat
for b₆ being Matrix of I,K,R holds
( b₆ = canMat (i,k,I,K,R) iff for i2, k2 being Nat st [i2,k2] in Indices b₆ holds
( ( [i,k] = [i2,k2] implies b₆ * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies b₆ * (i2,k2) = 0. R ) ) );