let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (G . i)
for a being Real holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
let i be Element of dom G; :: thesis: for x being Point of (G . i)
for a being Real holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
let x be Point of (G . i); :: thesis: for a being Real holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
let a be Real; :: thesis: (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
reconsider a = a as Real ;
reconsider v = (reproj (i,(0. (product G)))) . (a * x) as Element of product (carr G) by Th10;
reconsider s = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by Th10;
for j being Element of dom G holds v . j = a * (s . j)

proof

let j be Element of dom G; :: thesis: v . j = a * (s . j)

per cases ( i = j or i <> j ) ;

suppose A1: i = j ; :: thesis: v . j = a * (s . j)

then v . j = a * x by Th33;
hence v . j = a * (s . j) by Th33, A1; :: thesis: verum

end;

suppose A2: i <> j ; :: thesis: v . j = a * (s . j)

then v . j = 0. (G . j) by Th33;
then v . j = a * (0. (G . j)) by RLVECT_1:10;
hence v . j = a * (s . j) by Th33, A2; :: thesis: verum

end;

end;

end;

hence (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x) by Th13; :: thesis: verum