:: Open Mapping Theorem
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: LOPBAN_6:1
theorem Th2: :: LOPBAN_6:2
theorem Th3: :: LOPBAN_6:3
theorem :: LOPBAN_6:4
theorem Th5: :: LOPBAN_6:5
theorem Th6: :: LOPBAN_6:6
theorem :: LOPBAN_6:7
theorem Th8: :: LOPBAN_6:8
theorem Th9: :: LOPBAN_6:9
theorem Th10: :: LOPBAN_6:10
theorem Th11: :: LOPBAN_6:11
theorem Th12: :: LOPBAN_6:12
theorem Th13: :: LOPBAN_6:13
theorem Th14: :: LOPBAN_6:14
theorem Th15: :: LOPBAN_6:15
theorem :: LOPBAN_6:16