let V be RealLinearSpace; :: thesis: for v, w, u being Element of V st not v is zero & not w is zero & not are_Prop v,w holds
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
let v, w, u be Element of V; :: thesis: ( not v is zero & not w is zero & not are_Prop v,w implies ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) )
assume that
A1: ( not v is zero & not w is zero ) and
A2: not are_Prop v,w ; :: thesis: ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
A3: ( v <> 0. V & w <> 0. V ) by A1, STRUCT_0:def 15;
A4: ( v,w,u are_LinDep implies ex a, b being Real st u = (a * v) + (b * w) )

proof

assume v,w,u are_LinDep ; :: thesis: ex a, b being Real st u = (a * v) + (b * w)
then u,v,w are_LinDep by Th10;
then consider a, b, c being Real such that
A5: ((a * u) + (b * v)) + (c * w) = 0. V and
A6: ( a <> 0 or b <> 0 or c <> 0 ) by Def3;
a <> 0

proof

assume A7: a = 0 ; :: thesis: contradiction
then A8: 0. V = ((0. V) + (b * v)) + (c * w) by A5, RLVECT_1:23
.= (b * v) + (c * w) by RLVECT_1:10 ;
then b * v = (- c) * w by Lm1;
then A9: ( b = 0 or - c = 0 ) by A2, Def2;
A10: b <> 0

proof

assume A11: b = 0 ; :: thesis: contradiction
then 0. V = (0. V) + (c * w) by A8, RLVECT_1:23
.= c * w by RLVECT_1:10 ;
hence contradiction by A3, A6, A7, A11, RLVECT_1:24; :: thesis: verum

end;

c <> 0

proof

assume A12: c = 0 ; :: thesis: contradiction
then 0. V = (b * v) + (0. V) by A8, RLVECT_1:23
.= b * v by RLVECT_1:10 ;
hence contradiction by A3, A6, A7, A12, RLVECT_1:24; :: thesis: verum

end;

hence contradiction by A9, A10; :: thesis: verum

end;

then u = ((- ((a " ) * b)) * v) + ((- ((a " ) * c)) * w) by A5, Lm2;
hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum

end;

( ex a, b being Real st u = (a * v) + (b * w) implies v,w,u are_LinDep )

proof

given a, b being Real such that A13: u = (a * v) + (b * w) ; :: thesis: v,w,u are_LinDep
0. V = ((a * v) + (b * w)) + (- u) by A13, RLVECT_1:16
.= ((a * v) + (b * w)) + ((- 1) * u) by RLVECT_1:29 ;
hence v,w,u are_LinDep by Def3; :: thesis: verum

end;

hence ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) by A4; :: thesis: verum