let f be FinSequence of REAL ; :: thesis: ( len f = 3 implies f is Element of REAL 3 )
assume A1: len f = 3 ; :: thesis: f is Element of REAL 3
consider x1, x2, x3 being Element of REAL such that
A2: ( f . 1 = x1 & f . 2 = x2 & f . 3 = x3 ) ;
<*x1,x2,x3*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
hence f is Element of REAL 3 by A1, A2, FINSEQ_1:45; :: thesis: verum