begin
Lm1:
for GF being non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for a, b being Element of GF
for v being Element of V holds (a - b) * v = (a * v) - (b * v)
:: deftheorem Def1 defines linearly-closed VECTSP_4:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem
:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm2:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th25:
theorem
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem Th42:
:: deftheorem Def3 defines (0). VECTSP_4:def 3 :
:: deftheorem defines (Omega). VECTSP_4:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th47:
theorem Th48:
theorem
theorem
theorem
theorem
canceled;
theorem
:: deftheorem defines + VECTSP_4:def 5 :
Lm3:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset VECTSP_4:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
Lm4:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for v being Element of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
theorem Th62:
theorem Th63:
theorem
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem
theorem Th75:
theorem
theorem
canceled;
theorem
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th93:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem