:: RLVECT_4 semantic presentation

begin


scheme :: RLVECT_4:sch 1
LambdaSep3{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of F1(), F4() ->  Element of F1(), F5() ->  Element of F1(), F6() ->  Element of F2(), F7() ->  Element of F2(), F8() ->  Element of F2(), F9( set ) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) )
provided
A1: F3() <> F4() and
A2: F3() <> F5() and
A3: F4() <> F5()
proof
defpred S1[ Element of F1(), set ] means ( ( $1 = F3() implies $2 = F6() ) & ( $1 = F4() implies $2 = F7() ) & ( $1 = F5() implies $2 = F8() ) & ( $1 <> F3() & $1 <> F4() & $1 <> F5() implies $2 = F9($1) ) );
A4: for x being Element of F1() ex y being Element of F2() st S1[x,y]
proof
let x be Element of F1(); ::_thesis: ex y being Element of F2() st S1[x,y]
A5: ( x = F4() implies ex y being Element of F2() st S1[x,y] ) by A1, A3;
A6: ( x = F5() implies ex y being Element of F2() st S1[x,y] ) by A2, A3;
 ( x = F3() implies ex y being Element of F2() st S1[x,y] ) by A1, A2;
hence  ex y being Element of F2() st S1[x,y] by A5, A6; ::_thesis: verum
end;
consider f being Function of F1(),F2() such that
A7: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A4);
take  f ; ::_thesis: ( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) )
thus  ( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) ) by A7; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_V_being_RealLinearSpace
for_v_being_VECTOR_of_V
for_a_being_Real_ex_l_being_Linear_Combination_of_{v}_st_l_._v_=_a
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for a being Real ex l being Linear_Combination of {v} st l . v = a
let v be VECTOR of V; ::_thesis: for a being Real ex l being Linear_Combination of {v} st l . v = a
let a be Real; ::_thesis: ex l being Linear_Combination of {v} st l . v = a
thus  ex l being Linear_Combination of {v} st l . v = a ::_thesis: verum
proof
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A1: f . v = a and
A2: for u being VECTOR of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies f . u = 0 )
assume  not u in {v} ; ::_thesis: f . u = 0
then  u <> v by TARSKI:def_1;
hence  f . u = 0 by A2; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume that
A3: x in Carrier f and
A4: not x in {v} ; ::_thesis: contradiction
 ( f . x <> 0 & x <> v ) by A3, A4, RLVECT_2:19, TARSKI:def_1;
hence  contradiction by A2, A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6;
take  f ; ::_thesis: f . v = a
thus  f . v = a by A1; ::_thesis: verum
end;
end;

Lm2: now__::_thesis:_for_V_being_RealLinearSpace
for_v1,_v2_being_VECTOR_of_V
for_a,_b_being_Real_st_v1_<>_v2_holds_
ex_l_being_Linear_Combination_of_{v1,v2}_st_
(_l_._v1_=_a_&_l_._v2_=_b_)
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )
let v1, v2 be VECTOR of V; ::_thesis: for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )
let a, b be Real; ::_thesis: ( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) )
assume A1: v1 <> v2 ; ::_thesis: ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b )
thus  ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) ::_thesis: verum
proof
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A2: ( f . v1 = a & f . v2 = b ) and
A3: for u being VECTOR of V st u <> v1 & u <> v2 holds
f . u = H1(u) from FUNCT_2:sch_7(A1);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v1,v2}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v1,v2} implies f . u = 0 )
assume  not u in {v1,v2} ; ::_thesis: f . u = 0
then  ( u <> v1 & u <> v2 ) by TARSKI:def_2;
hence  f . u = 0 by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v1,v2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2} )
assume that
A4: x in Carrier f and
A5: not x in {v1,v2} ; ::_thesis: contradiction
A6: x <> v2 by A5, TARSKI:def_2;
 ( f . x <> 0 & x <> v1 ) by A4, A5, RLVECT_2:19, TARSKI:def_2;
hence  contradiction by A3, A4, A6; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2} by RLVECT_2:def_6;
take  f ; ::_thesis: ( f . v1 = a & f . v2 = b )
thus  ( f . v1 = a & f . v2 = b ) by A2; ::_thesis: verum
end;
end;

Lm3: now__::_thesis:_for_V_being_RealLinearSpace
for_v1,_v2,_v3_being_VECTOR_of_V
for_a,_b,_c_being_Real_st_v1_<>_v2_&_v1_<>_v3_&_v2_<>_v3_holds_
ex_l_being_Linear_Combination_of_{v1,v2,v3}_st_
(_l_._v1_=_a_&_l_._v2_=_b_&_l_._v3_=_c_)
let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )
let v1, v2, v3 be VECTOR of V; ::_thesis: for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )
let a, b, c be Real; ::_thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c ) )
assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 ; ::_thesis: ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c )
thus  ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c ) ::_thesis: verum
proof
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A4: ( f . v1 = a & f . v2 = b & f . v3 = c ) and
A5: for u being VECTOR of V st u <> v1 & u <> v2 & u <> v3 holds
f . u = H1(u) from RLVECT_4:sch_1(A1, A2, A3);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v1,v2,v3}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v1,v2,v3} implies f . u = 0 )
assume A6: not u in {v1,v2,v3} ; ::_thesis: f . u = 0
then A7: u <> v3 by ENUMSET1:def_1;
 ( u <> v1 & u <> v2 ) by A6, ENUMSET1:def_1;
hence  f . u = 0 by A5, A7; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v1,v2,v3}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} )
assume that
A8: x in Carrier f and
A9: not x in {v1,v2,v3} ; ::_thesis: contradiction
A10: ( x <> v2 & x <> v3 ) by A9, ENUMSET1:def_1;
 ( f . x <> 0 & x <> v1 ) by A8, A9, ENUMSET1:def_1, RLVECT_2:19;
hence  contradiction by A5, A8, A10; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6;
take  f ; ::_thesis: ( f . v1 = a & f . v2 = b & f . v3 = c )
thus  ( f . v1 = a & f . v2 = b & f . v3 = c ) by A4; ::_thesis: verum
end;
end;

theorem :: RLVECT_4:1
for V being RealLinearSpace
for v, w being VECTOR of V holds
( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
proof
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V holds
( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
let v, w be VECTOR of V; ::_thesis: ( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus  (v + w) - v = w by RLSUB_2:61; ::_thesis: ( (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus  (w + v) - v = w by RLSUB_2:61; ::_thesis: ( (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus A1: (v - v) + w = (0. V) + w by RLVECT_1:15
.= w by RLVECT_1:4 ; ::_thesis: ( (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus  (w - v) + v = w by RLSUB_2:61; ::_thesis: ( v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )
thus  ( v + (w - v) = w & w + (v - v) = w & v - (v - w) = w ) by A1, RLSUB_2:61, RLVECT_1:29; ::_thesis: verum
end;

theorem :: RLVECT_4:2
for V being RealLinearSpace
for v1, w, v2 being VECTOR of V st v1 - w = v2 - w holds
v1 = v2
proof
let V be RealLinearSpace; ::_thesis: for v1, w, v2 being VECTOR of V st v1 - w = v2 - w holds
v1 = v2
let v1, w, v2 be VECTOR of V; ::_thesis: ( v1 - w = v2 - w implies v1 = v2 )
assume  v1 - w = v2 - w ; ::_thesis: v1 = v2
then  - (v1 - w) = w - v2 by RLVECT_1:33;
then  w - v1 = w - v2 by RLVECT_1:33;
hence  v1 = v2 by RLVECT_1:23; ::_thesis: verum
end;

theorem Th3: :: RLVECT_4:3
for a being Real
for V being RealLinearSpace
for v being VECTOR of V holds - (a * v) = (- a) * v
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds - (a * v) = (- a) * v
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds - (a * v) = (- a) * v
let v be VECTOR of V; ::_thesis: - (a * v) = (- a) * v
thus  - (a * v) = a * (- v) by RLVECT_1:25
.= (- a) * v by RLVECT_1:24 ; ::_thesis: verum
end;

theorem :: RLVECT_4:4
for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
let v be VECTOR of V; ::_thesis: for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
let W1, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies v + W1 c= v + W2 )
assume A1: W1 is Subspace of W2 ; ::_thesis: v + W1 c= v + W2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W1 or x in v + W2 )
assume  x in v + W1 ; ::_thesis: x in v + W2
then consider u being VECTOR of V such that
A2: u in W1 and
A3: x = v + u by RLSUB_1:63;
 u in W2 by A1, A2, RLSUB_1:8;
hence  x in v + W2 by A3, RLSUB_1:63; ::_thesis: verum
end;

theorem :: RLVECT_4:5
for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in v + W holds
v + W = u + W
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V st u in v + W holds
v + W = u + W
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V st u in v + W holds
v + W = u + W
let W be Subspace of V; ::_thesis: ( u in v + W implies v + W = u + W )
reconsider C = v + W as Coset of W by RLSUB_1:def_6;
assume  u in v + W ; ::_thesis: v + W = u + W
then  C = u + W by RLSUB_1:78;
hence  v + W = u + W ; ::_thesis: verum
end;

theorem Th6: :: RLVECT_4:6
for V being RealLinearSpace
for u, v, w being VECTOR of V
for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being VECTOR of V
for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)
let u, v, w be VECTOR of V; ::_thesis: for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)
let f be Linear_Combination of {u,v,w}; ::_thesis: ( u <> v & u <> w & v <> w implies Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) )
assume that
A1: u <> v and
A2: u <> w and
A3: v <> w ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
set c = f . w;
set b = f . v;
set a = f . u;
A4: Carrier f c= {u,v,w} by RLVECT_2:def_6;
A5: now__::_thesis:_for_x_being_VECTOR_of_V_st_x_<>_v_&_x_<>_u_&_x_<>_w_holds_
f_._x_=_0
let x be VECTOR of V; ::_thesis: ( x <> v & x <> u & x <> w implies f . x = 0 )
assume  ( x <> v & x <> u & x <> w ) ; ::_thesis: f . x = 0
then  not x in Carrier f by A4, ENUMSET1:def_1;
hence  f . x = 0 by RLVECT_2:19; ::_thesis: verum
end;
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . u = 0 or f . u <> 0 ) ;
supposeA6: f . u = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . v = 0 or f . v <> 0 ) ;
supposeA7: f . v = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . w = 0 or f . w <> 0 ) ;
supposeA8: f . w = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_not_Carrier_f_<>_{}
set x = the Element of Carrier f;
assume A9: Carrier f <> {} ; ::_thesis: contradiction
then A10: the Element of Carrier f is VECTOR of V by TARSKI:def_3;
then  f . the Element of Carrier f <> 0 by A9, RLVECT_2:19;
hence  contradiction by A5, A6, A7, A8, A10; ::_thesis: verum
end;
then  f = ZeroLC V by RLVECT_2:def_5;
hence  Sum f = 0. V by RLVECT_2:30
.= (f . u) * u by A6, RLVECT_1:10
.= ((f . u) * u) + (0. V) by RLVECT_1:4
.= ((f . u) * u) + ((f . v) * v) by A7, RLVECT_1:10
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A8, RLVECT_1:10 ;
::_thesis: verum
end;
supposeA11: f . w <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A12: Carrier f c= {w}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w} )
assume that
A13: x in Carrier f and
A14: not x in {w} ; ::_thesis: contradiction
 ( f . x <> 0 & x <> w ) by A13, A14, RLVECT_2:19, TARSKI:def_1;
