theorem Th91: :: CLASSES4:91

for S being Sequence st dom S = NAT holds
( S . NAT = {} & last S = {} )