:: Basis of Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines linearly-independent VECTSP_7:def 1 :
theorem :: VECTSP_7:1
canceled;
theorem :: VECTSP_7:2
theorem Th3: :: VECTSP_7:3
theorem :: VECTSP_7:4
canceled;
theorem :: VECTSP_7:5
theorem Th6: :: VECTSP_7:6
theorem :: VECTSP_7:7
canceled;
theorem Th8: :: VECTSP_7:8
theorem :: VECTSP_7:9
:: deftheorem Def2 defines Lin VECTSP_7:def 2 :
theorem :: VECTSP_7:10
canceled;
theorem :: VECTSP_7:11
canceled;
theorem Th12: :: VECTSP_7:12
theorem Th13: :: VECTSP_7:13
theorem :: VECTSP_7:14
theorem :: VECTSP_7:15
theorem Th16: :: VECTSP_7:16
theorem :: VECTSP_7:17
theorem Th18: :: VECTSP_7:18
theorem :: VECTSP_7:19
theorem :: VECTSP_7:20
theorem :: VECTSP_7:21
theorem Th22: :: VECTSP_7:22
theorem Th23: :: VECTSP_7:23
:: deftheorem Def3 defines Basis VECTSP_7:def 3 :
theorem :: VECTSP_7:24
canceled;
theorem :: VECTSP_7:25
canceled;
theorem :: VECTSP_7:26
canceled;
theorem :: VECTSP_7:27
theorem :: VECTSP_7:28