let X be RealNormSpace-Sequence; :: thesis: for s being Point of (product X)
for a being FinSequence of REAL ex s1 being Point of (product X) st
for i being Element of dom X holds s1 . i = (a /. i) * (s . i)
let x be Point of (product X); :: thesis: for a being FinSequence of REAL ex s1 being Point of (product X) st
for i being Element of dom X holds s1 . i = (a /. i) * (x . i)
let a be FinSequence of REAL ; :: thesis: ex s1 being Point of (product X) st
for i being Element of dom X holds s1 . i = (a /. i) * (x . i)
A4: dom (carr X) = dom X by LemmaX;
defpred S₁[ object , object ] means ex i being Element of dom X st
( $1 = i & $2 = (a /. i) * (x . i) );
A5: for n being Nat st n in Seg (len X) holds
ex d being object st S₁[n,d]

proof

let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being object st S₁[n,d] )
assume n in Seg (len X) ; :: thesis: ex d being object st S₁[n,d]
then reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider d = (a /. i) * (x . i) as Element of (X . i) ;
take d ; :: thesis: S₁[n,d]
thus S₁[n,d] ; :: thesis: verum

end;

consider F being FinSequence such that
A6: ( dom F = Seg (len X) & ( for n being Nat st n in Seg (len X) holds
S₁[n,F . n] ) ) from FINSEQ_1:sch 1(A5);
A7: dom F = dom (carr X) by A4, A6, FINSEQ_1:def 3;
for y being object st y in dom (carr X) holds
F . y in (carr X) . y

proof

let y be object ; :: thesis: ( y in dom (carr X) implies F . y in (carr X) . y )
assume A8: y in dom (carr X) ; :: thesis: F . y in (carr X) . y
then reconsider n = y as Nat ;
consider i being Element of dom X such that
A9: ( n = i & F . n = (a /. i) * (x . i) ) by A6, A7, A8;
F . n in the carrier of (X . i) by A9;
hence F . y in (carr X) . y by A9, PRVECT_1:def 11; :: thesis: verum

end;

then reconsider F = F as Element of product (carr X) by A7, CARD_3:def 5;
reconsider F = F as Element of (product X) by EXTh10;
take F ; :: thesis: for i being Element of dom X holds F . i = (a /. i) * (x . i)
thus for i being Element of dom X holds F . i = (a /. i) * (x . i) :: thesis: verum

proof

let i be Element of dom X; :: thesis: F . i = (a /. i) * (x . i)
i in dom X ;
then A10: i in Seg (len X) by FINSEQ_1:def 3;
set n = i;
consider j being Element of dom X such that
A11: ( i = j & F . i = (a /. j) * (x . j) ) by A6, A10;
thus F . i = (a /. i) * (x . i) by A11; :: thesis: verum

end;