let X be RealNormSpace-Sequence; :: thesis: for s being Element of (product X) ex F being FinSequence of REAL st
( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(s . i).|| ) )
let s be Element of (product X); :: thesis: ex F being FinSequence of REAL st
( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(s . i).|| ) )
defpred S₁[ object , object ] means ex i being Element of dom X st
( $1 = i & $2 = ||.(s . i).|| );
A5: for n being Nat st n in Seg (len X) holds
ex d being Element of REAL st S₁[n,d]

proof

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

end;

consider F being FinSequence of REAL such that
A6: ( len F = len X & ( for n being Nat st n in Seg (len X) holds
S₁[n,F /. n] ) ) from FINSEQ_4:sch 1(A5);
take F ; :: thesis: ( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(s . i).|| ) )
thus A7: dom F = dom X by A6, FINSEQ_3:29; :: thesis: for i being Element of dom X holds F . i = ||.(s . i).||
thus for i being Element of dom X holds F . i = ||.(s . i).|| :: thesis: verum

proof

let i be Element of dom X; :: thesis: F . i = ||.(s . i).||
i in dom X ;
then A8: i in Seg (len X) by FINSEQ_1:def 3;
reconsider n = i as Nat ;
consider j being Element of dom X such that
A9: ( n = j & F /. n = ||.(s . j).|| ) by A6, A8;
thus F . i = ||.(s . i).|| by A7, A9, PARTFUN1:def 6; :: thesis: verum

end;