let n be Nat; :: thesis: for f being FinSequence of REAL st len f = n holds
f in the carrier of (Euclid n)
let f be FinSequence of REAL ; :: thesis: ( len f = n implies f in the carrier of (Euclid n) )
( f in REAL * & n -tuples_on REAL = { s where s is Element of REAL * : len s = n } ) by FINSEQ_1:def 11, FINSEQ_2:def 4;
hence ( len f = n implies f in the carrier of (Euclid n) ) ; :: thesis: verum