hence  contradiction by A5, A6, A7, A13; ::_thesis: verum
end;
 w in Carrier f by A11, RLVECT_2:19;
then A15: Carrier f = {w} by A12, ZFMISC_1:33;
set F = <*w*>;
A16: f (#) <*w*> = <*((f . w) * w)*> by RLVECT_2:26;
 ( rng <*w*> = {w} & <*w*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then  Sum f = Sum <*((f . w) * w)*> by A15, A16, RLVECT_2:def_8
.= (f . w) * w by RLVECT_1:44
.= (0. V) + ((f . w) * w) by RLVECT_1:4
.= ((0. V) + (0. V)) + ((f . w) * w) by RLVECT_1:4
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by A6, RLVECT_1:10 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A7, RLVECT_1:10; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
supposeA17: f . v <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . w = 0 or f . w <> 0 ) ;
supposeA18: f . w = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A19: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume that
A20: x in Carrier f and
A21: not x in {v} ; ::_thesis: contradiction
 ( f . x <> 0 & x <> v ) by A20, A21, RLVECT_2:19, TARSKI:def_1;
hence  contradiction by A5, A6, A18, A20; ::_thesis: verum
end;
 v in Carrier f by A17, RLVECT_2:19;
then A22: Carrier f = {v} by A19, ZFMISC_1:33;
set F = <*v*>;
A23: f (#) <*v*> = <*((f . v) * v)*> by RLVECT_2:26;
 ( rng <*v*> = {v} & <*v*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then  Sum f = Sum <*((f . v) * v)*> by A22, A23, RLVECT_2:def_8
.= (f . v) * v by RLVECT_1:44
.= (0. V) + ((f . v) * v) by RLVECT_1:4
.= ((0. V) + ((f . v) * v)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A6, RLVECT_1:10 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A18, RLVECT_1:10; ::_thesis: verum
end;
suppose f . w <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
then A24: w in Carrier f by RLVECT_2:19;
A25: Carrier f c= {v,w}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,w} )
assume that
A26: x in Carrier f and
A27: not x in {v,w} ; ::_thesis: contradiction
A28: x <> w by A27, TARSKI:def_2;
 ( f . x <> 0 & x <> v ) by A26, A27, RLVECT_2:19, TARSKI:def_2;
hence  contradiction by A5, A6, A26, A28; ::_thesis: verum
end;
 v in Carrier f by A17, RLVECT_2:19;
then  {v,w} c= Carrier f by A24, ZFMISC_1:32;
then A29: Carrier f = {v,w} by A25, XBOOLE_0:def_10;
set F = <*v,w*>;
A30: f (#) <*v,w*> = <*((f . v) * v),((f . w) * w)*> by RLVECT_2:27;
 ( rng <*v,w*> = {v,w} & <*v,w*> is one-to-one ) by A3, FINSEQ_2:127, FINSEQ_3:94;
then  Sum f = Sum <*((f . v) * v),((f . w) * w)*> by A29, A30, RLVECT_2:def_8
.= ((f . v) * v) + ((f . w) * w) by RLVECT_1:45
.= ((0. V) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:4 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A6, RLVECT_1:10; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
supposeA31: f . u <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . v = 0 or f . v <> 0 ) ;
supposeA32: f . v = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . w = 0 or f . w <> 0 ) ;
supposeA33: f . w = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A34: Carrier f c= {u}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {u} )
assume that
A35: x in Carrier f and
A36: not x in {u} ; ::_thesis: contradiction
 ( f . x <> 0 & x <> u ) by A35, A36, RLVECT_2:19, TARSKI:def_1;
hence  contradiction by A5, A32, A33, A35; ::_thesis: verum
end;
 u in Carrier f by A31, RLVECT_2:19;
then A37: Carrier f = {u} by A34, ZFMISC_1:33;
set F = <*u*>;
A38: f (#) <*u*> = <*((f . u) * u)*> by RLVECT_2:26;
 ( rng <*u*> = {u} & <*u*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93;
then  Sum f = Sum <*((f . u) * u)*> by A37, A38, RLVECT_2:def_8
.= (f . u) * u by RLVECT_1:44
.= ((f . u) * u) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + (0. V)) + (0. V) by RLVECT_1:4
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by A32, RLVECT_1:10 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A33, RLVECT_1:10; ::_thesis: verum
end;
suppose f . w <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
then A39: w in Carrier f by RLVECT_2:19;
A40: Carrier f c= {u,w}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {u,w} )
assume that
A41: x in Carrier f and
A42: not x in {u,w} ; ::_thesis: contradiction
A43: x <> u by A42, TARSKI:def_2;
 ( f . x <> 0 & x <> w ) by A41, A42, RLVECT_2:19, TARSKI:def_2;
hence  contradiction by A5, A32, A41, A43; ::_thesis: verum
end;
 u in Carrier f by A31, RLVECT_2:19;
then  {u,w} c= Carrier f by A39, ZFMISC_1:32;
then A44: Carrier f = {u,w} by A40, XBOOLE_0:def_10;
set F = <*u,w*>;
A45: f (#) <*u,w*> = <*((f . u) * u),((f . w) * w)*> by RLVECT_2:27;
 ( rng <*u,w*> = {u,w} & <*u,w*> is one-to-one ) by A2, FINSEQ_2:127, FINSEQ_3:94;
then  Sum f = Sum <*((f . u) * u),((f . w) * w)*> by A44, A45, RLVECT_2:def_8
.= ((f . u) * u) + ((f . w) * w) by RLVECT_1:45
.= (((f . u) * u) + (0. V)) + ((f . w) * w) by RLVECT_1:4 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A32, RLVECT_1:10; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
supposeA46: f . v <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
now__::_thesis:_Sum_f_=_(((f_._u)_*_u)_+_((f_._v)_*_v))_+_((f_._w)_*_w)
percases ( f . w = 0 or f . w <> 0 ) ;
supposeA47: f . w = 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
A48: Carrier f c= {u,v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {u,v} )
assume that
A49: x in Carrier f and
A50: not x in {u,v} ; ::_thesis: contradiction
A51: x <> u by A50, TARSKI:def_2;
 ( f . x <> 0 & x <> v ) by A49, A50, RLVECT_2:19, TARSKI:def_2;
hence  contradiction by A5, A47, A49, A51; ::_thesis: verum
end;
 ( v in Carrier f & u in Carrier f ) by A31, A46, RLVECT_2:19;
then  {u,v} c= Carrier f by ZFMISC_1:32;
then A52: Carrier f = {u,v} by A48, XBOOLE_0:def_10;
set F = <*u,v*>;
A53: f (#) <*u,v*> = <*((f . u) * u),((f . v) * v)*> by RLVECT_2:27;
 ( rng <*u,v*> = {u,v} & <*u,v*> is one-to-one ) by A1, FINSEQ_2:127, FINSEQ_3:94;
then  Sum f = Sum <*((f . u) * u),((f . v) * v)*> by A52, A53, RLVECT_2:def_8
.= ((f . u) * u) + ((f . v) * v) by RLVECT_1:45
.= (((f . u) * u) + ((f . v) * v)) + (0. V) by RLVECT_1:4 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by A47, RLVECT_1:10; ::_thesis: verum
end;
supposeA54: f . w <> 0 ; ::_thesis: Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w)
 {u,v,w} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {u,v,w} or x in Carrier f )
assume  x in {u,v,w} ; ::_thesis: x in Carrier f
then  ( x = u or x = v or x = w ) by ENUMSET1:def_1;
hence  x in Carrier f by A31, A46, A54, RLVECT_2:19; ::_thesis: verum
end;
then A55: Carrier f = {u,v,w} by A4, XBOOLE_0:def_10;
set F = <*u,v,w*>;
A56: f (#) <*u,v,w*> = <*((f . u) * u),((f . v) * v),((f . w) * w)*> by RLVECT_2:28;
 ( rng <*u,v,w*> = {u,v,w} & <*u,v,w*> is one-to-one ) by A1, A2, A3, FINSEQ_2:128, FINSEQ_3:95;
then  Sum f = Sum <*((f . u) * u),((f . v) * v),((f . w) * w)*> by A55, A56, RLVECT_2:def_8
.= (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) by RLVECT_1:46 ;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;
end;
end;
hence  Sum f = (((f . u) * u) + ((f . v) * v)) + ((f . w) * w) ; ::_thesis: verum
end;

theorem Th7: :: RLVECT_4:7
for V being RealLinearSpace
for u, v, w being VECTOR of V holds
( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being VECTOR of V holds
( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) )
let u, v, w be VECTOR of V; ::_thesis: ( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) )
thus  ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent implies for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) ::_thesis: ( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) implies ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) )
proof
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
assume that
A1: u <> v and
A2: u <> w and
A3: v <> w and
A4: {u,v,w} is linearly-independent ; ::_thesis: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 )
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * v)) + (c * w) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
consider f being Function of the carrier of V,REAL such that
A5: ( f . u = a & f . v = b & f . w = c ) and
A6: for x being VECTOR of V st x <> u & x <> v & x <> w holds
f . x = H1(x) from RLVECT_4:sch_1(A1, A2, A3);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_x_being_VECTOR_of_V_st_not_x_in_{u,v,w}_holds_
f_._x_=_0
let x be VECTOR of V; ::_thesis: ( not x in {u,v,w} implies f . x = 0 )
assume A7: not x in {u,v,w} ; ::_thesis: f . x = 0
then A8: x <> w by ENUMSET1:def_1;
 ( x <> u & x <> v ) by A7, ENUMSET1:def_1;
