let g1, g2 be Linear_Combination of B; :: thesis: ( ( for u being Element of U st u in B holds
g1 . u = l . (f . u) ) & ( for u being Element of U st u in B holds
g2 . u = l . (f . u) ) implies g1 = g2 )
assume that
A18: for u being Element of U st u in B holds
g1 . u = l . (f . u) and
A19: for u being Element of U st u in B holds
g2 . u = l . (f . u) ; :: thesis: g1 = g2
A20: for x being object st x in dom g1 holds
g1 . x = g2 . x

proof

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then reconsider x = x as Element of U ;
H: ( Carrier g1 c= B & Carrier g2 c= B ) by VECTSP_6:def 4;

per cases ( x in B or not x in B ) ;

suppose J: x in B ; :: thesis: g1 . x = g2 . x

then g1 . x = l . (f . x) by A18;
hence g1 . x = g2 . x by J, A19; :: thesis: verum

end;

suppose A21: not x in B ; :: thesis: g1 . x = g2 . x

then g1 . x = 0. F by H, VECTSP_6:2
.= g2 . x by A21, H, VECTSP_6:2 ;
hence g1 . x = g2 . x ; :: thesis: verum

end;

end;

end;

( dom g1 = [#] U & dom g2 = [#] U ) by FUNCT_2:92;
hence g1 = g2 by A20; :: thesis: verum