let V be RealLinearSpace; :: thesis: for p, q, r being Element of V st ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) holds
for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
let p, q, r be Element of V; :: thesis: ( ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) implies for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )
assume that
A1: for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) and
A2: for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; :: thesis: for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
let u, u1 be Element of V; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
consider a, b, c being Real such that
A3: u = ((a * p) + (b * q)) + (c * r) by A1;
consider a1, b1, c1 being Real such that
A4: u1 = ((a1 * p) + (b1 * q)) + (c1 * r) by A1;
A5: for a3, b3 being Real holds (a3 * u) + (b3 * u1) = ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r)

proof

let a3, b3 be Real; :: thesis: (a3 * u) + (b3 * u1) = ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r)
a3 * u = (((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r) by A3, Lm2;
hence (a3 * u) + (b3 * u1) = ((((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r)) + ((((b3 * a1) * p) + ((b3 * b1) * q)) + ((b3 * c1) * r)) by A4, Lm2
.= ((((a3 * a) * p) + ((b3 * a1) * p)) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r)) by Lm3
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r)) by RLVECT_1:def 6
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) * r) + ((b3 * c1) * r)) by RLVECT_1:def 6
.= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r) by RLVECT_1:def 6 ;
:: thesis: verum

end;

A6: not q is zero by A2, Th1;

A7: now :: thesis: ( ( are_Prop u,u1 or u is zero or u1 is zero ) implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

A8: now :: thesis: ( u1 is zero implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

assume u1 is zero ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then u1 = 0. V ;
then ( p,q,q are_LinDep & u,u1,q are_LinDep ) by ANPROJ_1:10, ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A6; :: thesis: verum

end;

A9: now :: thesis: ( u is zero implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

assume u is zero ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then u = 0. V ;
then ( p,q,q are_LinDep & u,u1,q are_LinDep ) by ANPROJ_1:10, ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A6; :: thesis: verum

end;

A10: now :: thesis: ( are_Prop u,u1 implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

assume are_Prop u,u1 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then ( p,q,q are_LinDep & u,u1,q are_LinDep ) by ANPROJ_1:11;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A6; :: thesis: verum

end;

assume ( are_Prop u,u1 or u is zero or u1 is zero ) ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A10, A9, A8; :: thesis: verum

end;

A11: ( not p is zero & not are_Prop p,q ) by A2, Th1;

A12: now :: thesis: ( not are_Prop u,u1 & not u is zero & not u1 is zero & c <> 0 implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

assume that
A13: not are_Prop u,u1 and
A14: not u is zero and
A15: not u1 is zero and
A16: c <> 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )

A17: now :: thesis: ( c1 <> 0 implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

set a3 = 1;
set b3 = - (c * (c1 "));
set y = (1 * u) + ((- (c * (c1 "))) * u1);
assume A18: c1 <> 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then c1 " <> 0 by XCMPLX_1:202;
then A19: c * (c1 ") <> 0 by A16, XCMPLX_1:6;
A20: not (1 * u) + ((- (c * (c1 "))) * u1) is zero

proof

assume (1 * u) + ((- (c * (c1 "))) * u1) is zero ; :: thesis: contradiction
then 0. V = (1 * u) + ((- (c * (c1 "))) * u1)
.= (1 * u) + ((c * (c1 ")) * (- u1)) by RLVECT_1:24
.= (1 * u) + (- ((c * (c1 ")) * u1)) by RLVECT_1:25 ;
then - (1 * u) = - ((c * (c1 ")) * u1) by RLVECT_1:def 10;
then 1 * u = (c * (c1 ")) * u1 by RLVECT_1:18;
hence contradiction by A13, A19; :: thesis: verum

end;

(1 * c) + ((- (c * (c1 "))) * c1) = c + ((- c) * ((c1 ") * c1))
.= c + ((- c) * 1) by A18, XCMPLX_0:def 7
.= 0 ;
then (1 * u) + ((- (c * (c1 "))) * u1) = ((((1 * a) + ((- (c * (c1 "))) * a1)) * p) + (((1 * b) + ((- (c * (c1 "))) * b1)) * q)) + (0 * r) by A5
.= ((((1 * a) + ((- (c * (c1 "))) * a1)) * p) + (((1 * b) + ((- (c * (c1 "))) * b1)) * q)) + (0. V) by RLVECT_1:10
.= (((1 * a) + ((- (c * (c1 "))) * a1)) * p) + (((1 * b) + ((- (c * (c1 "))) * b1)) * q) by RLVECT_1:4 ;
then A21: p,q,(1 * u) + ((- (c * (c1 "))) * u1) are_LinDep by A6, A11, ANPROJ_1:6;
u,u1,(1 * u) + ((- (c * (c1 "))) * u1) are_LinDep by A13, A14, A15, ANPROJ_1:6;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A20, A21; :: thesis: verum

end;

now :: thesis: ( c1 = 0 implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

set a3 = 0 ;
set b3 = 1;
set y = (0 * u) + (1 * u1);
A22: (0 * u) + (1 * u1) = (0 * u) + u1 by RLVECT_1:def 8
.= (0. V) + u1 by RLVECT_1:10
.= u1 by RLVECT_1:4 ;
assume c1 = 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )
then (0 * c) + (1 * c1) = 0 ;
then (0 * u) + (1 * u1) = ((((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q)) + (0 * r) by A5
.= ((((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q)) + (0. V) by RLVECT_1:10
.= (((0 * a) + (1 * a1)) * p) + (((0 * b) + (1 * b1)) * q) by RLVECT_1:4 ;
then A23: p,q,(0 * u) + (1 * u1) are_LinDep by A6, A11, ANPROJ_1:6;
u,u1,(0 * u) + (1 * u1) are_LinDep by A13, A14, A15, ANPROJ_1:6;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A15, A22, A23; :: thesis: verum

end;

hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A17; :: thesis: verum

end;

now :: thesis: ( not are_Prop u,u1 & not u is zero & not u1 is zero & c = 0 implies ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) )

assume that
A24: not are_Prop u,u1 and
A25: not u is zero and
A26: not u1 is zero and
A27: c = 0 ; :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )

now :: thesis: ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero )

set a3 = 1;
set b3 = 0 ;
set y = (1 * u) + (0 * u1);
A28: (1 * u) + (0 * u1) = u + (0 * u1) by RLVECT_1:def 8
.= u + (0. V) by RLVECT_1:10
.= u by RLVECT_1:4 ;
(1 * c) + (0 * c1) = 0 by A27;
then (1 * u) + (0 * u1) = ((((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q)) + (0 * r) by A5
.= ((((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q)) + (0. V) by RLVECT_1:10
.= (((1 * a) + (0 * a1)) * p) + (((1 * b) + (0 * b1)) * q) by RLVECT_1:4 ;
then A29: p,q,(1 * u) + (0 * u1) are_LinDep by A6, A11, ANPROJ_1:6;
u,u1,(1 * u) + (0 * u1) are_LinDep by A24, A25, A26, ANPROJ_1:6;
hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A25, A28, A29; :: thesis: verum

end;

hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) ; :: thesis: verum

end;

hence ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & not y is zero ) by A7, A12; :: thesis: verum