theorem Th3: :: FINSEQOP:3

for F, f being Function holds
( F .: ({},f) = {} & F .: (f,{}) = {} )