theorem Th1: :: FINSEQOP:1

for f being Function holds
( <:{},f:> = {} & <:f,{}:> = {} )