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
reconsider x1 = f . 1, x2 = f . 2, x3 = f . 3 as Element of REAL by XREAL_0:def 1;
<*x1,x2,x3*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
hence f is Element of REAL 3 by A1, FINSEQ_1:45; :: thesis: verum