let G be RealNormSpace-Sequence; :: thesis: for p being Point of (product G)
for r being Real
for r0, p0 being Element of product (carr G) st p = p0 holds
( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )
let p be Point of (product G); :: thesis: for r being Real
for r0, p0 being Element of product (carr G) st p = p0 holds
( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )
let r be Real; :: thesis: for r0, p0 being Element of product (carr G) st p = p0 holds
( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )
let r0, p0 be Element of product (carr G); :: thesis: ( p = p0 implies ( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) ) )
assume A1: p = p0 ; :: thesis: ( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )

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

assume A2: r * p = r0 ; :: thesis: for i being Element of dom G holds r0 . i = r * (p0 . i)

hereby :: thesis: verum

let i be Element of dom G; :: thesis: r0 . i = r * (p0 . i)
reconsider i0 = i as Element of dom (carr G) by Lm1;
A3: (multop G) . i0 = the Mult of (G . i0) by PRVECT_2:def 8;
reconsider rr = r 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 r0 . i = rr * (p0 . i) by A1, A2, A3, PRVECT_2:def 2
.= r * (p0 . i) ;
:: thesis: verum

end;

end;

assume A4: for i being Element of dom G holds r0 . i = r * (p0 . i) ; :: thesis: r * p = r0
reconsider rp = r * p as Element of product (carr G) by Th10;
A5: 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;
A6: 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 A7: i0 in dom rp ; :: thesis: rp . i0 = r0 . i0
then reconsider i1 = i0 as Element of dom G by Lm1, A5;
reconsider i = i0 as Element of dom (carr G) by A7, A5;
A8: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
reconsider r = r 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 = r * (p0 . i1) by A1, A8, PRVECT_2:def 2;
hence rp . i0 = r0 . i0 by A4; :: thesis: verum

end;

hence r * p = r0 by A5, A6, FUNCT_1:2; :: thesis: verum