:: deftheorem defines Base FIELD_7:def 7 :
for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Subset of (VecSp (E,F))
for BK being Subset of (VecSp (K,E)) holds Base (BE,BK) = { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ;