let G be RealNormSpace-Sequence; :: thesis: for p, r being Point of (product G)
for a being Real holds
( a * p = r iff for i being Element of dom G holds r . i = a * (p . i) )
let p, r be Point of (product G); :: thesis: for a being Real holds
( a * p = r iff for i being Element of dom G holds r . i = a * (p . i) )
let a be Real; :: thesis: ( a * p = r iff for i being Element of dom G holds r . i = a * (p . i) )
reconsider p0 = p, r0 = r as Element of product (carr G) by EXTh10;

hereby :: thesis: ( ( for i being Element of dom G holds r . i = a * (p . i) ) implies a * p = r )

assume A1: a * p = r ; :: thesis: for i being Element of dom G holds r . i = a * (p . i)

hereby :: thesis: verum

let i be Element of dom G; :: thesis: r . i = a * (p . i)
reconsider i0 = i as Element of dom (carr G) by LemmaX;
A2: (multop G) . i0 = the Mult of (G . i0) by PRVECT_2:def 8;
reconsider rr = a as Element of REAL by XREAL_0:def 1;
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
hence r . i = rr * (p0 . i) by A1, A2, PRVECT_2:def 2
.= a * (p . i) ;
:: thesis: verum

end;

end;

assume A3: for i being Element of dom G holds r . i = a * (p . i) ; :: thesis: a * p = r
reconsider rp = a * p as Element of product (carr G) by EXTh10;
A4: ex g being Function st
( rp = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
A5: ex g being Function st
( r0 = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;

now :: thesis: for i0 being object st i0 in dom rp holds
rp . i0 = r0 . i0

let i0 be object ; :: thesis: ( i0 in dom rp implies rp . i0 = r0 . i0 )
assume A6: i0 in dom rp ; :: thesis: rp . i0 = r0 . i0
then reconsider i1 = i0 as Element of dom G by A4, LemmaX;
reconsider i = i0 as Element of dom (carr G) by A4, A6;
A7: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
reconsider a = a as Element of REAL by XREAL_0:def 1;
(multop G) . i = the Mult of (G . i) by PRVECT_2:def 8;
then rp . i0 = a * (p0 . i1) by A7, PRVECT_2:def 2;
hence rp . i0 = r0 . i0 by A3; :: thesis: verum

end;

hence a * p = r by A4, A5; :: thesis: verum