theorem :: FINSEQOP:2

for f being Function holds
( [:{},f:] = {} & [:f,{}:] = {} )