theorem sp2: :: FIELD_7:18

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for BE being finite Subset of (VecSp (K,E))
for BF being finite Subset of (VecSp (K,F))
for l1 being Linear_Combination of BF
for l2 being Linear_Combination of BE st l1 = l2 & BF c= BE holds
Sum l1 = Sum l2