begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
begin
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines ker RANKNULL:def 1 :
theorem Th10:
:: deftheorem Def2 defines im RANKNULL:def 2 :
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
:: deftheorem defines \ RANKNULL:def 3 :
:: deftheorem defines ! RANKNULL:def 4 :
theorem Th24:
Lm1:
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def5 defines @ RANKNULL:def 5 :
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
:: deftheorem Def6 defines # RANKNULL:def 6 :
theorem Th42:
theorem Th43:
begin
:: deftheorem defines rank RANKNULL:def 7 :
:: deftheorem defines nullity RANKNULL:def 8 :
theorem Th44:
theorem