set X = { l where l is Linear_Combination of A : verum } ;
{ l where l is Linear_Combination of A : verum } c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Linear_Combination of A : verum } or x in the carrier of () )
assume x in { l where l is Linear_Combination of A : verum } ; :: thesis: x in the carrier of ()
then ex l being Linear_Combination of A st x = l ;
hence x in the carrier of () by Def29; :: thesis: verum
end;
then reconsider X = { l where l is Linear_Combination of A : verum } as Subset of () ;
A1: X is linearly-closed
proof
thus for v, u being Vector of () st v in X & u in X holds
v + u in X :: according to VECTSP_4:def 1 :: thesis: for b1 being Element of the carrier of R
for b2 being Element of the carrier of () holds
( not b2 in X or b1 * b2 in X )
proof
let v, u be Vector of (); :: thesis: ( v in X & u in X implies v + u in X )
assume that
A2: v in X and
A3: u in X ; :: thesis: v + u in X
consider l1 being Linear_Combination of A such that
A4: v = l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = l2 by A3;
A6: u = vector ((),l2) by ;
v = vector ((),l1) by ;
then v + u = l1 + l2 by ;
then v + u is Linear_Combination of A by Th27;
hence v + u in X ; :: thesis: verum
end;
let a be Element of R; :: thesis: for b1 being Element of the carrier of () holds
( not b1 in X or a * b1 in X )

let v be Vector of (); :: thesis: ( not v in X or a * v in X )
assume v in X ; :: thesis: a * v in X
then consider l being Linear_Combination of A such that
A7: v = l ;
a * v = a * (vector ((),l)) by
.= a * l by Th48 ;
then a * v is Linear_Combination of A by Th31;
hence a * v in X ; :: thesis: verum
end;
ZeroLC V is Linear_Combination of A by Th11;
then ZeroLC V in X ;
hence ex b1 being strict Submodule of LC_Z_Module V st the carrier of b1 = { l where l is Linear_Combination of A : verum } by ; :: thesis: verum