( 1. (SeqField f) = 1. (f . 0) & 0. (SeqField f) = 0. (f . 0) ) by dsf;
hence not SeqField f is degenerated ; :: thesis: verum