let n be Element of 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) )
A1: ( 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;
assume len f = n ; :: thesis: f in the carrier of (Euclid n)
hence f in the carrier of (Euclid n) by A1; :: thesis: verum