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 ) )
A1: ( ((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 3;
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 3;
then (((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u) = (0. V) + (a2 * u) ;
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 3; :: thesis: verum
end;
assume A2: ( not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) ) ; :: thesis: ( a1 = a2 & b1 = b2 & c1 = c2 )
then A3: c1 - c2 = 0 by A1;
( a1 - a2 = 0 & b1 - b2 = 0 ) by A2, A1;
hence ( a1 = a2 & b1 = b2 & c1 = c2 ) by A3; :: thesis: verum