theorem :: FINSEQOP:4

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