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