theorem Th31: :: LOPBAN14:30

for X being RealLinearSpace holds
( len (carr <*X*>) = len <*X*> & len (carr <*X*>) = 1 & carr <*X*> = <* the carrier of X*> )