let G be non-trivial RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (G . i)
for a being Element of 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 Element of 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 Element of REAL holds (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
let a be Element of REAL ; :: thesis: (reproj (i,(0. (product G)))) . (a * x) = a * ((reproj (i,(0. (product G)))) . x)
reconsider v = (reproj (i,(0. (product G)))) . (a * x) as Element of product (carr G) by LM001;
reconsider s = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by LM001;
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 XLm7;
hence v . j = a * (s . j) by XLm7, A1; :: thesis: verum

end;

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

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

end;

end;

end;

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