theorem :: FINSEQOP:5

for x being set
for F being Function holds F [;] (x,{}) = {}