let n, j be Element of NAT ; :: thesis: 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))
let F be FinSequence of the carrier of (REAL-US n); :: thesis: 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))
let Bn be Subset of (REAL-US n); :: thesis: 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))
let v0 be Element of (REAL-US n); :: thesis: 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))
let l be Linear_Combination of Bn; :: thesis: ( F is one-to-one & Bn is R-orthogonal & rng F = Carrier l & v0 in Bn & j in dom (l (#) F) & v0 = F . j implies (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) )
assume that
A1: F is one-to-one and
A2: Bn is R-orthogonal and
A3: rng F = Carrier l and
A4: v0 in Bn and
A5: j in dom (l (#) F) and
A6: v0 = F . j ; :: thesis: (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0))
A7: len (l (#) F) = len F by RLVECT_2:def 7;
then A8: dom (l (#) F) = Seg (len F) by FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;
reconsider F2 = l (#) F as FinSequence of the carrier of (REAL-US n) ;
reconsider rv0 = v0 as Element of REAL n by REAL_NS1:def 6;
A9: Carrier l c= Bn by RLVECT_2:def 6;
A10: dom (l (#) F) = Seg (len (l (#) F)) by FINSEQ_1:def 3;
then A11: j <= len F by A5, A7, FINSEQ_1:1;
consider f being sequence of the carrier of (REAL-US n) such that
A12: Sum F2 = f . (len F2) and
A13: f . 0 = 0. (REAL-US n) and
A14: for j2 being Nat
for v being Element of (REAL-US n) st j2 < len F2 & v = F2 . (j2 + 1) holds
f . (j2 + 1) = (f . j2) + v by RLVECT_1:def 12;
defpred S1[ Nat] means ( $1 >= j & $1 <= len F implies (Euclid_scalar n) . (v0,(f . $1)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) );
defpred S2[ Nat] means ( $1 < j implies (Euclid_scalar n) . (v0,(f . $1)) = 0 );
0. (REAL-US n) = 0* n by REAL_NS1:def 6;
then (Euclid_scalar n) . (v0,(f . 0)) = |(rv0,(0* n))| by A13, REAL_NS1:def 5
.= 0 by EUCLID_4:18 ;
then A15: S2[ 0 ] ;
A16: j in Seg (len F) by A5, A7, FINSEQ_1:def 3;
then A17: j <= len F2 by A7, FINSEQ_1:1;
A18: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A19: S2[k] ; :: thesis: S2[k + 1]
now :: thesis: ( ( k < len F2 & S2[k + 1] ) or ( k >= len F2 & S2[k + 1] ) )
per cases ( k < len F2 or k >= len F2 ) ;
case A20: k < len F2 ; :: thesis: verum
A21: 1 <= k + 1 by NAT_1:11;
k + 1 <= len F2 by A20, NAT_1:13;
then k + 1 in Seg (len F2) by A21, FINSEQ_1:1;
then k + 1 in dom F2 by FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (REAL-US n) ;
A22: f . (k + 1) = (f . k) + v by A14, A20;
reconsider rv = v as Element of REAL n by REAL_NS1:def 6;
reconsider fk = f . k as Element of REAL n by REAL_NS1:def 6;
per cases ( k + 1 < j or k + 1 >= j ) ;
suppose A23: k + 1 < j ; :: thesis: S2[k + 1]
A24: 1 <= k + 1 by NAT_1:11;
k + 1 < len F by A11, A23, XXREAL_0:2;
then k + 1 in Seg (len F) by A24, FINSEQ_1:1;
then A25: k + 1 in dom F by FINSEQ_1:def 3;
then A26: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A27: rv0 <> F /. (k + 1) by A1, A5, A6, A8, A23, A25, FUNCT_1:def 4;
reconsider fk1 = F /. (k + 1) as Element of REAL n by REAL_NS1:def 6;
A28: k < k + 1 by XREAL_1:29;
A29: |(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
A30: F /. (k + 1) in rng F by A25, A26, FUNCT_1:def 3;
v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A8, A25, RLVECT_2:def 7;
then |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:22
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A9, A30, A27
.= 0 ;
then |(rv0,(fk + rv))| = 0 by A19, A23, A28, A29, REAL_NS1:def 5, XXREAL_0:2;
hence S2[k + 1] by A22, REAL_NS1:def 5; :: thesis: verum
end;
suppose k + 1 >= j ; :: thesis: S2[k + 1]
hence S2[k + 1] ; :: thesis: verum
end;
end;
end;
end;
end;
hence S2[k + 1] ; :: thesis: verum
end;
A32: for i being Nat holds S2[i] from NAT_1:sch 2(A15, A18);
 A33: for i being Nat st i < j holds
(Euclid_scalar n) . (v0,(f . i)) = 0 by A32;
A34: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A35: S1[k] ; :: thesis: S1[k + 1]
per cases ( k + 1 < j or k + 1 >= j ) ;
suppose k + 1 < j ; :: thesis: S1[k + 1]
hence S1[k + 1] ; :: thesis: verum
end;
suppose A36: k + 1 >= j ; :: thesis: S1[k + 1]
per cases ( k + 1 > j or k + 1 = j ) by A36, XXREAL_0:1;
suppose A37: k + 1 > j ; :: thesis: S1[k + 1]
per cases ( k + 1 <= len F2 or k + 1 > len F2 ) ;
suppose A38: k + 1 <= len F2 ; :: thesis: S1[k + 1]
1 <= k + 1 by NAT_1:11;
then A39: k + 1 in Seg (len F2) by A38, FINSEQ_1:1;
then A40: k + 1 in dom F by A7, FINSEQ_1:def 3;
then A41: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A42: F /. (k + 1) in rng F by A40, FUNCT_1:def 3;
k + 1 in dom F2 by A39, FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (REAL-US n) ;
reconsider fk1 = F /. (k + 1) as Element of REAL n by REAL_NS1:def 6;
reconsider fk = f . k as Element of REAL n by REAL_NS1:def 6;
k < k + 1 by XREAL_1:29;
then A43: k < len F2 by A38, XXREAL_0:2;
then A44: f . (k + 1) = (f . k) + v by A14;
A45: rv0 <> F /. (k + 1) by A1, A5, A6, A8, A37, A40, A41, FUNCT_1:def 4;
reconsider rv = v as Element of REAL n by REAL_NS1:def 6;
v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A8, A40, RLVECT_2:def 7;
then A46: |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:22
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A9, A42, A45
.= 0 ;
|(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
then |(rv0,(fk + rv))| = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A35, A37, A43, A46, NAT_1:13, REAL_NS1:def 5, RLVECT_2:def 7;
hence S1[k + 1] by A44, REAL_NS1:def 5; :: thesis: verum
end;
suppose k + 1 > len F2 ; :: thesis: S1[k + 1]
hence S1[k + 1] by RLVECT_2:def 7; :: thesis: verum
end;
end;
end;
suppose A47: k + 1 = j ; :: thesis: S1[k + 1]
then F2 . (k + 1) in rng F2 by A5, FUNCT_1:def 3;
then reconsider v = F2 . (k + 1) as Element of (REAL-US n) ;
reconsider rv = v as Element of REAL n by REAL_NS1:def 6;
A48: v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A5, A47, RLVECT_2:def 7;
k + 1 in dom F by A5, A10, A7, A47, FINSEQ_1:def 3;
then A49: |(rv0,rv)| = |(rv0,((l . (F /. j)) * rv0))| by A6, A47, A48, PARTFUN1:def 6
.= (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by REAL_NS1:def 5 ;
k < k + 1 by XREAL_1:29;
then k < len F2 by A7, A11, A47, XXREAL_0:2;
then A50: f . (k + 1) = (f . k) + v by A14;
reconsider fk = f . k as Element of REAL n by REAL_NS1:def 6;
(Euclid_scalar n) . (v0,(f . k)) = 0 by A33, A47, XREAL_1:29;
then A51: |(rv0,fk)| = 0 by REAL_NS1:def 5;
|(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:28;
hence S1[k + 1] by A50, A51, A49, REAL_NS1:def 5; :: thesis: verum
end;
end;
end;
end;
end;
A52: S1[ 0 ] by A16, FINSEQ_1:1;
A53: for i being Nat holds S1[i] from NAT_1:sch 2(A52, A34);
 for i being Nat st i >= j & i <= len F holds
(Euclid_scalar n) . (v0,(f . i)) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A53;
hence (Euclid_scalar n) . (v0,(Sum (l (#) F))) = (Euclid_scalar n) . (v0,((l . (F /. j)) * v0)) by A12, A7, A11; :: thesis: verum