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 9;
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 8;
A10: dom (l (#) F) = Seg (len (l (#) F)) by FINSEQ_1:def 3;
then A11: j <= len F by A5, A7, FINSEQ_1:3;
consider f being Function of NAT ,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 Element of 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 15;
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:23 ;
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:3;
A18: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A19: S2[k] ; :: thesis: S2[k + 1]
now
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:3;
then k + 1 in dom F2 by FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 5;
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:3;
then A25: k + 1 in dom F by FINSEQ_1:def 3;
then A26: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 8;
then A27: rv0 <> F /. (k + 1) by A1, A5, A6, A8, A23, A25, FUNCT_1:def 8;
reconsider fk1 = F /. (k + 1) as Element of REAL n by REAL_NS1:def 6;
A28: k < k + 1 by XREAL_1:31;
A29: |(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:33;
A30: F /. (k + 1) in rng F by A25, A26, FUNCT_1:def 5;
v = (l . (F /. (k + 1))) * (F /. (k + 1)) by A8, A25, RLVECT_2:def 9;
then |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:27
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A9, A30, A27, Def3
.= 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 Element of NAT holds S2[i] from NAT_1:sch 1(A15, A18);
 A33: for i being Nat st i < j holds
(Euclid_scalar n) . v0,(f . i) = 0
proof
let i be Nat; :: thesis: ( i < j implies (Euclid_scalar n) . v0,(f . i) = 0 )
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
assume i < j ; :: thesis: (Euclid_scalar n) . v0,(f . i) = 0
then (Euclid_scalar n) . v0,(f . i0) = 0 by A32;
hence (Euclid_scalar n) . v0,(f . i) = 0 ; :: thesis: verum
end;
A34: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of 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:3;
then A40: k + 1 in dom F by A7, FINSEQ_1:def 3;
then A41: F /. (k + 1) = F . (k + 1) by PARTFUN1:def 8;
then A42: F /. (k + 1) in rng F by A40, FUNCT_1:def 5;
k + 1 in dom F2 by A39, FINSEQ_1:def 3;
then F2 . (k + 1) in rng F2 by FUNCT_1:def 5;
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:31;
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 8;
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 9;
then A46: |(rv0,rv)| = (l . (F /. (k + 1))) * |(rv0,fk1)| by EUCLID_4:27
.= (l . (F /. (k + 1))) * 0 by A2, A3, A4, A9, A42, A45, Def3
.= 0 ;
|(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:33;
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 9;
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 9; :: 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 5;
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 9;
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 8
.= (Euclid_scalar n) . v0,((l . (F /. j)) * v0) by REAL_NS1:def 5 ;
k < k + 1 by XREAL_1:31;
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:31;
then A51: |(rv0,fk)| = 0 by REAL_NS1:def 5;
|(rv0,(fk + rv))| = |(rv0,fk)| + |(rv0,rv)| by EUCLID_4:33;
hence S1[k + 1] by A50, A51, A49, REAL_NS1:def 5; :: thesis: verum
reconsider fk1 = F /. (k + 1) as Element of REAL n by REAL_NS1:def 6;
end;
end;
end;
end;
end;
A52: S1[ 0 ] by A16, FINSEQ_1:3;
A53: for i being Element of NAT holds S1[i] from NAT_1:sch 1(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)
proof
let i be Nat; :: thesis: ( i >= j & i <= len F implies (Euclid_scalar n) . v0,(f . i) = (Euclid_scalar n) . v0,((l . (F /. j)) * v0) )
assume that
A54: i >= j and
A55: i <= len F ; :: thesis: (Euclid_scalar n) . v0,(f . i) = (Euclid_scalar n) . v0,((l . (F /. j)) * v0)
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
(Euclid_scalar n) . v0,(f . i0) = (Euclid_scalar n) . v0,((l . (F /. j)) * v0) by A53, A54, A55;
hence (Euclid_scalar n) . v0,(f . i) = (Euclid_scalar n) . v0,((l . (F /. j)) * v0) ; :: thesis: verum
end;
hence (Euclid_scalar n) . v0,(Sum (l (#) F)) = (Euclid_scalar n) . v0,((l . (F /. j)) * v0) by A12, A7, A11; :: thesis: verum