hence  f . x = 0 by A6, A8; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {u,v,w}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {u,v,w} )
assume A9: x in Carrier f ; ::_thesis: x in {u,v,w}
then  f . x <> 0 by RLVECT_2:19;
then  ( x = u or x = v or x = w ) by A6, A9;
hence  x in {u,v,w} by ENUMSET1:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {u,v,w} by RLVECT_2:def_6;
assume  ((a * u) + (b * v)) + (c * w) = 0. V ; ::_thesis: ( a = 0 & b = 0 & c = 0 )
then A10: 0. V = Sum f by A1, A2, A3, A5, Th6;
then A11: not u in Carrier f by A4, RLVECT_3:def_1;
 ( not v in Carrier f & not w in Carrier f ) by A4, A10, RLVECT_3:def_1;
hence  ( a = 0 & b = 0 & c = 0 ) by A5, A11, RLVECT_2:19; ::_thesis: verum
end;
assume A12: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; ::_thesis: ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent )
A13: now__::_thesis:_(_not_u_=_v_&_not_u_=_w_&_not_v_=_w_)
assume A14: ( u = v or u = w or v = w ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( u = v or u = w or v = w ) by A14;
suppose u = v ; ::_thesis: contradiction
then ((1 * u) + ((- 1) * v)) + (0 * w) = (u + ((- 1) * u)) + (0 * w) by RLVECT_1:def_8
.= (u + (- u)) + (0 * w) by RLVECT_1:16
.= (u + (- u)) + (0. V) by RLVECT_1:10
.= u + (- u) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence  contradiction by A12; ::_thesis: verum
end;
suppose u = w ; ::_thesis: contradiction
then ((1 * u) + (0 * v)) + ((- 1) * w) = (u + (0 * v)) + ((- 1) * u) by RLVECT_1:def_8
.= (u + (0. V)) + ((- 1) * u) by RLVECT_1:10
.= (u + (0. V)) + (- u) by RLVECT_1:16
.= u + (- u) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence  contradiction by A12; ::_thesis: verum
end;
suppose v = w ; ::_thesis: contradiction
then ((0 * u) + (1 * v)) + ((- 1) * w) = ((0 * u) + (1 * v)) + (- v) by RLVECT_1:16
.= ((0. V) + (1 * v)) + (- v) by RLVECT_1:10
.= ((0. V) + v) + (- v) by RLVECT_1:def_8
.= v + (- v) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence  contradiction by A12; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( u <> v & u <> w & v <> w ) ; ::_thesis: {u,v,w} is linearly-independent
let l be Linear_Combination of {u,v,w}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume  Sum l = 0. V ; ::_thesis: Carrier l = {}
then A15: (((l . u) * u) + ((l . v) * v)) + ((l . w) * w) = 0. V by A13, Th6;
then A16: l . w = 0 by A12;
A17: ( l . u = 0 & l . v = 0 ) by A12, A15;
thus  Carrier l c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= Carrier l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in {} )
assume A18: x in Carrier l ; ::_thesis: x in {}
 Carrier l c= {u,v,w} by RLVECT_2:def_6;
then  ( x = u or x = v or x = w ) by A18, ENUMSET1:def_1;
hence  x in {} by A17, A16, A18, RLVECT_2:19; ::_thesis: verum
end;
thus  {} c= Carrier l by XBOOLE_1:2; ::_thesis: verum
end;

theorem Th8: :: RLVECT_4:8
for x being set
for V being RealLinearSpace
for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )
let v be VECTOR of V; ::_thesis: ( x in Lin {v} iff ex a being Real st x = a * v )
thus  ( x in Lin {v} implies ex a being Real st x = a * v ) ::_thesis: ( ex a being Real st x = a * v implies x in Lin {v} )
proof
assume  x in Lin {v} ; ::_thesis: ex a being Real st x = a * v
then consider l being Linear_Combination of {v} such that
A1: x = Sum l by RLVECT_3:14;
 Sum l = (l . v) * v by RLVECT_2:32;
hence  ex a being Real st x = a * v by A1; ::_thesis: verum
end;
given a being Real such that A2: x = a * v ; ::_thesis: x in Lin {v}
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A3: f . v = a and
A4: for z being VECTOR of V st z <> v holds
f . z = H1(z) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_z_being_VECTOR_of_V_st_not_z_in_{v}_holds_
f_._z_=_0
let z be VECTOR of V; ::_thesis: ( not z in {v} implies f . z = 0 )
assume  not z in {v} ; ::_thesis: f . z = 0
then  z <> v by TARSKI:def_1;
hence  f . z = 0 by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume A5: x in Carrier f ; ::_thesis: x in {v}
then  f . x <> 0 by RLVECT_2:19;
then  x = v by A4, A5;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6;
 Sum f = x by A2, A3, RLVECT_2:32;
hence  x in Lin {v} by RLVECT_3:14; ::_thesis: verum
end;

theorem :: RLVECT_4:9
for V being RealLinearSpace
for v being VECTOR of V holds v in Lin {v}
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds v in Lin {v}
let v be VECTOR of V; ::_thesis: v in Lin {v}
 v in {v} by TARSKI:def_1;
hence  v in Lin {v} by RLVECT_3:15; ::_thesis: verum
end;

theorem :: RLVECT_4:10
for x being set
for V being RealLinearSpace
for v, w being VECTOR of V holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
let v, w be VECTOR of V; ::_thesis: ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
thus  ( x in v + (Lin {w}) implies ex a being Real st x = v + (a * w) ) ::_thesis: ( ex a being Real st x = v + (a * w) implies x in v + (Lin {w}) )
proof
assume  x in v + (Lin {w}) ; ::_thesis: ex a being Real st x = v + (a * w)
then consider u being VECTOR of V such that
A1: u in Lin {w} and
A2: x = v + u by RLSUB_1:63;
 ex a being Real st u = a * w by A1, Th8;
hence  ex a being Real st x = v + (a * w) by A2; ::_thesis: verum
end;
given a being Real such that A3: x = v + (a * w) ; ::_thesis: x in v + (Lin {w})
 a * w in Lin {w} by Th8;
hence  x in v + (Lin {w}) by A3, RLSUB_1:63; ::_thesis: verum
end;

theorem Th11: :: RLVECT_4:11
for x being set
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; ::_thesis: ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
thus  ( x in Lin {w1,w2} implies ex a, b being Real st x = (a * w1) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (a * w1) + (b * w2) implies x in Lin {w1,w2} )
proof
assume A1: x in Lin {w1,w2} ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
now__::_thesis:_ex_a,_b_being_Real_st_x_=_(a_*_w1)_+_(b_*_w2)
percases ( w1 = w2 or w1 <> w2 ) ;
suppose w1 = w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
then  {w1,w2} = {w1} by ENUMSET1:29;
then consider a being Real such that
A2: x = a * w1 by A1, Th8;
x = (a * w1) + (0. V) by A2, RLVECT_1:4
.= (a * w1) + (0 * w2) by RLVECT_1:10 ;
hence  ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
supposeA3: w1 <> w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
consider l being Linear_Combination of {w1,w2} such that
A4: x = Sum l by A1, RLVECT_3:14;
 x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:33;
hence  ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
end;
end;
hence  ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
given a, b being Real such that A5: x = (a * w1) + (b * w2) ; ::_thesis: x in Lin {w1,w2}
now__::_thesis:_x_in_Lin_{w1,w2}
percases ( w1 = w2 or w1 <> w2 ) ;
supposeA6: w1 = w2 ; ::_thesis: x in Lin {w1,w2}
then  x = (a + b) * w1 by A5, RLVECT_1:def_6;
then  x in Lin {w1} by Th8;
hence  x in Lin {w1,w2} by A6, ENUMSET1:29; ::_thesis: verum
end;
supposeA7: w1 <> w2 ; ::_thesis: x in Lin {w1,w2}
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A8: ( f . w1 = a & f . w2 = b ) and
A9: for u being VECTOR of V st u <> w1 & u <> w2 holds
f . u = H1(u) from FUNCT_2:sch_7(A7);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{w1,w2}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {w1,w2} implies f . u = 0 )
assume  not u in {w1,w2} ; ::_thesis: f . u = 0
then  ( u <> w1 & u <> w2 ) by TARSKI:def_2;
hence  f . u = 0 by A9; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {w1,w2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w1,w2} )
assume that
A10: x in Carrier f and
A11: not x in {w1,w2} ; ::_thesis: contradiction
 ( x <> w1 & x <> w2 ) by A11, TARSKI:def_2;
then  f . x = 0 by A9, A10;
hence  contradiction by A10, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def_6;
 x = Sum f by A5, A7, A8, RLVECT_2:33;
hence  x in Lin {w1,w2} by RLVECT_3:14; ::_thesis: verum
end;
end;
end;
hence  x in Lin {w1,w2} ; ::_thesis: verum
end;

theorem :: RLVECT_4:12
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
proof
let V be RealLinearSpace; ::_thesis: for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
let w1, w2 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
 ( w1 in {w1,w2} & w2 in {w1,w2} ) by TARSKI:def_2;
hence  ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) by RLVECT_3:15; ::_thesis: verum
end;

