theorem :: FIELD_7:19

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = b2 )