:: RLSUB_1 semantic presentation

definition

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
attr a₂ is lineary-closed means :Def1: :: RLSUB_1:def 1
( ( for b₁, b₂ being VECTOR of a₁ st b₁ in a₂ & b₂ in a₂ holds
b₁ + b₂ in a₂ ) & ( for b₁ being Real
for b₂ being VECTOR of a₁ st b₂ in a₂ holds
b₁ * b₂ in a₂ ) );

end;

:: deftheorem Def1 defines lineary-closed RLSUB_1:def 1 :

theorem Th1: :: RLSUB_1:1

canceled;

theorem Th2: :: RLSUB_1:2

canceled;

theorem Th3: :: RLSUB_1:3

canceled;

theorem Th4: :: RLSUB_1:4

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is lineary-closed holds
0. b₁ in b₂

proof end;

theorem Th5: :: RLSUB_1:5

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ is lineary-closed holds
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
- b₃ in b₂

proof end;

theorem Th6: :: RLSUB_1:6

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ is lineary-closed holds
for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ - b₄ in b₂

proof end;

theorem Th7: :: RLSUB_1:7

for b₁ being RealLinearSpace holds {(0. b₁)} is lineary-closed

proof end;

theorem Th8: :: RLSUB_1:8

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st the carrier of b₁ = b₂ holds
b₂ is lineary-closed

proof end;

theorem Th9: :: RLSUB_1:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is lineary-closed & b₃ is lineary-closed & b₄ = { (b₅ + b₆) where B is VECTOR of b₁, B is VECTOR of b₁ : ( b₅ in b₂ & b₆ in b₃ ) } holds
b₄ is lineary-closed

proof end;

theorem Th10: :: RLSUB_1:10

for b₁ being RealLinearSpace
for b₂, b₃ being Subset of b₁ st b₂ is lineary-closed & b₃ is lineary-closed holds
b₂ /\ b₃ is lineary-closed

proof end;

definition

let c₁ be RealLinearSpace;
mode Subspace of c₁ -> RealLinearSpace means :Def2: :: RLSUB_1:def 2
( the carrier of a₂ c= the carrier of a₁ & the Zero of a₂ = the Zero of a₁ & the add of a₂ = the add of a₁ || the carrier of a₂ & the Mult of a₂ = the Mult of a₁ | [:REAL ,the carrier of a₂:] );
existence

proof end;

end;

:: deftheorem Def2 defines Subspace RLSUB_1:def 2 :

theorem Th11: :: RLSUB_1:11

canceled;

theorem Th12: :: RLSUB_1:12

canceled;

theorem Th13: :: RLSUB_1:13

canceled;

theorem Th14: :: RLSUB_1:14

canceled;

theorem Th15: :: RLSUB_1:15

canceled;

theorem Th16: :: RLSUB_1:16

for b₁ being RealLinearSpace
for b₂ being set
for b₃, b₄ being Subspace of b₁ st b₂ in b₃ & b₃ is Subspace of b₄ holds
b₂ in b₄

proof end;

theorem Th17: :: RLSUB_1:17

for b₁ being RealLinearSpace
for b₂ being set
for b₃ being Subspace of b₁ st b₂ in b₃ holds
b₂ in b₁

proof end;

theorem Th18: :: RLSUB_1:18

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₂ holds b₃ is VECTOR of b₁

proof end;

theorem Th19: :: RLSUB_1:19

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds 0. b₂ = 0. b₁ by Def2;

theorem Th20: :: RLSUB_1:20

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ = 0. b₃

proof end;

theorem Th21: :: RLSUB_1:21

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅, b₆ being VECTOR of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ + b₆ = b₂ + b₃

proof end;

theorem Th22: :: RLSUB_1:22

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁
for b₅ being VECTOR of b₄ st b₅ = b₂ holds
b₃ * b₅ = b₃ * b₂

proof end;

theorem Th23: :: RLSUB_1:23

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being VECTOR of b₃ st b₄ = b₂ holds
- b₂ = - b₄

proof end;

