let K be Ring; :: thesis: for V being LeftMod of K
for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
let V be LeftMod of K; :: thesis: for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
let A, A1, A2 be Subset of V; :: thesis: ( A is base & A = A1 \/ A2 & A1 misses A2 implies V is_the_direct_sum_of Lin A1, Lin A2 )
assume A1: ( A is base & A = A1 \/ A2 & A1 misses A2 ) ; :: thesis: V is_the_direct_sum_of Lin A1, Lin A2
set W = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #);
A2: ( A is linearly-independent & Lin A = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) ) by A1, MOD_3:def 2;
then A3: VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = (Lin A1) + (Lin A2) by A1, MOD_3:19;
(Lin A1) /\ (Lin A2) = (0). V by A1, A2, Th5;
hence V is_the_direct_sum_of Lin A1, Lin A2 by A3, VECTSP_5:def 4; :: thesis: verum