let V be free Z_Module; :: thesis: for I being Basis of V
for v being Vector of V st v in I holds
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let I be Basis of V; :: thesis: for v being Vector of V st v in I holds
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let v be Vector of V; :: thesis: ( v in I implies V is_the_direct_sum_of Lin (I \ {v}), Lin {v} )
assume A1: v in I ; :: thesis: V is_the_direct_sum_of Lin (I \ {v}), Lin {v}
I = (I \ {v}) \/ {v} by ;
then Lin I = (Lin (I \ {v})) + () by ZMODUL02:72;
then A3: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (Lin (I \ {v})) + () by VECTSP_7:def 3;
the carrier of (Lin (I \ {v})) /\ the carrier of () = {(0. V)}
proof
assume B1: the carrier of (Lin (I \ {v})) /\ the carrier of () <> {(0. V)} ; :: thesis: contradiction
0. V in (Lin (I \ {v})) /\ () by ZMODUL01:33;
then 0. V in the carrier of (Lin (I \ {v})) /\ the carrier of () by VECTSP_5:def 2;
then {(0. V)} c< the carrier of (Lin (I \ {v})) /\ the carrier of () by ;
then consider x being object such that
B2: x in the carrier of (Lin (I \ {v})) /\ the carrier of () and
B3: not x in {(0. V)} by XBOOLE_0:6;
B4: x <> 0. V by ;
B5: x in (Lin (I \ {v})) /\ () by ;
then x in V by ZMODUL01:24;
then reconsider x = x as Vector of V ;
x in Lin (I \ {v}) by ;
then consider lx1 being Linear_Combination of I \ {v} such that
B6: x = Sum lx1 by ZMODUL02:64;
B7: Carrier lx1 <> {} by ;
B8: Carrier lx1 c= I \ {v} by VECTSP_6:def 4;
x in Lin {v} by ;
then consider lx2 being Linear_Combination of {v} such that
B9: - x = Sum lx2 by ;
B11: Carrier lx2 c= {v} by VECTSP_6:def 4;
reconsider llx1 = lx1 as Linear_Combination of I by ;
reconsider llx2 = lx2 as Linear_Combination of I by ;
Carrier lx1 misses Carrier lx2 by ;
then (Carrier lx1) /\ (Carrier lx2) = {} ;
then B12: Carrier (llx1 + llx2) = (Carrier llx1) \/ (Carrier llx2) by ThCarrier1;
B13: (Sum llx1) + (Sum llx2) = 0. V by ;
reconsider llx = llx1 + llx2 as Linear_Combination of I by ZMODUL02:27;
Sum llx = 0. V by ;
hence contradiction by B7, B12, VECTSP_7:def 1, VECTSP_7:def 3; :: thesis: verum
end;
then (Lin (I \ {v})) /\ () = (0). V by ;
hence V is_the_direct_sum_of Lin (I \ {v}), Lin {v} by ; :: thesis: verum