:: deftheorem defmap defines Maps VECTSP13:def 21 :
for X being non empty set
for R being non empty doubleLoopStr
for L being non empty ModuleStr over R
for b₄ being strict ModuleStr over R holds
( b₄ = Maps (X,L) iff ( the carrier of b₄ = Funcs (X, the carrier of L) & the addF of b₄ = mapAdd (X,L) & the ZeroF of b₄ = X --> (0. L) & the lmult of b₄ = mapMult (X,L) ) );