let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let v be Element of V; :: thesis: for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let W1, W2 be strict Subspace of V; :: thesis: ( v + W1 = v + W2 iff W1 = W2 )

thus ( v + W1 = v + W2 implies W1 = W2 ) :: thesis: ( W1 = W2 implies v + W1 = v + W2 )

for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let v be Element of V; :: thesis: for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

let W1, W2 be strict Subspace of V; :: thesis: ( v + W1 = v + W2 iff W1 = W2 )

thus ( v + W1 = v + W2 implies W1 = W2 ) :: thesis: ( W1 = W2 implies v + W1 = v + W2 )

proof

thus
( W1 = W2 implies v + W1 = v + W2 )
; :: thesis: verum
assume A1:
v + W1 = v + W2
; :: thesis: W1 = W2

the carrier of W1 = the carrier of W2

end;the carrier of W1 = the carrier of W2

proof

hence
W1 = W2
by Th29; :: thesis: verum
A2:
the carrier of W1 c= the carrier of V
by Def2;

thus the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W2 c= the carrier of W1

assume A6: x in the carrier of W2 ; :: thesis: x in the carrier of W1

the carrier of W2 c= the carrier of V by Def2;

then reconsider y = x as Element of V by A6;

set z = v + y;

x in W2 by A6;

then v + y in v + W1 by A1;

then consider u being Element of V such that

A7: v + y = v + u and

A8: u in W1 ;

y = u by A7, RLVECT_1:8;

hence x in the carrier of W1 by A8; :: thesis: verum

end;thus the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W2 c= the carrier of W1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W2 or x in the carrier of W1 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W1 or x in the carrier of W2 )

assume A3: x in the carrier of W1 ; :: thesis: x in the carrier of W2

then reconsider y = x as Element of V by A2;

set z = v + y;

x in W1 by A3;

then v + y in v + W2 by A1;

then consider u being Element of V such that

A4: v + y = v + u and

A5: u in W2 ;

y = u by A4, RLVECT_1:8;

hence x in the carrier of W2 by A5; :: thesis: verum

end;assume A3: x in the carrier of W1 ; :: thesis: x in the carrier of W2

then reconsider y = x as Element of V by A2;

set z = v + y;

x in W1 by A3;

then v + y in v + W2 by A1;

then consider u being Element of V such that

A4: v + y = v + u and

A5: u in W2 ;

y = u by A4, RLVECT_1:8;

hence x in the carrier of W2 by A5; :: thesis: verum

assume A6: x in the carrier of W2 ; :: thesis: x in the carrier of W1

the carrier of W2 c= the carrier of V by Def2;

then reconsider y = x as Element of V by A6;

set z = v + y;

x in W2 by A6;

then v + y in v + W1 by A1;

then consider u being Element of V such that

A7: v + y = v + u and

A8: u in W1 ;

y = u by A7, RLVECT_1:8;

hence x in the carrier of W1 by A8; :: thesis: verum