theorem lem5: :: FIELD_12:14

for f being Field-yielding ascending sequence
for i being Element of NAT holds
( 1. (SeqField f) = 1. (f . i) & 0. (SeqField f) = 0. (f . i) )