let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: u1,v1,w1 are_LinDep
consider b being Real such that
A5: b <> 0 and
A6: v = b * v1 by ;
consider a being Real such that
A7: a <> 0 and
A8: u = a * u1 by ;
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 ;
A13: ( d1 * a <> 0 or d2 * b <> 0 or d3 * c <> 0 ) by ;
0. V = (((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1)) by
.= (((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; :: thesis: verum