theorem :: MATRIXR1:10

for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds
F1 = F2