let l1, l2 be Linear_Combination of BK; :: thesis: ( ( for b being Element of K st b in BK holds
l1 . b = Sum (down (l,b)) ) & ( for b being Element of K st b in BK holds
l2 . b = Sum (down (l,b)) ) implies l1 = l2 )
assume that
A1: for b being Element of K st b in BK holds
l1 . b = Sum (down (l,b)) and
A2: for b being Element of K st b in BK holds
l2 . b = Sum (down (l,b)) ; :: thesis: l1 = l2
A6: ( Carrier l1 c= BK & Carrier l2 c= BK ) by VECTSP_6:def 4;

now :: thesis: for o being object st o in the carrier of (VecSp (K,E)) holds
l1 . o = l2 . o

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,E)) implies l1 . b₁ = l2 . b₁ )
assume A: o in the carrier of (VecSp (K,E)) ; :: thesis: l1 . b₁ = l2 . b₁
then reconsider b = o as Element of K by FIELD_4:def 6;
reconsider bV = o as Element of (VecSp (K,E)) by A;

per cases ( b in BK or not b in BK ) ;

suppose A7: b in BK ; :: thesis: l1 . b₁ = l2 . b₁

then l1 . b = Sum (down (l,b)) by A1
.= l2 . b by A7, A2 ;
hence l1 . o = l2 . o ; :: thesis: verum

end;

suppose A7: not b in BK ; :: thesis: l1 . b₁ = l2 . b₁

then l1 . bV = 0. E by A6, VECTSP_6:2
.= l2 . bV by A6, A7, VECTSP_6:2 ;
hence l1 . o = l2 . o ; :: thesis: verum

end;

end;

end;

hence l1 = l2 ; :: thesis: verum