:: Yet another construction of free algebra
:: by Grzegorz Bancerek and Artur Korni{\l}owicz
::
:: Received August 8, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: MSAFREE3:1
canceled;
theorem :: MSAFREE3:2
:: deftheorem MSAFREE3:def 1 :
canceled;
:: deftheorem Def2 defines Free MSAFREE3:def 2 :
theorem Th3: :: MSAFREE3:3
theorem Th4: :: MSAFREE3:4
theorem Th5: :: MSAFREE3:5
theorem Th6: :: MSAFREE3:6
theorem :: MSAFREE3:7
theorem Th8: :: MSAFREE3:8
theorem Th9: :: MSAFREE3:9
:: deftheorem Def3 defines variables_in MSAFREE3:def 3 :
:: deftheorem defines variables_in MSAFREE3:def 4 :
theorem Th10: :: MSAFREE3:10
theorem Th11: :: MSAFREE3:11
theorem Th12: :: MSAFREE3:12
theorem Th13: :: MSAFREE3:13
theorem Th14: :: MSAFREE3:14
theorem Th15: :: MSAFREE3:15
:: deftheorem defines variables_in MSAFREE3:def 5 :
theorem Th16: :: MSAFREE3:16
:: deftheorem Def6 defines -Terms MSAFREE3:def 6 :
theorem Th17: :: MSAFREE3:17
theorem Th18: :: MSAFREE3:18
theorem Th19: :: MSAFREE3:19
theorem Th20: :: MSAFREE3:20
theorem Th21: :: MSAFREE3:21
theorem Th22: :: MSAFREE3:22
theorem Th23: :: MSAFREE3:23
theorem Th24: :: MSAFREE3:24
theorem Th25: :: MSAFREE3:25
theorem :: MSAFREE3:26
theorem Th27: :: MSAFREE3:27
theorem Th28: :: MSAFREE3:28
theorem Th29: :: MSAFREE3:29
theorem Th30: :: MSAFREE3:30
theorem Th31: :: MSAFREE3:31
theorem :: MSAFREE3:32
theorem Th33: :: MSAFREE3:33
theorem Th34: :: MSAFREE3:34
theorem Th35: :: MSAFREE3:35
theorem :: MSAFREE3:36
theorem :: MSAFREE3:37
theorem Th38: :: MSAFREE3:38
theorem Th39: :: MSAFREE3:39
theorem Th40: :: MSAFREE3:40