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
for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y 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 for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y 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: for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )

then A2: not are_Prop u,v by Th2;
assume ex y being Element of V st
( not y is zero & u,v,y are_LinDep & u1,v1,y are_LinDep ) ; :: thesis: contradiction
then consider y being Element of V such that
A3: not y is zero and
A4: u,v,y are_LinDep and
A5: u1,v1,y are_LinDep ;
( not u is zero & not v is zero ) by ;
then consider a, b being Real such that
A6: y = (a * u) + (b * v) by ;
A7: not are_Prop u1,v1 by ;
( not u1 is zero & not v1 is zero ) by ;
then consider a1, b1 being Real such that
A8: y = (a1 * u1) + (b1 * v1) by ;
0. V = ((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1)) by
.= ((a * u) + (b * v)) + ((- 1) * ((a1 * u1) + (b1 * v1))) by RLVECT_1:16
.= ((a * u) + (b * v)) + (((- 1) * (a1 * u1)) + ((- 1) * (b1 * v1))) by RLVECT_1:def 5
.= ((a * u) + (b * v)) + ((((- 1) * a1) * u1) + ((- 1) * (b1 * v1))) by RLVECT_1:def 7
.= ((a * u) + (b * v)) + ((((- 1) * a1) * u1) + (((- 1) * b1) * v1)) by RLVECT_1:def 7
.= (((a * u) + (b * v)) + (((- 1) * a1) * u1)) + (((- 1) * b1) * v1) by RLVECT_1:def 3 ;
then ( a = 0 & b = 0 ) by A1;
then y = (0. V) + (0 * v) by
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A3; :: thesis: verum