theorem Th59: :: HILB10_7:59

(App {}) . {} = {}