theorem Th83: :: MATGRP_0:71

for n being Nat
for S1, S2 being non empty 1-sorted
for X being Matrix of n,S2
for Y being Matrix of n,S1 holds
( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )