theorem :: SEQFUNC:11

for D being non empty set
for H being Functional_Sequence of D,REAL holds 1 (#) H = H