let f be FinSequence of ; :: thesis: ( f is rectangular implies not f is constant )
assume ex D being non empty compact non horizontal non vertical Subset of st f = SpStSeq D ; :: according to SPRECT_1:def 2 :: thesis: not f is constant
hence not f is constant ; :: thesis: verum