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