for k being Nat
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).| ) )