let V be RealLinearSpace; :: thesis: for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds
( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )
let u, v, u1, v1 be Element of V; :: thesis: ( ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) implies ( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep ) )
assume A1: for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ; :: thesis: ( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )

A2: now

let d1, d2, d3 be Real; :: thesis: ( ((d1 * u) + (d2 * v)) + (d3 * u1) = 0. V implies ( d1 = 0 & d2 = 0 & d3 = 0 ) )
assume ((d1 * u) + (d2 * v)) + (d3 * u1) = 0. V ; :: thesis: ( d1 = 0 & d2 = 0 & d3 = 0 )
then 0. V = (((d1 * u) + (d2 * v)) + (d3 * u1)) + (0. V) by RLVECT_1:10
.= (((d1 * u) + (d2 * v)) + (d3 * u1)) + (0 * v1) by RLVECT_1:23 ;
hence ( d1 = 0 & d2 = 0 & d3 = 0 ) by A1; :: thesis: verum

end;

now

let d1, d2, d3 be Real; :: thesis: ( ((d1 * u1) + (d2 * v1)) + (d3 * u) = 0. V implies ( d1 = 0 & d2 = 0 & d3 = 0 ) )
assume ((d1 * u1) + (d2 * v1)) + (d3 * u) = 0. V ; :: thesis: ( d1 = 0 & d2 = 0 & d3 = 0 )
then 0. V = ((d3 * u) + (d1 * u1)) + (d2 * v1) by RLVECT_1:def 6
.= (((d3 * u) + (0. V)) + (d1 * u1)) + (d2 * v1) by RLVECT_1:10
.= (((d3 * u) + (0 * v)) + (d1 * u1)) + (d2 * v1) by RLVECT_1:23 ;
hence ( d1 = 0 & d2 = 0 & d3 = 0 ) by A1; :: thesis: verum

end;

hence ( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep ) by A2, Th1; :: thesis: verum