set A = DualSet L;
A2: for v, u being Vector of () st v in DualSet L & u in DualSet L holds
v + u in DualSet L
proof
let v, u be Vector of (); :: 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 ;
hence v + u in DualSet L ; :: thesis: verum
end;
for a being Element of INT.Ring
for v being Vector of () 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 () st v in DualSet L holds
a * v in DualSet L

let v be Vector of (); :: 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 ;
hence a * v in DualSet L ; :: thesis: verum
end;
hence DualSet L is linearly-closed by ; :: thesis: verum