:: deftheorem defines LinTrans VECTSP13:def 23 :
for F being Field
for U, V being VectSp of F
for b₄ being strict Subspace of Maps (U,V) holds
( b₄ = LinTrans (U,V) iff the carrier of b₄ = { f where f is linear-transformation of U,V : verum } );