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
proof
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;
then not V is trivial ;
hence ex b1 being RealLinearSpace st
( b1 is strict & not b1 is trivial ) ; :: thesis: verum