Suggestion: Revising MATRLIN:20

MATRLIN:20 is the theorem

for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for p being FinSequence of V1 st f is linear holds
f . (Sum p) = Sum (f * p)

Actually, the proof doesn't use the assumption that V1 and V2 are finite-dimensional; the same proof proves the statement in which the attribute "finite-dimensional" is dropped. I've confirmed this by running the modified statement and the original proof through the verifier. -- JesseAlama - 15 Apr 2007

Follow up