let a, b, c be Real; <*<*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; verum