consider A being non empty set , a being BinOp of A, Z being Element of A, l being Function of [:the carrier of F,A:],A;
take VectSpStr(# A,a,Z,l #) ; :: thesis: ( not VectSpStr(# A,a,Z,l #) is empty & VectSpStr(# A,a,Z,l #) is strict )
thus not the carrier of VectSpStr(# A,a,Z,l #) is empty ; :: according to STRUCT_0:def 1 :: thesis: VectSpStr(# A,a,Z,l #) is strict
thus VectSpStr(# A,a,Z,l #) is strict ; :: thesis: verum