theorem :: RLVECT_4:13
for x being set
for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let V be RealLinearSpace; ::_thesis: for v, w1, w2 being VECTOR of V holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; ::_thesis: ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
thus  ( x in v + (Lin {w1,w2}) implies ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (v + (a * w1)) + (b * w2) implies x in v + (Lin {w1,w2}) )
proof
assume  x in v + (Lin {w1,w2}) ; ::_thesis: ex a, b being Real st x = (v + (a * w1)) + (b * w2)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2} and
A2: x = v + u by RLSUB_1:63;
consider a, b being Real such that
A3: u = (a * w1) + (b * w2) by A1, Th11;
take  a ; ::_thesis: ex b being Real st x = (v + (a * w1)) + (b * w2)
take  b ; ::_thesis: x = (v + (a * w1)) + (b * w2)
thus  x = (v + (a * w1)) + (b * w2) by A2, A3, RLVECT_1:def_3; ::_thesis: verum
end;
given a, b being Real such that A4: x = (v + (a * w1)) + (b * w2) ; ::_thesis: x in v + (Lin {w1,w2})
 (a * w1) + (b * w2) in Lin {w1,w2} by Th11;
then  v + ((a * w1) + (b * w2)) in v + (Lin {w1,w2}) by RLSUB_1:63;
hence  x in v + (Lin {w1,w2}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;

theorem Th14: :: RLVECT_4:14
for x being set
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let v1, v2, v3 be VECTOR of V; ::_thesis: ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
thus  ( x in Lin {v1,v2,v3} implies ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) ::_thesis: ( ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Lin {v1,v2,v3} )
proof
assume A1: x in Lin {v1,v2,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ;
supposeA2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
consider l being Linear_Combination of {v1,v2,v3} such that
A3: x = Sum l by A1, RLVECT_3:14;
 x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, Th6;
hence  ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then A4: ( {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {v3,v3,v1} ) by ENUMSET1:30, ENUMSET1:59;
now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A4, ENUMSET1:30;
suppose {v1,v2,v3} = {v1,v2} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Real such that
A5: x = (a * v1) + (b * v2) by A1, Th11;
x = ((a * v1) + (b * v2)) + (0. V) by A5, RLVECT_1:4
.= ((a * v1) + (b * v2)) + (0 * v3) by RLVECT_1:10 ;
hence  ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
suppose {v1,v2,v3} = {v1,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Real such that
A6: x = (a * v1) + (b * v3) by A1, Th11;
x = ((a * v1) + (0. V)) + (b * v3) by A6, RLVECT_1:4
.= ((a * v1) + (0 * v2)) + (b * v3) by RLVECT_1:10 ;
hence  ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence  ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence  ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
given a, b, c being Real such that A7: x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: x in Lin {v1,v2,v3}
now__::_thesis:_x_in_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ;
supposeA8: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: x in Lin {v1,v2,v3}
now__::_thesis:_x_in_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A8;
suppose v1 = v2 ; ::_thesis: x in Lin {v1,v2,v3}
then  ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A7, ENUMSET1:30, RLVECT_1:def_6;
hence  x in Lin {v1,v2,v3} by Th11; ::_thesis: verum
end;
supposeA9: v1 = v3 ; ::_thesis: x in Lin {v1,v2,v3}
then A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57
.= {v2,v1} by ENUMSET1:30 ;
x = (b * v2) + ((a * v1) + (c * v1)) by A7, A9, RLVECT_1:def_3
.= (b * v2) + ((a + c) * v1) by RLVECT_1:def_6 ;
hence  x in Lin {v1,v2,v3} by A10, Th11; ::_thesis: verum
end;
supposeA11: v2 = v3 ; ::_thesis: x in Lin {v1,v2,v3}
then A12: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
.= {v1,v2} by ENUMSET1:30 ;
x = (a * v1) + ((b * v2) + (c * v2)) by A7, A11, RLVECT_1:def_3
.= (a * v1) + ((b + c) * v2) by RLVECT_1:def_6 ;
hence  x in Lin {v1,v2,v3} by A12, Th11; ::_thesis: verum
end;
end;
end;
hence  x in Lin {v1,v2,v3} ; ::_thesis: verum
end;
supposeA13: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: x in Lin {v1,v2,v3}
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
A14: v1 <> v3 by A13;
A15: v2 <> v3 by A13;
A16: v1 <> v2 by A13;
consider f being Function of the carrier of V,REAL such that
A17: ( f . v1 = a & f . v2 = b & f . v3 = c ) and
A18: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds
f . v = H1(v) from RLVECT_4:sch_1(A16, A14, A15);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2,v3}_holds_
f_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in {v1,v2,v3} implies f . v = 0 )
assume A19: not v in {v1,v2,v3} ; ::_thesis: f . v = 0
then A20: v <> v3 by ENUMSET1:def_1;
 ( v <> v1 & v <> v2 ) by A19, ENUMSET1:def_1;
hence  f . v = 0 by A18, A20; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= {v1,v2,v3}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} )
assume that
A21: x in Carrier f and
A22: not x in {v1,v2,v3} ; ::_thesis: contradiction
A23: x <> v3 by A22, ENUMSET1:def_1;
 ( x <> v1 & x <> v2 ) by A22, ENUMSET1:def_1;
then  f . x = 0 by A18, A21, A23;
hence  contradiction by A21, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6;
 x = Sum f by A7, A13, A17, Th6;
hence  x in Lin {v1,v2,v3} by RLVECT_3:14; ::_thesis: verum
end;
end;
end;
hence  x in Lin {v1,v2,v3} ; ::_thesis: verum
end;

theorem :: RLVECT_4:15
for V being RealLinearSpace
for w1, w2, w3 being VECTOR of V holds
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
proof
let V be RealLinearSpace; ::_thesis: for w1, w2, w3 being VECTOR of V holds
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
let w1, w2, w3 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
A1: w3 in {w1,w2,w3} by ENUMSET1:def_1;
 ( w1 in {w1,w2,w3} & w2 in {w1,w2,w3} ) by ENUMSET1:def_1;
hence  ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) by A1, RLVECT_3:15; ::_thesis: verum
end;

theorem :: RLVECT_4:16
for x being set
for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let V be RealLinearSpace; ::_thesis: for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let v, w1, w2, w3 be VECTOR of V; ::_thesis: ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
thus  ( x in v + (Lin {w1,w2,w3}) implies ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) ::_thesis: ( ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Lin {w1,w2,w3}) )
proof
assume  x in v + (Lin {w1,w2,w3}) ; ::_thesis: ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2,w3} and
A2: x = v + u by RLSUB_1:63;
consider a, b, c being Real such that
A3: u = ((a * w1) + (b * w2)) + (c * w3) by A1, Th14;
take  a ; ::_thesis: ex b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take  b ; ::_thesis: ex c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take  c ; ::_thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3)
 x = (v + ((a * w1) + (b * w2))) + (c * w3) by A2, A3, RLVECT_1:def_3;
hence  x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def_3; ::_thesis: verum
end;
given a, b, c being Real such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; ::_thesis: x in v + (Lin {w1,w2,w3})
 ((a * w1) + (b * w2)) + (c * w3) in Lin {w1,w2,w3} by Th14;
