:: Linear Independence in Left Module over Domain
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines linearly-independent LMOD_5:def 1 :
theorem :: LMOD_5:1
canceled;
theorem :: LMOD_5:2
theorem Th3: :: LMOD_5:3
theorem :: LMOD_5:4
theorem Th5: :: LMOD_5:5
theorem :: LMOD_5:6
theorem Th7: :: LMOD_5:7
theorem Th8: :: LMOD_5:8
:: deftheorem Def2 defines Lin LMOD_5:def 2 :
theorem Th9: :: LMOD_5:9
theorem Th10: :: LMOD_5:10
theorem :: LMOD_5:11
theorem :: LMOD_5:12
theorem Th13: :: LMOD_5:13
theorem :: LMOD_5:14
theorem Th15: :: LMOD_5:15
theorem :: LMOD_5:16
theorem :: LMOD_5:17
theorem :: LMOD_5:18