:: deftheorem Def12 defines ProjFinSeq EUCLID_7:def 12 :
for n being Nat
for x0 being Element of REAL n
for b₃ being FinSequence of REAL n holds
( b₃ = ProjFinSeq x0 iff ( len b₃ = n & ( for i being Nat st 1 <= i & i <= n holds
b₃ . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) ) );