let V be RealLinearSpace; :: thesis: for u, v, w 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 u, v, w 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 and
A2: not w is zero and
A3: not are_Prop v,w ; :: thesis: ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
A4: w <> 0. V by A2;
A5: v <> 0. V by A1;
A6: ( 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 Th5;
then consider a, b, c being Real such that
A7: ((a * u) + (b * v)) + (c * w) = 0. V and
A8: ( a <> 0 or b <> 0 or c <> 0 ) ;
a <> 0

proof

assume A9: a = 0 ; :: thesis: contradiction
then A10: 0. V = ((0. V) + (b * v)) + (c * w) by A7, RLVECT_1:10
.= (b * v) + (c * w) ;
A11: b <> 0

proof

assume A12: b = 0 ; :: thesis: contradiction
then 0. V = (0. V) + (c * w) by A10, RLVECT_1:10
.= c * w ;
hence contradiction by A4, A8, A9, A12, RLVECT_1:11; :: thesis: verum

end;

A13: c <> 0

proof

assume A14: c = 0 ; :: thesis: contradiction
then 0. V = (b * v) + (0. V) by A10, RLVECT_1:10
.= b * v ;
hence contradiction by A5, A8, A9, A14, RLVECT_1:11; :: thesis: verum

end;

b * v = (- c) * w by A10, Lm1;
then ( b = 0 or - c = 0 ) by A3;
hence contradiction by A11, A13; :: thesis: verum

end;

then u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w) by A7, 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 A15: u = (a * v) + (b * w) ; :: thesis: v,w,u are_LinDep
0. V = ((a * v) + (b * w)) + (- u) by A15, RLVECT_1:5
.= ((a * v) + (b * w)) + ((- 1) * u) by RLVECT_1:16 ;
hence v,w,u are_LinDep ; :: thesis: verum

end;

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