:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :
for F being Field
for A, B being strict VectSp of F
for f being Function of the carrier of A, the carrier of B
for b₅ being Function of the carrier of (lattice A), the carrier of (lattice B) holds
( b₅ = FuncLatt f iff for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b₅ . S = Lin B0 );