let X be RealLinearSpace; :: thesis: ( len (carr <*X*>) = len <*X*> & len (carr <*X*>) = 1 & carr <*X*> = <* the carrier of X*> )
thus len (carr <*X*>) = len <*X*> by PRVECT_1:def 11; :: thesis: ( len (carr <*X*>) = 1 & carr <*X*> = <* the carrier of X*> )
hence A1: len (carr <*X*>) = 1 by FINSEQ_1:40; :: thesis: carr <*X*> = <* the carrier of X*>
A2: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
A3: <*X*> . 1 = X ;
1 in {1} by TARSKI:def 1;
then (carr <*X*>) . 1 = the carrier of X by A2, A3, PRVECT_1:def 11;
hence carr <*X*> = <* the carrier of X*> by A1, FINSEQ_1:40; :: thesis: verum