then  v + (((a * w1) + (b * w2)) + (c * w3)) in v + (Lin {w1,w2,w3}) by RLSUB_1:63;
then  (v + ((a * w1) + (b * w2))) + (c * w3) in v + (Lin {w1,w2,w3}) by RLVECT_1:def_3;
hence  x in v + (Lin {w1,w2,w3}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;

theorem :: RLVECT_4:17
for V being RealLinearSpace
for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(v - u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(v - u)} is linearly-independent
let u, v be VECTOR of V; ::_thesis: ( {u,v} is linearly-independent & u <> v implies {u,(v - u)} is linearly-independent )
assume A1: ( {u,v} is linearly-independent & u <> v ) ; ::_thesis: {u,(v - u)} is linearly-independent
now__::_thesis:_for_a,_b_being_Real_st_(a_*_u)_+_(b_*_(v_-_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_)
let a, b be Real; ::_thesis: ( (a * u) + (b * (v - u)) = 0. V implies ( a = 0 & b = 0 ) )
assume  (a * u) + (b * (v - u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 )
then A2: 0. V = (a * u) + ((b * v) - (b * u)) by RLVECT_1:34
.= ((a * u) + (b * v)) - (b * u) by RLVECT_1:def_3
.= ((a * u) - (b * u)) + (b * v) by RLVECT_1:def_3
.= ((a - b) * u) + (b * v) by RLVECT_1:35 ;
then  a - b = 0 by A1, RLVECT_3:13;
hence  ( a = 0 & b = 0 ) by A1, A2, RLVECT_3:13; ::_thesis: verum
end;
hence  {u,(v - u)} is linearly-independent by RLVECT_3:13; ::_thesis: verum
end;

theorem :: RLVECT_4:18
for V being RealLinearSpace
for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(v + u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(v + u)} is linearly-independent
let u, v be VECTOR of V; ::_thesis: ( {u,v} is linearly-independent & u <> v implies {u,(v + u)} is linearly-independent )
assume A1: ( {u,v} is linearly-independent & u <> v ) ; ::_thesis: {u,(v + u)} is linearly-independent
now__::_thesis:_for_a,_b_being_Real_st_(a_*_u)_+_(b_*_(v_+_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_)
let a, b be Real; ::_thesis: ( (a * u) + (b * (v + u)) = 0. V implies ( a = 0 & b = 0 ) )
assume  (a * u) + (b * (v + u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 )
then A2: 0. V = (a * u) + ((b * u) + (b * v)) by RLVECT_1:def_5
.= ((a * u) + (b * u)) + (b * v) by RLVECT_1:def_3
.= ((a + b) * u) + (b * v) by RLVECT_1:def_6 ;
then  b = 0 by A1, RLVECT_3:13;
hence  ( a = 0 & b = 0 ) by A1, A2, RLVECT_3:13; ::_thesis: verum
end;
hence  {u,(v + u)} is linearly-independent by RLVECT_3:13; ::_thesis: verum
end;

theorem Th19: :: RLVECT_4:19
for a being Real
for V being RealLinearSpace
for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds
{u,(a * v)} is linearly-independent
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds
{u,(a * v)} is linearly-independent
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds
{u,(a * v)} is linearly-independent
let u, v be VECTOR of V; ::_thesis: ( {u,v} is linearly-independent & u <> v & a <> 0 implies {u,(a * v)} is linearly-independent )
assume that
A1: ( {u,v} is linearly-independent & u <> v ) and
A2: a <> 0 ; ::_thesis: {u,(a * v)} is linearly-independent
now__::_thesis:_for_b,_c_being_Real_st_(b_*_u)_+_(c_*_(a_*_v))_=_0._V_holds_
(_b_=_0_&_c_=_0_)
let b, c be Real; ::_thesis: ( (b * u) + (c * (a * v)) = 0. V implies ( b = 0 & c = 0 ) )
assume  (b * u) + (c * (a * v)) = 0. V ; ::_thesis: ( b = 0 & c = 0 )
then A3: 0. V = (b * u) + ((c * a) * v) by RLVECT_1:def_7;
then  c * a = 0 by A1, RLVECT_3:13;
hence  ( b = 0 & c = 0 ) by A1, A2, A3, RLVECT_3:13, XCMPLX_1:6; ::_thesis: verum
end;
hence  {u,(a * v)} is linearly-independent by RLVECT_3:13; ::_thesis: verum
end;

theorem :: RLVECT_4:20
for V being RealLinearSpace
for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(- v)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds
{u,(- v)} is linearly-independent
let u, v be VECTOR of V; ::_thesis: ( {u,v} is linearly-independent & u <> v implies {u,(- v)} is linearly-independent )
A1: - v = (- 1) * v by RLVECT_1:16;
assume  ( {u,v} is linearly-independent & u <> v ) ; ::_thesis: {u,(- v)} is linearly-independent
hence  {u,(- v)} is linearly-independent by A1, Th19; ::_thesis: verum
end;

theorem Th21: :: RLVECT_4:21
for a, b being Real
for V being RealLinearSpace
for v being VECTOR of V st a <> b holds
{(a * v),(b * v)} is linearly-dependent
proof
let a, b be Real; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V st a <> b holds
{(a * v),(b * v)} is linearly-dependent
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st a <> b holds
{(a * v),(b * v)} is linearly-dependent
let v be VECTOR of V; ::_thesis: ( a <> b implies {(a * v),(b * v)} is linearly-dependent )
assume A1: a <> b ; ::_thesis: {(a * v),(b * v)} is linearly-dependent
now__::_thesis:_{(a_*_v),(b_*_v)}_is_linearly-dependent
percases ( v = 0. V or v <> 0. V ) ;
suppose v = 0. V ; ::_thesis: {(a * v),(b * v)} is linearly-dependent
then  a * v = 0. V by RLVECT_1:10;
hence  {(a * v),(b * v)} is linearly-dependent by RLVECT_3:11; ::_thesis: verum
end;
supposeA2: v <> 0. V ; ::_thesis: {(a * v),(b * v)} is linearly-dependent
A3: (b * (a * v)) + ((- a) * (b * v)) = ((a * b) * v) + ((- a) * (b * v)) by RLVECT_1:def_7
.= ((a * b) * v) - (a * (b * v)) by Th3
.= ((a * b) * v) - ((a * b) * v) by RLVECT_1:def_7
.= 0. V by RLVECT_1:15 ;
A4: ( not b = 0 or not - a = 0 ) by A1;
 a * v <> b * v by A1, A2, RLVECT_1:37;
hence  {(a * v),(b * v)} is linearly-dependent by A3, A4, RLVECT_3:13; ::_thesis: verum
end;
end;
end;
hence  {(a * v),(b * v)} is linearly-dependent ; ::_thesis: verum
end;

theorem :: RLVECT_4:22
for a being Real
for V being RealLinearSpace
for v being VECTOR of V st a <> 1 holds
{v,(a * v)} is linearly-dependent
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V st a <> 1 holds
{v,(a * v)} is linearly-dependent
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V st a <> 1 holds
{v,(a * v)} is linearly-dependent
let v be VECTOR of V; ::_thesis: ( a <> 1 implies {v,(a * v)} is linearly-dependent )
 v = 1 * v by RLVECT_1:def_8;
hence  ( a <> 1 implies {v,(a * v)} is linearly-dependent ) by Th21; ::_thesis: verum
end;

theorem :: RLVECT_4:23
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(v - u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(v - u)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(v - u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; ::_thesis: {u,w,(v - u)} is linearly-independent
now__::_thesis:_for_a,_b,_c_being_Real_st_((a_*_u)_+_(b_*_w))_+_(c_*_(v_-_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_&_c_=_0_)
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * w)) + (c * (v - u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume  ((a * u) + (b * w)) + (c * (v - u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + (b * w)) + ((c * v) - (c * u)) by RLVECT_1:34
.= (a * u) + ((b * w) + ((c * v) - (c * u))) by RLVECT_1:def_3
.= (a * u) + (((b * w) + (c * v)) - (c * u)) by RLVECT_1:def_3
.= (a * u) + (((b * w) - (c * u)) + (c * v)) by RLVECT_1:def_3
.= ((a * u) + ((b * w) - (c * u))) + (c * v) by RLVECT_1:def_3
.= (((a * u) + (b * w)) - (c * u)) + (c * v) by RLVECT_1:def_3
.= (((a * u) - (c * u)) + (b * w)) + (c * v) by RLVECT_1:def_3
.= (((a - c) * u) + (b * w)) + (c * v) by RLVECT_1:35 ;
then  a - c = 0 by A1, Th7;
hence  ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th7; ::_thesis: verum
end;
hence  {u,w,(v - u)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem :: RLVECT_4:24
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(w - u),(v - u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(w - u),(v - u)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,(w - u),(v - u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; ::_thesis: {u,(w - u),(v - u)} is linearly-independent
now__::_thesis:_for_a,_b,_c_being_Real_st_((a_*_u)_+_(b_*_(w_-_u)))_+_(c_*_(v_-_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_&_c_=_0_)
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * (w - u))) + (c * (v - u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume  ((a * u) + (b * (w - u))) + (c * (v - u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + ((b * w) - (b * u))) + (c * (v - u)) by RLVECT_1:34
.= ((a * u) + ((b * w) + (- (b * u)))) + ((c * v) - (c * u)) by RLVECT_1:34
.= (((a * u) + (- (b * u))) + (b * w)) + ((- (c * u)) + (c * v)) by RLVECT_1:def_3
.= ((a * u) + (- (b * u))) + ((b * w) + ((- (c * u)) + (c * v))) by RLVECT_1:def_3
.= ((a * u) + (- (b * u))) + ((- (c * u)) + ((b * w) + (c * v))) by RLVECT_1:def_3
.= (((a * u) + (- (b * u))) + (- (c * u))) + ((b * w) + (c * v)) by RLVECT_1:def_3
.= (((a * u) + (b * (- u))) + (- (c * u))) + ((b * w) + (c * v)) by RLVECT_1:25
.= (((a * u) + ((- b) * u)) + (- (c * u))) + ((b * w) + (c * v)) by RLVECT_1:24
.= (((a * u) + ((- b) * u)) + (c * (- u))) + ((b * w) + (c * v)) by RLVECT_1:25
.= (((a * u) + ((- b) * u)) + ((- c) * u)) + ((b * w) + (c * v)) by RLVECT_1:24
.= (((a + (- b)) * u) + ((- c) * u)) + ((b * w) + (c * v)) by RLVECT_1:def_6
.= (((a + (- b)) + (- c)) * u) + ((b * w) + (c * v)) by RLVECT_1:def_6
.= ((((a + (- b)) + (- c)) * u) + (b * w)) + (c * v) by RLVECT_1:def_3 ;
then  ( (a + (- b)) + (- c) = 0 & b = 0 ) by A1, Th7;
hence  ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th7; ::_thesis: verum
end;
hence  {u,(w - u),(v - u)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem :: RLVECT_4:25
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(v + u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(v + u)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(v + u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; ::_thesis: {u,w,(v + u)} is linearly-independent
now__::_thesis:_for_a,_b,_c_being_Real_st_((a_*_u)_+_(b_*_w))_+_(c_*_(v_+_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_&_c_=_0_)
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * w)) + (c * (v + u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume  ((a * u) + (b * w)) + (c * (v + u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + (b * w)) + ((c * u) + (c * v)) by RLVECT_1:def_5
.= (a * u) + ((b * w) + ((c * u) + (c * v))) by RLVECT_1:def_3
.= (a * u) + ((c * u) + ((b * w) + (c * v))) by RLVECT_1:def_3
.= ((a * u) + (c * u)) + ((b * w) + (c * v)) by RLVECT_1:def_3
.= ((a + c) * u) + ((b * w) + (c * v)) by RLVECT_1:def_6
.= (((a + c) * u) + (b * w)) + (c * v) by RLVECT_1:def_3 ;
then  c = 0 by A1, Th7;
hence  ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th7; ::_thesis: verum
end;
hence  {u,w,(v + u)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem :: RLVECT_4:26
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(w + u),(v + u)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(w + u),(v + u)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,(w + u),(v + u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; ::_thesis: {u,(w + u),(v + u)} is linearly-independent
now__::_thesis:_for_a,_b,_c_being_Real_st_((a_*_u)_+_(b_*_(w_+_u)))_+_(c_*_(v_+_u))_=_0._V_holds_
(_a_=_0_&_b_=_0_&_c_=_0_)
let a, b, c be Real; ::_thesis: ( ((a * u) + (b * (w + u))) + (c * (v + u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume  ((a * u) + (b * (w + u))) + (c * (v + u)) = 0. V ; ::_thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + ((b * u) + (b * w))) + (c * (v + u)) by RLVECT_1:def_5
.= (((a * u) + (b * u)) + (b * w)) + (c * (v + u)) by RLVECT_1:def_3
.= (((a + b) * u) + (b * w)) + (c * (v + u)) by RLVECT_1:def_6
.= (((a + b) * u) + (b * w)) + ((c * u) + (c * v)) by RLVECT_1:def_5
.= ((a + b) * u) + ((b * w) + ((c * u) + (c * v))) by RLVECT_1:def_3
.= ((a + b) * u) + ((c * u) + ((b * w) + (c * v))) by RLVECT_1:def_3
.= (((a + b) * u) + (c * u)) + ((b * w) + (c * v)) by RLVECT_1:def_3
.= (((a + b) + c) * u) + ((b * w) + (c * v)) by RLVECT_1:def_6
.= ((((a + b) + c) * u) + (b * w)) + (c * v) by RLVECT_1:def_3 ;
then  ( (a + b) + c = 0 & b = 0 ) by A1, Th7;
hence  ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th7; ::_thesis: verum
end;
hence  {u,(w + u),(v + u)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem Th27: :: RLVECT_4:27
for a being Real
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds
{u,w,(a * v)} is linearly-independent
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds
{u,w,(a * v)} is linearly-independent
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds
{u,w,(a * v)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 implies {u,w,(a * v)} is linearly-independent )
assume that
A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) and
A2: a <> 0 ; ::_thesis: {u,w,(a * v)} is linearly-independent
now__::_thesis:_for_b,_c,_d_being_Real_st_((b_*_u)_+_(c_*_w))_+_(d_*_(a_*_v))_=_0._V_holds_
(_b_=_0_&_c_=_0_&_d_=_0_)
let b, c, d be Real; ::_thesis: ( ((b * u) + (c * w)) + (d * (a * v)) = 0. V implies ( b = 0 & c = 0 & d = 0 ) )
assume  ((b * u) + (c * w)) + (d * (a * v)) = 0. V ; ::_thesis: ( b = 0 & c = 0 & d = 0 )
then A3: 0. V = ((b * u) + (c * w)) + ((d * a) * v) by RLVECT_1:def_7;
then  d * a = 0 by A1, Th7;
hence  ( b = 0 & c = 0 & d = 0 ) by A1, A2, A3, Th7, XCMPLX_1:6; ::_thesis: verum
end;
hence  {u,w,(a * v)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem Th28: :: RLVECT_4:28
for a, b being Real
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds
{u,(a * w),(b * v)} is linearly-independent
proof
let a, b be Real; ::_thesis: for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds
{u,(a * w),(b * v)} is linearly-independent
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds
{u,(a * w),(b * v)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 implies {u,(a * w),(b * v)} is linearly-independent )
assume that
A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) and
A2: ( a <> 0 & b <> 0 ) ; ::_thesis: {u,(a * w),(b * v)} is linearly-independent
now__::_thesis:_for_c,_d,_e_being_Real_st_((c_*_u)_+_(d_*_(a_*_w)))_+_(e_*_(b_*_v))_=_0._V_holds_
(_c_=_0_&_d_=_0_&_e_=_0_)
let c, d, e be Real; ::_thesis: ( ((c * u) + (d * (a * w))) + (e * (b * v)) = 0. V implies ( c = 0 & d = 0 & e = 0 ) )
assume  ((c * u) + (d * (a * w))) + (e * (b * v)) = 0. V ; ::_thesis: ( c = 0 & d = 0 & e = 0 )
then A3: 0. V = ((c * u) + ((d * a) * w)) + (e * (b * v)) by RLVECT_1:def_7
.= ((c * u) + ((d * a) * w)) + ((e * b) * v) by RLVECT_1:def_7 ;
then  ( d * a = 0 & e * b = 0 ) by A1, Th7;
hence  ( c = 0 & d = 0 & e = 0 ) by A1, A2, A3, Th7, XCMPLX_1:6; ::_thesis: verum
end;
hence  {u,(a * w),(b * v)} is linearly-independent by Th7; ::_thesis: verum
end;

theorem :: RLVECT_4:29
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(- v)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(- v)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(- v)} is linearly-independent )
 - v = (- 1) * v by RLVECT_1:16;
hence  ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(- v)} is linearly-independent ) by Th27; ::_thesis: verum
end;

theorem :: RLVECT_4:30
for V being RealLinearSpace
for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(- w),(- v)} is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,(- w),(- v)} is linearly-independent
let u, w, v be VECTOR of V; ::_thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,(- w),(- v)} is linearly-independent )
 ( - v = (- 1) * v & - w = (- 1) * w ) by RLVECT_1:16;
hence  ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,(- w),(- v)} is linearly-independent ) by Th28; ::_thesis: verum
end;

theorem Th31: :: RLVECT_4:31
for a, b being Real
for V being RealLinearSpace
for v, w being VECTOR of V st a <> b holds
{(a * v),(b * v),w} is linearly-dependent
proof
let a, b be Real; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V st a <> b holds
{(a * v),(b * v),w} is linearly-dependent
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V st a <> b holds
{(a * v),(b * v),w} is linearly-dependent
let v, w be VECTOR of V; ::_thesis: ( a <> b implies {(a * v),(b * v),w} is linearly-dependent )
assume  a <> b ; ::_thesis: {(a * v),(b * v),w} is linearly-dependent
then  {(a * v),(b * v)} is linearly-dependent by Th21;
hence  {(a * v),(b * v),w} is linearly-dependent by RLVECT_3:5, SETWISEO:2; ::_thesis: verum
end;

theorem :: RLVECT_4:32
for a being Real
for V being RealLinearSpace
for v, w being VECTOR of V st a <> 1 holds
{v,(a * v),w} is linearly-dependent
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for v, w being VECTOR of V st a <> 1 holds
{v,(a * v),w} is linearly-dependent
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V st a <> 1 holds
{v,(a * v),w} is linearly-dependent
let v, w be VECTOR of V; ::_thesis: ( a <> 1 implies {v,(a * v),w} is linearly-dependent )
 v = 1 * v by RLVECT_1:def_8;
hence  ( a <> 1 implies {v,(a * v),w} is linearly-dependent ) by Th31; ::_thesis: verum
end;

theorem :: RLVECT_4:33
for V being RealLinearSpace
for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
proof
let V be RealLinearSpace; ::_thesis: for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
let v, w be VECTOR of V; ::_thesis: ( v in Lin {w} & v <> 0. V implies Lin {v} = Lin {w} )
assume that
A1: v in Lin {w} and
A2: v <> 0. V ; ::_thesis: Lin {v} = Lin {w}
consider a being Real such that
A3: v = a * w by A1, Th8;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_Lin_{v}_implies_u_in_Lin_{w}_)_&_(_u_in_Lin_{w}_implies_u_in_Lin_{v}_)_)
let u be VECTOR of V; ::_thesis: ( ( u in Lin {v} implies u in Lin {w} ) & ( u in Lin {w} implies u in Lin {v} ) )
A4: a <> 0 by A2, A3, RLVECT_1:10;
thus  ( u in Lin {v} implies u in Lin {w} ) ::_thesis: ( u in Lin {w} implies u in Lin {v} )
proof
assume  u in Lin {v} ; ::_thesis: u in Lin {w}
then consider b being Real such that
A5: u = b * v by Th8;
 u = (b * a) * w by A3, A5, RLVECT_1:def_7;
hence  u in Lin {w} by Th8; ::_thesis: verum
end;
assume  u in Lin {w} ; ::_thesis: u in Lin {v}
then consider b being Real such that
A6: u = b * w by Th8;
(a ") * v = ((a ") * a) * w by A3, RLVECT_1:def_7
.= 1 * w by A4, XCMPLX_0:def_7
.= w by RLVECT_1:def_8 ;
then  u = (b * (a ")) * v by A6, RLVECT_1:def_7;
hence  u in Lin {v} by Th8; ::_thesis: verum
end;
hence  Lin {v} = Lin {w} by RLSUB_1:31; ::_thesis: verum
end;

theorem :: RLVECT_4:34
for V being RealLinearSpace
for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
let v1, v2, w1, w2 be VECTOR of V; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} implies ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) )
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent and
A3: v1 in Lin {w1,w2} and
A4: v2 in Lin {w1,w2} ; ::_thesis: ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
consider r1, r2 being Real such that
A5: v1 = (r1 * w1) + (r2 * w2) by A3, Th11;
consider r3, r4 being Real such that
A6: v2 = (r3 * w1) + (r4 * w2) by A4, Th11;
set t = (r1 * r4) - (r2 * r3);
A7: now__::_thesis:_(_r1_=_0_implies_not_r2_=_0_)
assume  ( r1 = 0 & r2 = 0 ) ; ::_thesis: contradiction
then v1 = (0. V) + (0 * w2) by A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A2, RLVECT_3:11; ::_thesis: verum
end;
now__::_thesis:_not_r1_*_r4_=_r2_*_r3
assume A8: r1 * r4 = r2 * r3 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( r1 <> 0 or r2 <> 0 ) by A7;
supposeA9: r1 <> 0 ; ::_thesis: contradiction
 ((r1 ") * r1) * r4 = (r1 ") * (r2 * r3) by A8, XCMPLX_1:4;
then  1 * r4 = (r1 ") * (r2 * r3) by A9, XCMPLX_0:def_7;
then v2 = (r3 * w1) + ((r3 * ((r1 ") * r2)) * w2) by A6
.= (r3 * w1) + (r3 * (((r1 ") * r2) * w2)) by RLVECT_1:def_7
.= (r3 * 1) * (w1 + (((r1 ") * r2) * w2)) by RLVECT_1:def_5
.= (r3 * ((r1 ") * r1)) * (w1 + (((r1 ") * r2) * w2)) by A9, XCMPLX_0:def_7
.= ((r3 * (r1 ")) * r1) * (w1 + (((r1 ") * r2) * w2))
.= (r3 * (r1 ")) * (r1 * (w1 + (((r1 ") * r2) * w2))) by RLVECT_1:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (r1 * (((r1 ") * r2) * w2))) by RLVECT_1:def_5
.= (r3 * (r1 ")) * ((r1 * w1) + ((r1 * ((r1 ") * r2)) * w2)) by RLVECT_1:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (((r1 * (r1 ")) * r2) * w2))
.= (r3 * (r1 ")) * ((r1 * w1) + ((1 * r2) * w2)) by A9, XCMPLX_0:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (r2 * w2)) ;
hence  contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum
end;
supposeA10: r2 <> 0 ; ::_thesis: contradiction
(r2 ") * (r1 * r4) = (r2 ") * (r2 * r3) by A8
.= ((r2 ") * r2) * r3
.= 1 * r3 by A10, XCMPLX_0:def_7
.= r3 ;
then v2 = ((r4 * ((r2 ") * r1)) * w1) + (r4 * w2) by A6
.= (r4 * (((r2 ") * r1) * w1)) + (r4 * w2) by RLVECT_1:def_7
.= (r4 * 1) * ((((r2 ") * r1) * w1) + w2) by RLVECT_1:def_5
.= (r4 * ((r2 ") * r2)) * ((((r2 ") * r1) * w1) + w2) by A10, XCMPLX_0:def_7
.= ((r4 * (r2 ")) * r2) * ((((r2 ") * r1) * w1) + w2)
.= (r4 * (r2 ")) * (r2 * ((((r2 ") * r1) * w1) + w2)) by RLVECT_1:def_7
.= (r4 * (r2 ")) * ((r2 * (((r2 ") * r1) * w1)) + (r2 * w2)) by RLVECT_1:def_5
.= (r4 * (r2 ")) * (((r2 * ((r2 ") * r1)) * w1) + (r2 * w2)) by RLVECT_1:def_7
.= (r4 * (r2 ")) * ((((r2 * (r2 ")) * r1) * w1) + (r2 * w2))
.= (r4 * (r2 ")) * (((1 * r1) * w1) + (r2 * w2)) by A10, XCMPLX_0:def_7
.= (r4 * (r2 ")) * ((r1 * w1) + (r2 * w2)) ;
hence  contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
then A11: (r1 * r4) - (r2 * r3) <> 0 ;
A12: now__::_thesis:_(_r2_<>_0_implies_(_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_&_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_)_)
assume A13: r2 <> 0 ; ::_thesis: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) )
(r2 ") * v1 = ((r2 ") * (r1 * w1)) + ((r2 ") * (r2 * w2)) by A5, RLVECT_1:def_5
.= (((r2 ") * r1) * w1) + ((r2 ") * (r2 * w2)) by RLVECT_1:def_7
.= (((r2 ") * r1) * w1) + (((r2 ") * r2) * w2) by RLVECT_1:def_7
.= (((r2 ") * r1) * w1) + (1 * w2) by A13, XCMPLX_0:def_7
.= (((r2 ") * r1) * w1) + w2 by RLVECT_1:def_8 ;
then A14: w2 = ((r2 ") * v1) - (((r2 ") * r1) * w1) by RLSUB_2:61;
then  w2 = ((r2 ") * v1) - ((r2 ") * (r1 * w1)) by RLVECT_1:def_7;
then v2 = (r3 * w1) + (r4 * ((r2 ") * (v1 - (r1 * w1)))) by A6, RLVECT_1:34
.= (r3 * w1) + ((r4 * (r2 ")) * (v1 - (r1 * w1))) by RLVECT_1:def_7
.= (r3 * w1) + (((r4 * (r2 ")) * v1) - ((r4 * (r2 ")) * (r1 * w1))) by RLVECT_1:34
.= ((r3 * w1) + ((r4 * (r2 ")) * v1)) - ((r4 * (r2 ")) * (r1 * w1)) by RLVECT_1:def_3
.= (((r4 * (r2 ")) * v1) + (r3 * w1)) - (((r4 * (r2 ")) * r1) * w1) by RLVECT_1:def_7
.= ((r4 * (r2 ")) * v1) + ((r3 * w1) - (((r4 * (r2 ")) * r1) * w1)) by RLVECT_1:def_3
.= ((r4 * (r2 ")) * v1) + ((r3 - ((r4 * (r2 ")) * r1)) * w1) by RLVECT_1:35 ;
then r2 * v2 = (r2 * ((r4 * (r2 ")) * v1)) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_5
.= ((r2 * (r4 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_7
.= ((r4 * (r2 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1))
.= ((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by A13, XCMPLX_0:def_7
.= (r4 * v1) + ((r2 * (r3 - ((r4 * (r2 ")) * r1))) * w1) by RLVECT_1:def_7
.= (r4 * v1) + (((r2 * r3) - ((r2 * (r2 ")) * (r4 * r1))) * w1)
.= (r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1) by A13, XCMPLX_0:def_7
.= (r4 * v1) + ((- ((r1 * r4) - (r2 * r3))) * w1)
.= (r4 * v1) + (- (((r1 * r4) - (r2 * r3)) * w1)) by Th3 ;
then  - (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1) by RLSUB_2:61;
then ((r1 * r4) - (r2 * r3)) * w1 = - ((r2 * v2) - (r4 * v1)) by RLVECT_1:17
.= (r4 * v1) + (- (r2 * v2)) by RLVECT_1:33 ;
then  ((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_7;
then  1 * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by A11, XCMPLX_0:def_7;
then w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_8
.= ((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_5
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * ((- r2) * v2)) by Th3
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((((r1 * r4) - (r2 * r3)) ") * (- r2)) * v2) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((- (((r1 * r4) - (r2 * r3)) ")) * r2) * v2)
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- (((r1 * r4) - (r2 * r3)) ")) * (r2 * v2)) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2))) by Th3 ;
hence  w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by RLVECT_1:def_7; ::_thesis: w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2)
then A15: w2 = ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))) by A14, RLVECT_1:def_7
.= ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (((r2 ") * r1) * ((((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:34
.= ((r2 ") * v1) - (((r1 * (r2 ")) * (((r1 * r4) - (r2 * r3)) ")) * ((r4 * v1) - (r2 * v2))) by RLVECT_1:def_7
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * v1) - (r2 * v2)))
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - ((r2 ") * (r2 * v2))))) by RLVECT_1:34
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (1 * v2)))) by A13, XCMPLX_0:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - v2))) by RLVECT_1:def_8
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2)) by RLVECT_1:29
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:35 ;
(r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) = (r2 ") * (1 - (r1 * ((((r1 * r4) - (r2 * r3)) ") * r4)))
.= (r2 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) - ((((r1 * r4) - (r2 * r3)) ") * (r1 * r4))) by A11, XCMPLX_0:def_7
.= (((r2 ") * r2) * (((r1 * r4) - (r2 * r3)) ")) * (- r3)
.= (1 * (((r1 * r4) - (r2 * r3)) ")) * (- r3) by A13, XCMPLX_0:def_7
.= - ((((r1 * r4) - (r2 * r3)) ") * r3) ;
hence  w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by A15, Th3; ::_thesis: verum
end;
set a4 = (((r1 * r4) - (r2 * r3)) ") * r1;
set a3 = - ((((r1 * r4) - (r2 * r3)) ") * r3);
set a2 = - ((((r1 * r4) - (r2 * r3)) ") * r2);
set a1 = (((r1 * r4) - (r2 * r3)) ") * r4;
now__::_thesis:_(_r1_<>_0_implies_(_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_&_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_)_)
assume A16: r1 <> 0 ; ::_thesis: ( w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) )
A17: (r1 ") + ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) = (r1 ") * (1 + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3)))
.= (r1 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3))) by A11, XCMPLX_0:def_7
.= (((r1 * r4) - (r2 * r3)) ") * (((r1 ") * r1) * r4)
.= (((r1 * r4) - (r2 * r3)) ") * (1 * r4) by A16, XCMPLX_0:def_7
.= (((r1 * r4) - (r2 * r3)) ") * r4 ;
(r1 ") * v1 = ((r1 ") * (r1 * w1)) + ((r1 ") * (r2 * w2)) by A5, RLVECT_1:def_5
.= (((r1 ") * r1) * w1) + ((r1 ") * (r2 * w2)) by RLVECT_1:def_7
.= (1 * w1) + ((r1 ") * (r2 * w2)) by A16, XCMPLX_0:def_7
.= w1 + ((r1 ") * (r2 * w2)) by RLVECT_1:def_8
.= w1 + ((r2 * (r1 ")) * w2) by RLVECT_1:def_7 ;
then A18: w1 = ((r1 ") * v1) - ((r2 * (r1 ")) * w2) by RLSUB_2:61;
then v2 = ((r3 * ((r1 ") * v1)) - (r3 * ((r2 * (r1 ")) * w2))) + (r4 * w2) by A6, RLVECT_1:34
.= (((r3 * (r1 ")) * v1) - (r3 * (((r1 ") * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7
.= (((r3 * (r1 ")) * v1) - ((r3 * ((r1 ") * r2)) * w2)) + (r4 * w2) by RLVECT_1:def_7
.= (((r3 * (r1 ")) * v1) - (((r1 ") * (r3 * r2)) * w2)) + (r4 * w2)
.= ((((r1 ") * r3) * v1) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7
.= (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7 ;
then r1 * v2 = (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + (r1 * (r4 * w2)) by RLVECT_1:def_5
.= (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= ((r1 * ((r1 ") * (r3 * v1))) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:34
.= (((r1 * (r1 ")) * (r3 * v1)) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= (((r1 * (r1 ")) * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= ((1 * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7
.= ((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7
.= ((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_8
.= ((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2) by RLVECT_1:def_8
.= (r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2)) by RLVECT_1:29
.= (r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2)) by RLVECT_1:35
.= (r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2) by Th3
.= (r3 * v1) + (((r1 * r4) - (r2 * r3)) * w2) ;
then (((r1 * r4) - (r2 * r3)) ") * (r1 * v2) = ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (((r1 * r4) - (r2 * r3)) * w2)) by RLVECT_1:def_5
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w2) by RLVECT_1:def_7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (1 * w2) by A11, XCMPLX_0:def_7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + w2 by RLVECT_1:def_8 ;
hence w2 = ((((r1 * r4) - (r2 * r3)) ") * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLSUB_2:61
.= (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLVECT_1:def_7
.= (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:def_7 ;
::_thesis: w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))
hence w1 = ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (r1 ")) * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A18, RLVECT_1:def_5
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + (((r2 * (r1 ")) * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (((r1 ") * r1) * (((r1 * r4) - (r2 * r3)) "))) * v2))
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (1 * (((r1 * r4) - (r2 * r3)) "))) * v2)) by A16, XCMPLX_0:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * ((- (((r1 * r4) - (r2 * r3)) ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by Th3
.= ((r1 ") * v1) - ((((r2 * (r1 ")) * (- (((r1 * r4) - (r2 * r3)) "))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * (r1 ")) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2))
.= ((r1 ") * v1) - (((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * ((r1 ") * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * (r2 * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((- 1) * ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:16
.= ((r1 ") * v1) - ((- (((((r1 * r4) - (r2 * r3)) ") * r2) * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= (((r1 ") * v1) - (- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:27
.= (((r1 ") * v1) + (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:17
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by A17, RLVECT_1:def_6 ;
::_thesis: verum
end;
then A19: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2) & w2 = ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) by A7, A12, Th3;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_Lin_{w1,w2}_implies_u_in_Lin_{v1,v2}_)_&_(_u_in_Lin_{v1,v2}_implies_u_in_Lin_{w1,w2}_)_)
let u be VECTOR of V; ::_thesis: ( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) )
thus  ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) ::_thesis: ( u in Lin {v1,v2} implies u in Lin {w1,w2} )
proof
assume  u in Lin {w1,w2} ; ::_thesis: u in Lin {v1,v2}
then consider r5, r6 being Real such that
A20: u = (r5 * w1) + (r6 * w2) by Th11;
u = ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (r6 * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, A20, RLVECT_1:def_5
.= ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ;
hence  u in Lin {v1,v2} by Th11; ::_thesis: verum
end;
assume  u in Lin {v1,v2} ; ::_thesis: u in Lin {w1,w2}
then consider r5, r6 being Real such that
A21: u = (r5 * v1) + (r6 * v2) by Th11;
u = (r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by A5, A6, A21, RLVECT_1:def_5
.= ((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by RLVECT_1:def_5
.= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2)) by RLVECT_1:def_3
.= (((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_3
.= ((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_7
.= ((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_6
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2)) by RLVECT_1:def_3
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2) by RLVECT_1:def_6 ;
hence  u in Lin {w1,w2} by Th11; ::_thesis: verum
end;
hence  Lin {w1,w2} = Lin {v1,v2} by RLSUB_1:31; ::_thesis: ( {w1,w2} is linearly-independent & w1 <> w2 )
now__::_thesis:_for_a,_b_being_Real_st_(a_*_w1)_+_(b_*_w2)_=_0._V_holds_
(_not_a_<>_0_&_not_b_<>_0_)
let a, b be Real; ::_thesis: ( (a * w1) + (b * w2) = 0. V implies ( not a <> 0 & not b <> 0 ) )
A22: ((r1 * r4) - (r2 * r3)) " <> 0 by A11, XCMPLX_1:202;
assume  (a * w1) + (b * w2) = 0. V ; ::_thesis: ( not a <> 0 & not b <> 0 )
then A23: 0. V = ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (b * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, RLVECT_1:def_5
.= ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (b * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ;
then  0 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * a) + ((- r3) * b)) by A1, A2, RLVECT_3:13;
then A24: (r4 * a) - (r3 * b) = 0 by A22, XCMPLX_1:6;
 0 = (((r1 * r4) - (r2 * r3)) ") * (((- r2) * a) + (r1 * b)) by A1, A2, A23, RLVECT_3:13;
then A25: (r1 * b) + (- (r2 * a)) = 0 by A22, XCMPLX_1:6;
assume A26: ( a <> 0 or b <> 0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a <> 0 or b <> 0 ) by A26;
supposeA27: a <> 0 ; ::_thesis: contradiction
 (a ") * (r1 * b) = ((a ") * a) * r2 by A25, XCMPLX_1:4;
then  (a ") * (r1 * b) = 1 * r2 by A27, XCMPLX_0:def_7;
then  r2 = r1 * ((a ") * b) ;
then  v1 = (r1 * w1) + (r1 * (((a ") * b) * w2)) by A5, RLVECT_1:def_7;
then A28: v1 = r1 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5;
 ((a ") * a) * r4 = (a ") * (r3 * b) by A24, XCMPLX_1:4;
then  1 * r4 = (a ") * (r3 * b) by A27, XCMPLX_0:def_7;
then  r4 = r3 * ((a ") * b) ;
then  v2 = (r3 * w1) + (r3 * (((a ") * b) * w2)) by A6, RLVECT_1:def_7;
then  v2 = r3 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5;
hence  contradiction by A1, A2, A28, Th21; ::_thesis: verum
end;
supposeA29: b <> 0 ; ::_thesis: contradiction
 ((b ") * b) * r1 = (b ") * (r2 * a) by A25, XCMPLX_1:4;
then  1 * r1 = (b ") * (r2 * a) by A29, XCMPLX_0:def_7;
then  r1 = r2 * ((b ") * a) ;
then  v1 = (r2 * (((b ") * a) * w1)) + (r2 * w2) by A5, RLVECT_1:def_7;
then A30: v1 = r2 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5;
 ((b ") * b) * r3 = (b ") * (r4 * a) by A24, XCMPLX_1:4;
then  1 * r3 = (b ") * (r4 * a) by A29, XCMPLX_0:def_7;
then  r3 = r4 * ((b ") * a) ;
then  v2 = (r4 * (((b ") * a) * w1)) + (r4 * w2) by A6, RLVECT_1:def_7;
then  v2 = r4 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5;
hence  contradiction by A1, A2, A30, Th21; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( {w1,w2} is linearly-independent & w1 <> w2 ) by RLVECT_3:13; ::_thesis: verum
end;

theorem :: RLVECT_4:35
for V being RealLinearSpace
for w, v being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds
ex a being Real st v = a * w
proof
let V be RealLinearSpace; ::_thesis: for w, v being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds
ex a being Real st v = a * w
let w, v be VECTOR of V; ::_thesis: ( w <> 0. V & {v,w} is linearly-dependent implies ex a being Real st v = a * w )
assume that
A1: w <> 0. V and
A2: {v,w} is linearly-dependent ; ::_thesis: ex a being Real st v = a * w
consider a, b being Real such that
A3: (a * v) + (b * w) = 0. V and
A4: ( a <> 0 or b <> 0 ) by A2, RLVECT_3:13;
A5: a * v = - (b * w) by A3, RLVECT_1:6;
now__::_thesis:_ex_a_being_Real_st_v_=_a_*_w
percases ( a <> 0 or a = 0 ) ;
supposeA6: a <> 0 ; ::_thesis: ex a being Real st v = a * w
 ((a ") * a) * v = (a ") * (- (b * w)) by A5, RLVECT_1:def_7;
then  1 * v = (a ") * (- (b * w)) by A6, XCMPLX_0:def_7;
then v = (a ") * (- (b * w)) by RLVECT_1:def_8
.= (a ") * ((- b) * w) by Th3
.= ((a ") * (- b)) * w by RLVECT_1:def_7 ;
hence  ex a being Real st v = a * w ; ::_thesis: verum
end;
supposeA7: a = 0 ; ::_thesis: ex a being Real st v = a * w
then  0. V = - (b * w) by A5, RLVECT_1:10;
then A8: 0. V = (- b) * w by Th3;
 - b <> 0 by A4, A7;
hence  ex a being Real st v = a * w by A1, A8, RLVECT_1:11; ::_thesis: verum
end;
end;
end;
hence  ex a being Real st v = a * w ; ::_thesis: verum
end;

theorem :: RLVECT_4:36
for V being RealLinearSpace
for v, w, u being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds
ex a, b being Real st u = (a * v) + (b * w)
proof
let V be RealLinearSpace; ::_thesis: for v, w, u being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds
ex a, b being Real st u = (a * v) + (b * w)
let v, w, u be VECTOR of V; ::_thesis: ( v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent implies ex a, b being Real st u = (a * v) + (b * w) )
assume that
A1: ( v <> w & {v,w} is linearly-independent ) and
A2: {u,v,w} is linearly-dependent ; ::_thesis: ex a, b being Real st u = (a * v) + (b * w)
consider a, b, c being Real such that
A3: ((a * u) + (b * v)) + (c * w) = 0. V and
A4: ( a <> 0 or b <> 0 or c <> 0 ) by A2, Th7;
now__::_thesis:_ex_a,_b_being_Real_st_u_=_(a_*_v)_+_(b_*_w)
percases ( a <> 0 or a = 0 ) ;
supposeA5: a <> 0 ; ::_thesis: ex a, b being Real st u = (a * v) + (b * w)
 (a * u) + ((b * v) + (c * w)) = 0. V by A3, RLVECT_1:def_3;
then  a * u = - ((b * v) + (c * w)) by RLVECT_1:6;
then  ((a ") * a) * u = (a ") * (- ((b * v) + (c * w))) by RLVECT_1:def_7;
then  1 * u = (a ") * (- ((b * v) + (c * w))) by A5, XCMPLX_0:def_7;
then u = (a ") * (- ((b * v) + (c * w))) by RLVECT_1:def_8
.= (a ") * ((- 1) * ((b * v) + (c * w))) by RLVECT_1:16
.= ((a ") * (- 1)) * ((b * v) + (c * w)) by RLVECT_1:def_7
.= (((a ") * (- 1)) * (b * v)) + (((a ") * (- 1)) * (c * w)) by RLVECT_1:def_5
.= ((((a ") * (- 1)) * b) * v) + (((a ") * (- 1)) * (c * w)) by RLVECT_1:def_7
.= ((((a ") * (- 1)) * b) * v) + ((((a ") * (- 1)) * c) * w) by RLVECT_1:def_7 ;
hence  ex a, b being Real st u = (a * v) + (b * w) ; ::_thesis: verum
end;
supposeA6: a = 0 ; ::_thesis: ex a, b being Real st u = (a * v) + (b * w)
then  0. V = ((0. V) + (b * v)) + (c * w) by A3, RLVECT_1:10
.= (b * v) + (c * w) by RLVECT_1:4 ;
hence  ex a, b being Real st u = (a * v) + (b * w) by A1, A4, A6, RLVECT_3:13; ::_thesis: verum
end;
end;
end;
hence  ex a, b being Real st u = (a * v) + (b * w) ; ::_thesis: verum
end;

theorem :: RLVECT_4:37
for V being RealLinearSpace
for v being VECTOR of V
for a being Real ex l being Linear_Combination of {v} st l . v = a by Lm1;

theorem :: RLVECT_4:38
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) by Lm2;

theorem :: RLVECT_4:39
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex l being Linear_Combination of {v1,v2,v3} st
( l . v1 = a & l . v2 = b & l . v3 = c ) by Lm3;