let F be Field; :: thesis: for E1, E2 being FieldExtension of F st E1 == E2 holds
VecSp (E1,F) = VecSp (E2,F)
let E1, E2 be FieldExtension of F; :: thesis: ( E1 == E2 implies VecSp (E1,F) = VecSp (E2,F) )
set V1 = VecSp (E1,F);
set V2 = VecSp (E2,F);
assume AS: E1 == E2 ; :: thesis: VecSp (E1,F) = VecSp (E2,F)
A: the carrier of (VecSp (E1,F)) = the carrier of E2 by AS, FIELD_4:def 6
.= the carrier of (VecSp (E2,F)) by FIELD_4:def 6 ;
B: the addF of (VecSp (E1,F)) = the addF of E2 by AS, FIELD_4:def 6
.= the addF of (VecSp (E2,F)) by FIELD_4:def 6 ;
C: the ZeroF of (VecSp (E1,F)) = 0. E1 by FIELD_4:def 6
.= 0. E2 by AS
.= the ZeroF of (VecSp (E2,F)) by FIELD_4:def 6 ;
the lmult of (VecSp (E1,F)) = the multF of E2 | [: the carrier of F, the carrier of E2:] by AS, FIELD_4:def 6
.= the lmult of (VecSp (E2,F)) by FIELD_4:def 6 ;
hence VecSp (E1,F) = VecSp (E2,F) by A, B, C; :: thesis: verum