:: RUSUB_3 semantic presentation
:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
theorem Th1: :: RUSUB_3:1
theorem Th2: :: RUSUB_3:2
Lemma4:
for b1 being RealUnitarySpace
for b2 being set holds
( b2 in (0). b1 iff b2 = 0. b1 )
theorem Th3: :: RUSUB_3:3
theorem Th4: :: RUSUB_3:4
theorem Th5: :: RUSUB_3:5
theorem Th6: :: RUSUB_3:6
Lemma6:
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 holds
b2 /\ b3 is Subspace of b4
Lemma7:
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 & b2 is Subspace of b4 holds
b2 is Subspace of b3 /\ b4
Lemma8:
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b3 holds
b2 is Subspace of b3 + b4
Lemma9:
for b1 being RealUnitarySpace
for b2, b3, b4 being Subspace of b1 st b2 is Subspace of b4 & b3 is Subspace of b4 holds
b2 + b3 is Subspace of b4
theorem Th7: :: RUSUB_3:7
theorem Th8: :: RUSUB_3:8
theorem Th9: :: RUSUB_3:9
theorem Th10: :: RUSUB_3:10
theorem Th11: :: RUSUB_3:11
theorem Th12: :: RUSUB_3:12
:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
theorem Th13: :: RUSUB_3:13
theorem Th14: :: RUSUB_3:14
theorem Th15: :: RUSUB_3:15
theorem Th16: :: RUSUB_3:16
theorem Th17: :: RUSUB_3:17
theorem Th18: :: RUSUB_3:18
theorem Th19: :: RUSUB_3:19
theorem Th20: :: RUSUB_3:20
theorem Th21: :: RUSUB_3:21
theorem Th22: :: RUSUB_3:22
theorem Th23: :: RUSUB_3:23
theorem Th24: :: RUSUB_3:24
theorem Th25: :: RUSUB_3:25
Lemma22:
for b1, b2 being set st not b2 in b1 holds
b1 \ {b2} = b1
theorem Th26: :: RUSUB_3:26
theorem Th27: :: RUSUB_3:27
theorem Th28: :: RUSUB_3:28
theorem Th29: :: RUSUB_3:29
theorem Th30: :: RUSUB_3:30
theorem Th31: :: RUSUB_3:31
theorem Th32: :: RUSUB_3:32
theorem Th33: :: RUSUB_3:33
theorem Th34: :: RUSUB_3:34
theorem Th35: :: RUSUB_3:35
theorem Th36: :: RUSUB_3:36
theorem Th37: :: RUSUB_3:37
theorem Th38: :: RUSUB_3:38
theorem Th39: :: RUSUB_3:39
theorem Th40: :: RUSUB_3:40
theorem Th41: :: RUSUB_3:41
theorem Th42: :: RUSUB_3:42
theorem Th43: :: RUSUB_3:43
theorem Th44: :: RUSUB_3:44
theorem Th45: :: RUSUB_3:45