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:37;
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 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) ) by A1;
u <> 0. V

proof

assume A3: u = 0. V ; :: thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:10
.= (1 * u) + (0. V) by A3, RLVECT_1:def 9
.= (1 * u) + (0 * v) by RLVECT_1:23 ;
hence contradiction by A2; :: thesis: verum

end;

then not V is trivial by STRUCT_0:def 19;
hence ex b₁ being RealLinearSpace st
( b₁ is strict & not b₁ is trivial ) ; :: thesis: verum