:: deftheorem Def3 defines + MATRLIN:def 3 :
for K being non empty doubleLoopStr
for V1, V2 being non empty ModuleStr over K
for f1, f2, b₆ being Function of V1,V2 holds
( b₆ = f1 + f2 iff for v being Element of V1 holds b₆ . v = (f1 . v) + (f2 . v) );