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
proof
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;
for a being Element of INT.Ring
for v being Vector of (DivisibleMod L) st v in DualSet L holds
a * v in DualSet L
proof
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;
hence DualSet L is linearly-closed by A2, VECTSP_4:def 1; :: thesis: verum