theorem Th24: :: RLSUB_1:24

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅, b₆ being VECTOR of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ - b₆ = b₂ - b₃

proof end;

Lemma13: for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being Subspace of b₁ st the carrier of b₃ = b₂ holds
b₂ is lineary-closed

proof end;

theorem Th25: :: RLSUB_1:25

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds 0. b₁ in b₂

proof end;

theorem Th26: :: RLSUB_1:26

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ in b₃

proof end;

theorem Th27: :: RLSUB_1:27

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds 0. b₂ in b₁

proof end;

theorem Th28: :: RLSUB_1:28

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ + b₃ in b₄

proof end;

theorem Th29: :: RLSUB_1:29

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁ st b₂ in b₄ holds
b₃ * b₂ in b₄

proof end;

theorem Th30: :: RLSUB_1:30

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ st b₂ in b₃ holds
- b₂ in b₃

proof end;

theorem Th31: :: RLSUB_1:31

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ - b₃ in b₄

proof end;

theorem Th32: :: RLSUB_1:32

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being BinOp of b₃
for b₆ being Function of [:REAL ,b₃:],b₃ st b₂ = b₃ & b₄ = 0. b₁ & b₅ = the add of b₁ || b₂ & b₆ = the Mult of b₁ | [:REAL ,b₂:] holds
RLSStruct(# b₃,b₄,b₅,b₆ #) is Subspace of b₁

proof end;

theorem Th33: :: RLSUB_1:33

for b₁ being RealLinearSpace holds b₁ is Subspace of b₁

proof end;

theorem Th34: :: RLSUB_1:34

for b₁, b₂ being strict RealLinearSpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₁ holds
b₁ = b₂

proof end;

theorem Th35: :: RLSUB_1:35

for b₁, b₂, b₃ being RealLinearSpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₃ holds
b₁ is Subspace of b₃

proof end;

theorem Th36: :: RLSUB_1:36

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is Subspace of b₃

proof end;

theorem Th37: :: RLSUB_1:37

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st ( for b₄ being VECTOR of b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ is Subspace of b₃

proof end;

registration

let c₁ be RealLinearSpace;
cluster strict Subspace of a₁;
existence

proof end;

end;

theorem Th38: :: RLSUB_1:38

for b₁ being RealLinearSpace
for b₂, b₃ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₃ holds
b₂ = b₃

proof end;

theorem Th39: :: RLSUB_1:39

for b₁ being RealLinearSpace
for b₂, b₃ being strict Subspace of b₁ st ( for b₄ being VECTOR of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

theorem Th40: :: RLSUB_1:40

for b₁ being strict RealLinearSpace
for b₂ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₁ holds
b₂ = b₁

proof end;

theorem Th41: :: RLSUB_1:41

for b₁ being strict RealLinearSpace
for b₂ being strict Subspace of b₁ st ( for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff b₃ in b₁ ) ) holds
b₂ = b₁

proof end;

theorem Th42: :: RLSUB_1:42

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being Subspace of b₁ st the carrier of b₃ = b₂ holds
b₂ is lineary-closed by Lemma13;

theorem Th43: :: RLSUB_1:43

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is lineary-closed holds
ex b₃ being strict Subspace of b₁ st b₂ = the carrier of b₃

proof end;

definition

let c₁ be RealLinearSpace;
func (0). c₁ -> strict Subspace of a₁ means :Def3: :: RLSUB_1:def 3
the carrier of a₂ = {(0. a₁)};
correctness

proof end;

end;

:: deftheorem Def3 defines (0). RLSUB_1:def 3 :

definition

let c₁ be RealLinearSpace;
func (Omega). c₁ -> strict Subspace of a₁ equals :: RLSUB_1:def 4
RLSStruct(# the carrier of a₁,the Zero of a₁,the add of a₁,the Mult of a₁ #);
coherence

proof end;

end;

:: deftheorem Def4 defines (Omega). RLSUB_1:def 4 :

theorem Th44: :: RLSUB_1:44

canceled;

theorem Th45: :: RLSUB_1:45

canceled;

theorem Th46: :: RLSUB_1:46

canceled;

theorem Th47: :: RLSUB_1:47

canceled;

theorem Th48: :: RLSUB_1:48

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds (0). b₂ = (0). b₁

proof end;

theorem Th49: :: RLSUB_1:49

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ = (0). b₃

proof end;

theorem Th50: :: RLSUB_1:50

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds (0). b₂ is Subspace of b₁ by Th35;

theorem Th51: :: RLSUB_1:51

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds (0). b₁ is Subspace of b₂

proof end;

theorem Th52: :: RLSUB_1:52

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ is Subspace of b₃

proof end;

theorem Th53: :: RLSUB_1:53

canceled;

theorem Th54: :: RLSUB_1:54

for b₁ being strict RealLinearSpace holds b₁ is Subspace of (Omega). b₁ ;

definition

let c₁ be RealLinearSpace;
let c₂ be VECTOR of c₁;
let c₃ be Subspace of c₁;
func c₂ + c₃ -> Subset of a₁ equals :: RLSUB_1:def 5
{ (a₂ + b₁) where B is VECTOR of a₁ : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines + RLSUB_1:def 5 :

Lemma30: for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Subspace of c₁;
mode Coset of c₂ -> Subset of a₁ means :Def6: :: RLSUB_1:def 6
ex b₁ being VECTOR of a₁ st a₃ = b₁ + a₂;
existence

proof end;

end;

:: deftheorem Def6 defines Coset RLSUB_1:def 6 :

theorem Th55: :: RLSUB_1:55

canceled;

theorem Th56: :: RLSUB_1:56

canceled;

theorem Th57: :: RLSUB_1:57

canceled;

theorem Th58: :: RLSUB_1:58

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( 0. b₁ in b₂ + b₃ iff b₂ in b₃ )

proof end;

theorem Th59: :: RLSUB_1:59

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds b₂ in b₂ + b₃

proof end;

theorem Th60: :: RLSUB_1:60

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂ by Lemma30;

theorem Th61: :: RLSUB_1:61

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds b₂ + ((0). b₁) = {b₂}

proof end;

Lemma35: for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff b₂ + b₃ = the carrier of b₃ )

proof end;

theorem Th62: :: RLSUB_1:62

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds b₂ + ((Omega). b₁) = the carrier of b₁

proof end;

theorem Th63: :: RLSUB_1:63

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( 0. b₁ in b₂ + b₃ iff b₂ + b₃ = the carrier of b₃ )

proof end;

theorem Th64: :: RLSUB_1:64

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff b₂ + b₃ = the carrier of b₃ ) by Lemma35;

theorem Th65: :: RLSUB_1:65

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁ st b₂ in b₄ holds
(b₃ * b₂) + b₄ = the carrier of b₄

proof end;

theorem Th66: :: RLSUB_1:66

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁ st b₃ <> 0 & (b₃ * b₂) + b₄ = the carrier of b₄ holds
b₂ in b₄

proof end;

theorem Th67: :: RLSUB_1:67

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff (- b₂) + b₃ = the carrier of b₃ )

proof end;

theorem Th68: :: RLSUB_1:68

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₄ iff b₃ + b₄ = (b₃ + b₂) + b₄ )

