let X be RealNormSpace-Sequence; :: thesis: for x being Point of (product X) ex d being FinSequence of REAL st
( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) )
let x be Point of (product X); :: thesis: ex d being FinSequence of REAL st
( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) )
defpred S₁[ object , object ] means ex i being Element of dom X st
( $1 = i & $2 = ||.(x . i).|| " );
A4: 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 = ||.(x . i).|| " as Element of REAL by XREAL_0:def 1;
take d ; :: thesis: S₁[n,d]
thus S₁[n,d] ; :: thesis: verum

end;

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

proof

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

end;