let V be non trivial RealLinearSpace; :: thesis: ( ex y, u, v, w being Element of V st

for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies V is up-3-dimensional )

given y, u, v, w being Element of V such that A1: for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ; :: thesis: V is up-3-dimensional

take y ; :: according to ANPROJ_2:def 6 :: thesis: ex v, w1 being Element of V st

for a, b, c being Real st ((a * y) + (b * v)) + (c * w1) = 0. V holds

( a = 0 & b = 0 & c = 0 )

take u ; :: thesis: ex w1 being Element of V st

for a, b, c being Real st ((a * y) + (b * u)) + (c * w1) = 0. V holds

( a = 0 & b = 0 & c = 0 )

take v ; :: thesis: for a, b, c being Real st ((a * y) + (b * u)) + (c * v) = 0. V holds

( a = 0 & b = 0 & c = 0 )

let a, b, a1 be Real; :: thesis: ( ((a * y) + (b * u)) + (a1 * v) = 0. V implies ( a = 0 & b = 0 & a1 = 0 ) )

assume ((a * y) + (b * u)) + (a1 * v) = 0. V ; :: thesis: ( a = 0 & b = 0 & a1 = 0 )

then 0. V = (((a * y) + (b * u)) + (a1 * v)) + (0. V) by RLVECT_1:4

.= (((a * y) + (b * u)) + (a1 * v)) + (0 * w) by RLVECT_1:10 ;

hence ( a = 0 & b = 0 & a1 = 0 ) by A1; :: thesis: verum

for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies V is up-3-dimensional )

given y, u, v, w being Element of V such that A1: for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds

( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ; :: thesis: V is up-3-dimensional

take y ; :: according to ANPROJ_2:def 6 :: thesis: ex v, w1 being Element of V st

for a, b, c being Real st ((a * y) + (b * v)) + (c * w1) = 0. V holds

( a = 0 & b = 0 & c = 0 )

take u ; :: thesis: ex w1 being Element of V st

for a, b, c being Real st ((a * y) + (b * u)) + (c * w1) = 0. V holds

( a = 0 & b = 0 & c = 0 )

take v ; :: thesis: for a, b, c being Real st ((a * y) + (b * u)) + (c * v) = 0. V holds

( a = 0 & b = 0 & c = 0 )

let a, b, a1 be Real; :: thesis: ( ((a * y) + (b * u)) + (a1 * v) = 0. V implies ( a = 0 & b = 0 & a1 = 0 ) )

assume ((a * y) + (b * u)) + (a1 * v) = 0. V ; :: thesis: ( a = 0 & b = 0 & a1 = 0 )

then 0. V = (((a * y) + (b * u)) + (a1 * v)) + (0. V) by RLVECT_1:4

.= (((a * y) + (b * u)) + (a1 * v)) + (0 * w) by RLVECT_1:10 ;

hence ( a = 0 & b = 0 & a1 = 0 ) by A1; :: thesis: verum