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 S1[ 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 S1[n,d]
proof
let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being object st S1[n,d] )
assume n in Seg (len X) ; :: thesis: ex d being object st S1[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: S1[n,d]
thus S1[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
S1[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;