:: Basic Properties of Functor Structures
:: by Claus Zinn and Wolfgang Jaksch
::
:: Received April 24, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: FUNCTOR1:1
theorem :: FUNCTOR1:2
theorem Th3: :: FUNCTOR1:3
theorem :: FUNCTOR1:4
theorem Th5: :: FUNCTOR1:5
theorem Th6: :: FUNCTOR1:6
theorem Th7: :: FUNCTOR1:7
theorem Th8: :: FUNCTOR1:8
theorem Th9: :: FUNCTOR1:9
theorem Th10: :: FUNCTOR1:10
theorem Th11: :: FUNCTOR1:11
theorem Th12: :: FUNCTOR1:12
theorem Th13: :: FUNCTOR1:13
theorem :: FUNCTOR1:14
theorem :: FUNCTOR1:15
canceled;
theorem :: FUNCTOR1:16
canceled;
theorem :: FUNCTOR1:17
theorem :: FUNCTOR1:18
theorem :: FUNCTOR1:19
theorem :: FUNCTOR1:20
theorem :: FUNCTOR1:21
Lm1:
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
theorem :: FUNCTOR1:22
theorem :: FUNCTOR1:23
theorem :: FUNCTOR1:24