theorem :: ZMATRLIN:37

for p, q being FinSequence of INT.Ring
for p1, q1 being FinSequence of F_Real st p = p1 & q = q1 holds
p "*" q = p1 "*" q1