proof end;

theorem Th69: :: RLSUB_1:69

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₄ iff b₃ + b₄ = (b₃ - b₂) + b₄ )

proof end;

theorem Th70: :: RLSUB_1:70

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff b₃ + b₄ = b₂ + b₄ )

proof end;

theorem Th71: :: RLSUB_1:71

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ + b₃ = (- b₂) + b₃ iff b₂ in b₃ )

proof end;

theorem Th72: :: RLSUB_1:72

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Subspace of b₁ st b₂ in b₃ + b₅ & b₂ in b₄ + b₅ holds
b₃ + b₅ = b₄ + b₅

proof end;

theorem Th73: :: RLSUB_1:73

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₃ + b₄ & b₂ in (- b₃) + b₄ holds
b₃ in b₄

proof end;

theorem Th74: :: RLSUB_1:74

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁ st b₃ <> 1 & b₃ * b₂ in b₂ + b₄ holds
b₂ in b₄

proof end;

theorem Th75: :: RLSUB_1:75

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Real
for b₄ being Subspace of b₁ st b₂ in b₄ holds
b₃ * b₂ in b₂ + b₄

proof end;

theorem Th76: :: RLSUB_1:76

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( - b₂ in b₂ + b₃ iff b₂ in b₃ )

proof end;

theorem Th77: :: RLSUB_1:77

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ + b₃ in b₃ + b₄ iff b₂ in b₄ )

