let k be Nat; :: thesis: for c being XFinSequence of REAL ex d being XFinSequence of REAL st
( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) )
let c be XFinSequence of REAL ; :: thesis: ex d being XFinSequence of REAL st
( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) )
deffunc H₁( Nat) -> Element of REAL = In (|.(c . $1).|,REAL);
consider d being XFinSequence of REAL such that
A1: ( len d = len c & ( for j being Nat st j in len c holds
d . j = H₁(j) ) ) from AFINSQ_2:sch 1();
take d ; :: thesis: ( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) )
thus len d = len c by A1; :: thesis: for i being Nat st i in dom d holds
d . i = |.(c . i).|
let i be Nat; :: thesis: ( i in dom d implies d . i = |.(c . i).| )
assume i in dom d ; :: thesis: d . i = |.(c . i).|
then d . i = In (|.(c . i).|,REAL) by A1;
hence d . i = |.(c . i).| ; :: thesis: verum