let V be RealLinearSpace; :: thesis: for p, q, r being Element of V st p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect holds
ex a, b being Real st r = (a * p) + (b * q)
let p, q, r be Element of V; :: thesis: ( p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect implies ex a, b being Real st r = (a * p) + (b * q) )
assume A1: ( p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect ) ; :: thesis: ex a, b being Real st r = (a * p) + (b * q)
then ( not p is zero & not q is zero & not r is zero ) by Def1;
then A2: ( p <> 0. V & q <> 0. V & r <> 0. V ) by STRUCT_0:def 15;
consider a, b, c being Real such that
A3: ( ((a * p) + (b * q)) + (c * r) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) by A1, ANPROJ_1:def 3;
A4: c <> 0

proof

assume A5: not c <> 0 ; :: thesis: contradiction
A6: ( a <> 0 & b <> 0 )

proof

assume A7: ( not a <> 0 or not b <> 0 ) ; :: thesis: contradiction

A8: now

assume A9: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * q)) + (0 * r) by A3, A5, RLVECT_1:23
.= ((0. V) + (b * q)) + (0. V) by RLVECT_1:23
.= (b * q) + (0. V) by RLVECT_1:10
.= b * q by RLVECT_1:10 ;
hence contradiction by A2, A3, A5, A9, RLVECT_1:24; :: thesis: verum

end;

now

assume A10: b = 0 ; :: thesis: contradiction
then 0. V = ((a * p) + (0. V)) + (0 * r) by A3, A5, RLVECT_1:23
.= ((a * p) + (0. V)) + (0. V) by RLVECT_1:23
.= (a * p) + (0. V) by RLVECT_1:10
.= a * p by RLVECT_1:10 ;
hence contradiction by A2, A3, A5, A10, RLVECT_1:24; :: thesis: verum

end;

hence contradiction by A7, A8; :: thesis: verum

end;

0. V = ((a * p) + (b * q)) + (0. V) by A3, A5, RLVECT_1:23
.= (a * p) + (b * q) by RLVECT_1:10 ;
then A11: a * p = - (b * q) by RLVECT_1:19
.= (- b) * q by Lm8 ;
- b <> 0 by A6;
hence contradiction by A1, A6, A11, ANPROJ_1:def 2; :: thesis: verum

end;

c * r = - ((a * p) + (b * q)) by A3, RLVECT_1:def 11
.= (- (a * p)) + (- (b * q)) by RLVECT_1:45
.= ((- a) * p) + (- (b * q)) by Lm8
.= ((- a) * p) + ((- b) * q) by Lm8 ;
then (c " ) * (c * r) = ((c " ) * ((- a) * p)) + ((c " ) * ((- b) * q)) by RLVECT_1:def 9
.= (((c " ) * (- a)) * p) + ((c " ) * ((- b) * q)) by RLVECT_1:def 9
.= (((c " ) * (- a)) * p) + (((c " ) * (- b)) * q) by RLVECT_1:def 9 ;
then (((c " ) * (- a)) * p) + (((c " ) * (- b)) * q) = ((c " ) * c) * r by RLVECT_1:def 9
.= 1 * r by A4, XCMPLX_0:def 7
.= r by RLVECT_1:def 9 ;
hence ex a, b being Real st r = (a * p) + (b * q) ; :: thesis: verum