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

now :: thesis: for o being object st o in the carrier of (VecSp (K,F)) holds
f1 . o = f2 . o

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,F)) implies f1 . b₁ = f2 . b₁ )
assume A: o in the carrier of (VecSp (K,F)) ; :: thesis: f1 . b₁ = f2 . b₁
then reconsider c = o as Element of K by FIELD_4:def 6;
reconsider cV = o as Element of (VecSp (K,F)) by A;

per cases ( c in Base (BE,BK) or not c in Base (BE,BK) ) ;

suppose B0: c in Base (BE,BK) ; :: thesis: f1 . b₁ = f2 . b₁

then consider a, b being Element of K such that
B1: ( c = a * b & a in BE & b in BK ) ;
consider f1l2 being Linear_Combination of BE such that
B2: ( Sum f1l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
f1 . (a * b) = f1l2 . a ) ) by B1, A1;
consider f2l2 being Linear_Combination of BE such that
B3: ( Sum f2l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
f2 . (a * b) = f2l2 . a ) ) by B1, A2;
f1l2 = f2l2 by B2, B3, ZMODUL033;
then f1 . (a * b) = f2l2 . a by B0, B1, B2
.= f2 . (a * b) by B0, B1, B3 ;
hence f1 . o = f2 . o by B1; :: thesis: verum

end;

suppose A7: not c in Base (BE,BK) ; :: thesis: f1 . b₁ = f2 . b₁

then f1 . cV = 0. F by A6, VECTSP_6:2
.= f2 . cV by A6, A7, VECTSP_6:2 ;
hence f1 . o = f2 . o ; :: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum