:: A Theory of Matrices of Real Elements :: by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang :: :: Received February 20, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users
for D1, D2 being set for A being Matrix of D1 for B being Matrix of D2 st A = B holds for i, j being Nat st [i,j]inIndices A holds A * (i,j) = B * (i,j)