let K be Ring; :: thesis: for V being LeftMod of K holds
( SubJoin V is commutative & SubJoin V is associative & SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )
let V be LeftMod of K; :: thesis: ( SubJoin V is commutative & SubJoin V is associative & SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )
set S0 = Submodules V;
set S1 = SubJoin V;
reconsider L = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) as Lattice by VECTSP_5:57;
SubJoin V = the L_join of L ;
hence ( SubJoin V is commutative & SubJoin V is associative ) ; :: thesis: ( SubJoin V is having_a_unity & (0). V = the_unity_wrt (SubJoin V) )
set e = (0). V;
reconsider e9 = @ ((0). V) as Element of Submodules V ;
A1: e9 = (0). V by LMOD_6:def 2;

now :: thesis: for a9 being Element of Submodules V holds
( (SubJoin V) . (e9,a9) = a9 & (SubJoin V) . (a9,e9) = a9 )

let a9 be Element of Submodules V; :: thesis: ( (SubJoin V) . (e9,a9) = a9 & (SubJoin V) . (a9,e9) = a9 )
reconsider b = a9 as Element of Submodules V ;
reconsider a = b as strict Subspace of V ;
thus (SubJoin V) . (e9,a9) = ((0). V) + a by A1, VECTSP_5:def 7
.= a9 by VECTSP_5:9 ; :: thesis: (SubJoin V) . (a9,e9) = a9
thus (SubJoin V) . (a9,e9) = a + ((0). V) by A1, VECTSP_5:def 7
.= a9 by VECTSP_5:9 ; :: thesis: verum

end;

then A2: e9 is_a_unity_wrt SubJoin V by BINOP_1:3;
hence SubJoin V is having_a_unity by SETWISEO:def 2; :: thesis: (0). V = the_unity_wrt (SubJoin V)
thus (0). V = the_unity_wrt (SubJoin V) by A1, A2, BINOP_1:def 8; :: thesis: verum