set A = DualSet L;

A2: for v, u being Vector of (DivisibleMod L) st v in DualSet L & u in DualSet L holds

v + u in DualSet L

for v being Vector of (DivisibleMod L) st v in DualSet L holds

a * v in DualSet L

A2: for v, u being Vector of (DivisibleMod L) st v in DualSet L & u in DualSet L holds

v + u in DualSet L

proof

for a being Element of INT.Ring
let v, u be Vector of (DivisibleMod L); :: thesis: ( v in DualSet L & u in DualSet L implies v + u in DualSet L )

assume B1: ( v in DualSet L & u in DualSet L ) ; :: thesis: v + u in DualSet L

consider v1 being Dual of L such that

B2: v1 = v by B1;

consider u1 being Dual of L such that

B3: u1 = u by B1;

v + u is Dual of L by B2, B3, LmDE1;

hence v + u in DualSet L ; :: thesis: verum

end;assume B1: ( v in DualSet L & u in DualSet L ) ; :: thesis: v + u in DualSet L

consider v1 being Dual of L such that

B2: v1 = v by B1;

consider u1 being Dual of L such that

B3: u1 = u by B1;

v + u is Dual of L by B2, B3, LmDE1;

hence v + u in DualSet L ; :: thesis: verum

for v being Vector of (DivisibleMod L) st v in DualSet L holds

a * v in DualSet L

proof

hence
DualSet L is linearly-closed
by A2, VECTSP_4:def 1; :: thesis: verum
let a be Element of INT.Ring; :: thesis: for v being Vector of (DivisibleMod L) st v in DualSet L holds

a * v in DualSet L

let v be Vector of (DivisibleMod L); :: thesis: ( v in DualSet L implies a * v in DualSet L )

assume B1: v in DualSet L ; :: thesis: a * v in DualSet L

consider v1 being Dual of L such that

B2: v1 = v by B1;

a * v is Dual of L by B2, LmDE2;

hence a * v in DualSet L ; :: thesis: verum

end;a * v in DualSet L

let v be Vector of (DivisibleMod L); :: thesis: ( v in DualSet L implies a * v in DualSet L )

assume B1: v in DualSet L ; :: thesis: a * v in DualSet L

consider v1 being Dual of L such that

B2: v1 = v by B1;

a * v is Dual of L by B2, LmDE2;

hence a * v in DualSet L ; :: thesis: verum