set X = { l where l is Linear_Combination of A : verum } ;

{ l where l is Linear_Combination of A : verum } c= the carrier of (LC_Z_Module V)

A1: X is linearly-closed

then ZeroLC V in X ;

hence ex b_{1} being strict Submodule of LC_Z_Module V st the carrier of b_{1} = { l where l is Linear_Combination of A : verum }
by A1, ZMODUL01:50; :: thesis: verum

{ l where l is Linear_Combination of A : verum } c= the carrier of (LC_Z_Module V)

proof

then reconsider X = { l where l is Linear_Combination of A : verum } as Subset of (LC_Z_Module V) ;
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 (LC_Z_Module V) )

assume x in { l where l is Linear_Combination of A : verum } ; :: thesis: x in the carrier of (LC_Z_Module V)

then ex l being Linear_Combination of A st x = l ;

hence x in the carrier of (LC_Z_Module V) by Def29; :: thesis: verum

end;assume x in { l where l is Linear_Combination of A : verum } ; :: thesis: x in the carrier of (LC_Z_Module V)

then ex l being Linear_Combination of A st x = l ;

hence x in the carrier of (LC_Z_Module V) by Def29; :: thesis: verum

A1: X is linearly-closed

proof

ZeroLC V is Linear_Combination of A
by Th11;
thus
for v, u being Vector of (LC_Z_Module V) st v in X & u in X holds

v + u in X :: according to VECTSP_4:def 1 :: thesis: for b_{1} being Element of the carrier of R

for b_{2} being Element of the carrier of (LC_Z_Module V) holds

( not b_{2} in X or b_{1} * b_{2} in X )_{1} being Element of the carrier of (LC_Z_Module V) holds

( not b_{1} in X or a * b_{1} in X )

let v be Vector of (LC_Z_Module V); :: 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 ((LC_Z_Module V),l)) by A7, RLVECT_2:def 1, RLVECT_1:1

.= a * l by Th48 ;

then a * v is Linear_Combination of A by Th31;

hence a * v in X ; :: thesis: verum

end;v + u in X :: according to VECTSP_4:def 1 :: thesis: for b

for b

( not b

proof

let a be Element of R; :: thesis: for b
let v, u be Vector of (LC_Z_Module V); :: 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 ((LC_Z_Module V),l2) by A5, RLVECT_2:def 1, RLVECT_1:1;

v = vector ((LC_Z_Module V),l1) by A4, RLVECT_2:def 1, RLVECT_1:1;

then v + u = l1 + l2 by A6, Th47;

then v + u is Linear_Combination of A by Th27;

hence v + u in X ; :: thesis: verum

end;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 ((LC_Z_Module V),l2) by A5, RLVECT_2:def 1, RLVECT_1:1;

v = vector ((LC_Z_Module V),l1) by A4, RLVECT_2:def 1, RLVECT_1:1;

then v + u = l1 + l2 by A6, Th47;

then v + u is Linear_Combination of A by Th27;

hence v + u in X ; :: thesis: verum

( not b

let v be Vector of (LC_Z_Module V); :: 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 ((LC_Z_Module V),l)) by A7, RLVECT_2:def 1, RLVECT_1:1

.= a * l by Th48 ;

then a * v is Linear_Combination of A by Th31;

hence a * v in X ; :: thesis: verum

then ZeroLC V in X ;

hence ex b