let l1, l2 be Linear_Combination of BE; :: thesis: ( ( for a being Element of K st a in BE & b in BK holds
l1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l1 . a = 0. F ) & ( for a being Element of K st a in BE & b in BK holds
l2 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l2 . a = 0. F ) implies l1 = l2 )
assume that
A1: ( ( for a being Element of K st a in BE & b in BK holds
l1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l1 . a = 0. F ) ) and
A2: ( ( for a being Element of K st a in BE & b in BK holds
l2 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l2 . a = 0. F ) ) ; :: thesis: l1 = l2
A3: the carrier of (VecSp (E,F)) = the carrier of E by FIELD_4:def 6;
E is Subring of K by FIELD_4:def 1;
then A5: the carrier of E c= the carrier of K by C0SP1:def 3;

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

let o be object ; :: thesis: ( o in the carrier of (VecSp (E,F)) implies l1 . b₁ = l2 . b₁ )
assume A: o in the carrier of (VecSp (E,F)) ; :: thesis: l1 . b₁ = l2 . b₁

per cases ( ( o in BE & b in BK ) or not o in BE or not b in BK ) ;

suppose A7: ( o in BE & b in BK ) ; :: thesis: l1 . b₁ = l2 . b₁

reconsider a = o as Element of K by A, A3, A5;
l1 . a = l . (a * b) by A1, A7
.= l2 . a by A7, A2 ;
hence l1 . o = l2 . o ; :: thesis: verum

end;

suppose A7: ( not o in BE or not b in BK ) ; :: thesis: l1 . b₁ = l2 . b₁

reconsider a = o as Element of E by A, FIELD_4:def 6;
l1 . a = 0. F by A1, A7
.= l2 . a by A7, A2 ;
hence l1 . o = l2 . o ; :: thesis: verum

end;

end;

end;

hence l1 = l2 ; :: thesis: verum