theorem str12: :: FIELD_7:4

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
VecSp (E1,F) = VecSp (E2,F)