set X = the Basis of V;
X1: ( the Basis of V is linearly-independent & Lin the Basis of V = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;
the Basis of V <> {}
proof
assume the Basis of V = {} ; :: thesis: contradiction
then the Basis of V = {} the carrier of V ;
then X3: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V by X1, ZMODUL02:67;
for x, y being object st x in the carrier of V & y in the carrier of V holds
x = y
proof
let x, y be object ; :: thesis: ( x in the carrier of V & y in the carrier of V implies x = y )
assume ( x in the carrier of V & y in the carrier of V ) ; :: thesis: x = y
then reconsider x1 = x, y1 = y as Vector of V ;
( x1 in (0). V & y1 in (0). V ) by X3;
then ( x1 = 0. V & y1 = 0. V ) by ZMODUL02:66;
hence x = y ; :: thesis: verum
end;
then V is trivial ;
hence contradiction ; :: thesis: verum
end;
then consider v being object such that
X2: v in the Basis of V by XBOOLE_0:def 1;
reconsider v = v as Vector of V by X2;
X20: v <> 0. V by X2, ZMODUL02:57, VECTSP_7:def 3;
reconsider f = Coordinate (v, the Basis of V) as Function of V,INT.Ring ;
DM1: dom f = the carrier of V by FUNCT_2:def 1;
J1: f . (0. V) = 0 by PROJ4;
A16: f . v = 1 by X2, X20, PROJ5;
take f ; :: thesis: ( f is additive & f is homogeneous & not f is constant & not f is trivial )
thus ( f is additive & f is homogeneous & not f is constant & not f is trivial ) by A16, DM1, J1, defCoord; :: thesis: verum