:: Homomorphisms of Order Sorted Algebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem Def1 defines order-sorted OSALG_3:def 1 :
theorem :: OSALG_3:1
canceled;
theorem Th2: :: OSALG_3:2
theorem Th3: :: OSALG_3:3
theorem :: OSALG_3:4
theorem Th5: :: OSALG_3:5
theorem Th6: :: OSALG_3:6
theorem Th7: :: OSALG_3:7
theorem Th8: :: OSALG_3:8
:: deftheorem Def2 defines are_os_isomorphic OSALG_3:def 2 :
theorem Th9: :: OSALG_3:9
theorem Th10: :: OSALG_3:10
theorem :: OSALG_3:11
theorem Th12: :: OSALG_3:12
theorem Th13: :: OSALG_3:13
theorem Th14: :: OSALG_3:14
theorem Th15: :: OSALG_3:15
theorem Th16: :: OSALG_3:16
theorem :: OSALG_3:17
theorem :: OSALG_3:18
theorem :: OSALG_3:19