for k being Nat
for seq being Real_Sequence st seq is V95() holds
seq ^\ k is V95() by SEQM_3:27;