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 )
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
A2: ( not y is zero & u,v,y are_LinDep & u1,v1,y are_LinDep ) ;
A3: ( not u is zero & not v is zero & not are_Prop u,v ) by A1, Th2;
A4: ( not u1 is zero & not v1 is zero & not are_Prop u1,v1 ) by A1, Th2;
consider a, b being Real such that
A5: y = (a * u) + (b * v) by A2, A3, ANPROJ_1:11;
consider a1, b1 being Real such that
A6: y = (a1 * u1) + (b1 * v1) by A2, A4, ANPROJ_1:11;
0. V = ((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1)) by A5, A6, RLVECT_1:28
.= ((a * u) + (b * v)) + ((- 1) * ((a1 * u1) + (b1 * v1))) by RLVECT_1:29
.= ((a * u) + (b * v)) + (((- 1) * (a1 * u1)) + ((- 1) * (b1 * v1))) by RLVECT_1:def 9
.= ((a * u) + (b * v)) + ((((- 1) * a1) * u1) + ((- 1) * (b1 * v1))) by RLVECT_1:def 9
.= ((a * u) + (b * v)) + ((((- 1) * a1) * u1) + (((- 1) * b1) * v1)) by RLVECT_1:def 9
.= (((a * u) + (b * v)) + (((- 1) * a1) * u1)) + (((- 1) * b1) * v1) by RLVECT_1:def 6 ;
then ( a = 0 & b = 0 ) by A1;
then y = (0. V) + (0 * v) by A5, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A2, STRUCT_0:def 15; :: thesis: verum