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) )
assume A1: len f = n ; :: thesis: f in the carrier of (Euclid n)
A2: f in REAL * by FINSEQ_1:def 11;
n -tuples_on REAL = { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
hence f in the carrier of (Euclid n) by A1, A2; :: thesis: verum