let a, b, c be Real; :: thesis: <*<*a*>,<*b*>,<*c*>*> is Matrix of 3,1,F_Real
rng <*a*> c= REAL ;
then reconsider p = <*a*> as FinSequence of REAL by FINSEQ_1:def 4;
rng <*b*> c= REAL ;
then reconsider q = <*b*> as FinSequence of REAL by FINSEQ_1:def 4;
rng <*c*> c= REAL ;
then reconsider r = <*c*> as FinSequence of REAL by FINSEQ_1:def 4;
( len p = 1 & len q = 1 & len r = 1 ) by FINSEQ_1:40;
hence <*<*a*>,<*b*>,<*c*>*> is Matrix of 3,1,F_Real by MATRIXR2:34; :: thesis: verum