theorem HetHomo: :: RVSUM_3:12

for f being real-valued FinSequence st Het f = 0 holds
f is homogeneous