for n, j being Element of NAT
for F being FinSequence of the carrier of (REAL-US n)
for Bn being Subset of (REAL-US n)
for v0 being Element of (REAL-US n)
for l being Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j holds
(Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))