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_{1}( 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_{1}(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

( 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

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

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