consider V being strict RealLinearSpace such that

A1: ex u, v being Element of V st

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

( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;

consider u, v being Element of V such that

A2: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) and

for w being Element of V ex a, b being Real st w = (a * u) + (b * v) by A1;

u <> 0. V

hence ex b_{1} being RealLinearSpace st

( b_{1} is strict & not b_{1} is trivial )
; :: thesis: verum

A1: ex u, v being Element of V st

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

( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;

consider u, v being Element of V such that

A2: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) and

for w being Element of V ex a, b being Real st w = (a * u) + (b * v) by A1;

u <> 0. V

proof

then
not V is trivial
;
assume A3:
u = 0. V
; :: thesis: contradiction

0. V = (0. V) + (0. V)

.= (1 * u) + (0. V) by A3

.= (1 * u) + (0 * v) by RLVECT_1:10 ;

hence contradiction by A2; :: thesis: verum

end;0. V = (0. V) + (0. V)

.= (1 * u) + (0. V) by A3

.= (1 * u) + (0 * v) by RLVECT_1:10 ;

hence contradiction by A2; :: thesis: verum

hence ex b

( b