Description: Two expressions for the 1-dimensional subspaces of partial vector space
A. Remark in Crawley p. 120 line 21, but using a non-identity
translation (nonzero vector) F whose trace is P rather than
P itself; F exists by cdlemf . E is the division ring base
by erngdv , and sF is the scalar product by dvavsca . F
must be a non-identity translation for the expression to be a
1-dimensional subspace, although the theorem doesn't require it.
(Contributed by NM, 14-Oct-2013)