let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
let V be VectSp of F; :: thesis: for l being Linear_Combination of V holds l = l ! (Carrier l)
let l be Linear_Combination of V; :: thesis: l = l ! (Carrier l)
set f = l | (Carrier l);
set g = (V \ (Carrier l)) --> (0. F);
set m = (l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F));
A2: dom l = [#] V by FUNCT_2:92;
then dom (l | (Carrier l)) = Carrier l by RELAT_1:62;
then A3: (dom (l | (Carrier l))) \/ (dom ((V \ (Carrier l)) --> (0. F))) = [#] V by XBOOLE_1:45;
A4: for x being object st x in dom l holds
l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

proof

let x be object ; :: thesis: ( x in dom l implies l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x )
assume x in dom l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then reconsider x = x as Element of V ;

per cases ( x in Carrier l or not x in Carrier l ) ;

suppose A5: x in Carrier l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

then not x in dom ((V \ (Carrier l)) --> (0. F)) by XBOOLE_0:def 5;
then ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = (l | (Carrier l)) . x by A3, FUNCT_4:def 1;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A5, FUNCT_1:49; :: thesis: verum

end;

suppose A6: not x in Carrier l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

then x in V \ (Carrier l) by XBOOLE_0:def 5;
then ( ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = ((V \ (Carrier l)) --> (0. F)) . x & ((V \ (Carrier l)) --> (0. F)) . x = 0. F ) by A3, FUNCOP_1:7, FUNCT_4:def 1;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A6; :: thesis: verum

end;

end;

end;

dom l = dom ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) by A2, A3, FUNCT_4:def 1;
hence l = l ! (Carrier l) by A4; :: thesis: verum