let V be RealLinearSpace; :: thesis: for u, v, w being Element of V
for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )
let u, v, w be Element of V; :: thesis: for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )
let a1, b1, c1, a2, b2, c2 be Real; :: thesis: ( not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) implies ( a1 = a2 & b1 = b2 & c1 = c2 ) )
assume that
A1: not u,v,w are_LinDep and
A2: ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) ; :: thesis: ( a1 = a2 & b1 = b2 & c1 = c2 )
( ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) implies (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V )

proof

assume ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) ; :: thesis: (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V
then ((c1 - c2) * w) + ((a1 * u) + (b1 * v)) = (a2 * u) + (b2 * v) by Lm6;
then (((c1 - c2) * w) + (a1 * u)) + (b1 * v) = (a2 * u) + (b2 * v) by RLVECT_1:def 6;
then ((b1 - b2) * v) + (((c1 - c2) * w) + (a1 * u)) = a2 * u by Lm6;
then (((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u) = a2 * u by RLVECT_1:def 6;
then (((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u) = (0. V) + (a2 * u) by RLVECT_1:10;
then ((a1 - a2) * u) + (((b1 - b2) * v) + ((c1 - c2) * w)) = 0. V by Lm6;
hence (((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w) = 0. V by RLVECT_1:def 6; :: thesis: verum

end;

then ( a1 - a2 = 0 & b1 - b2 = 0 & c1 - c2 = 0 ) by A1, A2, Def3;
hence ( a1 = a2 & b1 = b2 & c1 = c2 ) ; :: thesis: verum