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 A1, Th2;

then consider a, b being Real such that

A6: y = (a * u) + (b * v) by A4, A2, ANPROJ_1:6;

A7: not are_Prop u1,v1 by A1, Th2;

( not u1 is zero & not v1 is zero ) by A1, Th2;

then consider a1, b1 being Real such that

A8: y = (a1 * u1) + (b1 * v1) by A5, A7, ANPROJ_1:6;

0. V = ((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1)) by A6, A8, RLVECT_1:15

.= ((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 A6, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A3; :: thesis: verum

( 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 A1, Th2;

then consider a, b being Real such that

A6: y = (a * u) + (b * v) by A4, A2, ANPROJ_1:6;

A7: not are_Prop u1,v1 by A1, Th2;

( not u1 is zero & not v1 is zero ) by A1, Th2;

then consider a1, b1 being Real such that

A8: y = (a1 * u1) + (b1 * v1) by A5, A7, ANPROJ_1:6;

0. V = ((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1)) by A6, A8, RLVECT_1:15

.= ((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 A6, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A3; :: thesis: verum