let F be Field; :: thesis: for V being VectSp of F
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let V be VectSp of F; :: thesis: for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let A, B be Subset of V; :: thesis: for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let l be Linear_Combination of B; :: thesis: ( A c= B implies l = (l ! A) + (l ! (B \ A)) )
assume A1: A c= B ; :: thesis: l = (l ! A) + (l ! (B \ A))
set r = (l ! A) + (l ! (B \ A));
let v be Element of V; :: according to FUNCT_2:def 8 :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
A2: ( not v in B or v in A or v in B \ A )

proof

assume A3: v in B ; :: thesis: ( v in A or v in B \ A )
B = A \/ (B \ A) by A1, XBOOLE_1:45;
hence ( v in A or v in B \ A ) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

per cases ( v in A or v in B \ A or not v in B ) by A2;

suppose A4: v in A ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v

then not v in B \ A by XBOOLE_0:def 5;
then A5: (l ! (B \ A)) . v = 0. F by Th26;
(l ! A) . v = l . v by A4, Th25;
then ((l ! A) + (l ! (B \ A))) . v = (l . v) + (0. F) by A5, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; :: thesis: verum

end;

suppose A6: v in B \ A ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v

then not v in A by XBOOLE_0:def 5;
then A7: (l ! A) . v = 0. F by Th26;
(l ! (B \ A)) . v = l . v by A6, Th25;
then ((l ! A) + (l ! (B \ A))) . v = (0. F) + (l . v) by A7, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; :: thesis: verum

end;

suppose A8: not v in B ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v

Carrier l c= B by VECTSP_6:def 4;
then A9: not v in Carrier l by A8;
not v in B \ A by A8, XBOOLE_0:def 5;
then A10: (l ! (B \ A)) . v = 0. F by Th26;
not v in A by A1, A8;
then (l ! A) . v = 0. F by Th26;
then ((l ! A) + (l ! (B \ A))) . v = (0. F) + (0. F) by A10, VECTSP_6:22
.= 0. F by RLVECT_1:4 ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v by A9; :: thesis: verum

end;

end;