let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for r being set
for x being Function st r in the carrier of (G . i) & x in product (carr G) holds
x +* (i,r) in the carrier of (product G)
let i be Element of dom G; :: thesis: for r being set
for x being Function st r in the carrier of (G . i) & x in product (carr G) holds
x +* (i,r) in the carrier of (product G)
let r be set ; :: thesis: for x being Function st r in the carrier of (G . i) & x in product (carr G) holds
x +* (i,r) in the carrier of (product G)
let x be Function; :: thesis: ( r in the carrier of (G . i) & x in product (carr G) implies x +* (i,r) in the carrier of (product G) )
assume A1: ( r in the carrier of (G . i) & x in product (carr G) ) ; :: thesis: x +* (i,r) in the carrier of (product G)
then consider g being Function such that
A2: ( x = 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;
set h = x +* (i,r);
set s = i .--> r;
i .--> r = {i} --> r by FUNCOP_1:def 9;
then A3: dom (i .--> r) = {i} ;
A4: dom (x +* (i,r)) = dom (carr G) by A2, FUNCT_7:30;
for j being object st j in dom (carr G) holds
(x +* (i,r)) . j in (carr G) . j

proof

let j be object ; :: thesis: ( j in dom (carr G) implies (x +* (i,r)) . j in (carr G) . j )
assume A5: j in dom (carr G) ; :: thesis: (x +* (i,r)) . j in (carr G) . j

per cases ( not j in dom (i .--> r) or j in dom (i .--> r) ) ;

suppose not j in dom (i .--> r) ; :: thesis: (x +* (i,r)) . j in (carr G) . j

then j <> i by A3, TARSKI:def 1;
then (x +* (i,r)) . j = x . j by FUNCT_7:32;
hence (x +* (i,r)) . j in (carr G) . j by A2, A5; :: thesis: verum

end;

suppose j in dom (i .--> r) ; :: thesis: (x +* (i,r)) . j in (carr G) . j

then A6: j = i by TARSKI:def 1;
then (x +* (i,r)) . j = r by A5, A2, FUNCT_7:31;
hence (x +* (i,r)) . j in (carr G) . j by A1, A6, PRVECT_1:def 11; :: thesis: verum

end;

end;

end;

then x +* (i,r) in product (carr G) by A4, CARD_3:def 5;
hence x +* (i,r) in the carrier of (product G) by Th10; :: thesis: verum