let V be RealLinearSpace; for u, v, w, u1, v1, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds
u1,v1,w1 are_LinDep
let u, v, w, u1, v1, w1 be Element of V; ( are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep implies u1,v1,w1 are_LinDep )
assume that
A1:
are_Prop u,u1
and
A2:
are_Prop v,v1
and
A3:
are_Prop w,w1
and
A4:
u,v,w are_LinDep
; u1,v1,w1 are_LinDep
consider b being Real such that
A5:
b <> 0
and
A6:
v = b * v1
by A2, Th1;
consider a being Real such that
A7:
a <> 0
and
A8:
u = a * u1
by A1, Th1;
consider d1, d2, d3 being Real such that
A9:
((d1 * u) + (d2 * v)) + (d3 * w) = 0. V
and
A10:
( d1 <> 0 or d2 <> 0 or d3 <> 0 )
by A4;
consider c being Real such that
A11:
c <> 0
and
A12:
w = c * w1
by A3, Th1;
A13:
( d1 * a <> 0 or d2 * b <> 0 or d3 * c <> 0 )
by A7, A5, A11, A10, XCMPLX_1:6;
0. V =
(((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1))
by A8, A6, A12, A9, RLVECT_1:def 7
.=
(((d1 * a) * u1) + ((d2 * b) * v1)) + (d3 * (c * w1))
by RLVECT_1:def 7
.=
(((d1 * a) * u1) + ((d2 * b) * v1)) + ((d3 * c) * w1)
by RLVECT_1:def 7
;
hence
u1,v1,w1 are_LinDep
by A13; verum