proof end;

theorem Th78: :: RLSUB_1:78

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ - b₃ in b₂ + b₄ iff b₃ in b₄ )

proof end;

theorem Th79: :: RLSUB_1:79

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ = b₃ + b₅ ) )

proof end;

theorem Th80: :: RLSUB_1:80

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ = b₃ - b₅ ) )

proof end;

theorem Th81: :: RLSUB_1:81

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( ex b₅ being VECTOR of b₁ st
( b₂ in b₅ + b₄ & b₃ in b₅ + b₄ ) iff b₂ - b₃ in b₄ )

proof end;

theorem Th82: :: RLSUB_1:82

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ + b₄ = b₃ + b₄ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ + b₅ = b₃ )

proof end;

theorem Th83: :: RLSUB_1:83

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ + b₄ = b₃ + b₄ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ - b₅ = b₃ )

proof end;

theorem Th84: :: RLSUB_1:84

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being strict Subspace of b₁ holds
( b₂ + b₃ = b₂ + b₄ iff b₃ = b₄ )

proof end;

theorem Th85: :: RLSUB_1:85

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being strict Subspace of b₁ st b₂ + b₄ = b₃ + b₅ holds
b₄ = b₅

proof end;

theorem Th86: :: RLSUB_1:86

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( b₃ is lineary-closed iff b₃ = the carrier of b₂ )

proof end;

theorem Th87: :: RLSUB_1:87

for b₁ being RealLinearSpace
for b₂, b₃ being strict Subspace of b₁
for b₄ being Coset of b₂
for b₅ being Coset of b₃ st b₄ = b₅ holds
b₂ = b₃

proof end;

theorem Th88: :: RLSUB_1:88

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds {b₂} is Coset of (0). b₁

proof end;

theorem Th89: :: RLSUB_1:89

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ is Coset of (0). b₁ holds
ex b₃ being VECTOR of b₁ st b₂ = {b₃}

proof end;

theorem Th90: :: RLSUB_1:90

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁ holds the carrier of b₂ is Coset of b₂

proof end;

theorem Th91: :: RLSUB_1:91

for b₁ being RealLinearSpace holds the carrier of b₁ is Coset of (Omega). b₁

proof end;

theorem Th92: :: RLSUB_1:92

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st b₂ is Coset of (Omega). b₁ holds
b₂ = the carrier of b₁

proof end;

theorem Th93: :: RLSUB_1:93

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( 0. b₁ in b₃ iff b₃ = the carrier of b₂ )

proof end;

theorem Th94: :: RLSUB_1:94

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being Coset of b₃ holds
( b₂ in b₄ iff b₄ = b₂ + b₃ )

proof end;

theorem Th95: :: RLSUB_1:95

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅ being Coset of b₄ st b₂ in b₅ & b₃ in b₅ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₄ & b₂ + b₆ = b₃ )

proof end;

theorem Th96: :: RLSUB_1:96

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅ being Coset of b₄ st b₂ in b₅ & b₃ in b₅ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₄ & b₂ - b₆ = b₃ )

proof end;

theorem Th97: :: RLSUB_1:97

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( ex b₅ being Coset of b₄ st
( b₂ in b₅ & b₃ in b₅ ) iff b₂ - b₃ in b₄ )

proof end;

theorem Th98: :: RLSUB_1:98

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄, b₅ being Coset of b₃ st b₂ in b₄ & b₂ in b₅ holds
b₄ = b₅

proof end;