let F be Field; :: thesis: for E being FieldExtension of F

for K being b_{1} -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)

let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)

let K be E -extending FieldExtension of F; :: thesis: VecSp (E,F) is Subspace of VecSp (K,F)

set VK = VecSp (K,F);

set VE = VecSp (E,F);

H1: E is Subring of K by FIELD_4:def 1;

then H2: the carrier of E c= the carrier of K by C0SP1:def 3;

H3: ( the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,F)) = the carrier of K ) by FIELD_4:def 6;

F is Subring of E by FIELD_4:def 1;

then H4: the carrier of F c= the carrier of E by C0SP1:def 3;

B1: the carrier of (VecSp (E,F)) c= the carrier of (VecSp (K,F)) by H1, H3, C0SP1:def 3;

B2: 0. (VecSp (E,F)) = 0. E by FIELD_4:def 6

.= 0. K by H1, C0SP1:def 3

.= 0. (VecSp (K,F)) by FIELD_4:def 6 ;

B3: the addF of (VecSp (E,F)) = the addF of E by FIELD_4:def 6

.= the addF of K || the carrier of E by H1, C0SP1:def 3

.= the addF of (VecSp (K,F)) || the carrier of E by FIELD_4:def 6

.= the addF of (VecSp (K,F)) || the carrier of (VecSp (E,F)) by FIELD_4:def 6 ;

B4: the lmult of (VecSp (E,F)) = the multF of E | [: the carrier of F, the carrier of (VecSp (E,F)):] by H3, FIELD_4:def 6

.= ( the multF of K || the carrier of E) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H1, C0SP1:def 3

.= the multF of K | [: the carrier of F, the carrier of (VecSp (E,F)):] by H4, H3, ZFMISC_1:96, RELAT_1:74

.= ( the multF of K | [: the carrier of F, the carrier of K:]) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H2, H3, ZFMISC_1:96, RELAT_1:74

.= the lmult of (VecSp (K,F)) | [: the carrier of F, the carrier of (VecSp (E,F)):] by FIELD_4:def 6 ;

thus VecSp (E,F) is Subspace of VecSp (K,F) by B1, B2, B3, B4, VECTSP_4:def 2; :: thesis: verum

for K being b

let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)

let K be E -extending FieldExtension of F; :: thesis: VecSp (E,F) is Subspace of VecSp (K,F)

set VK = VecSp (K,F);

set VE = VecSp (E,F);

H1: E is Subring of K by FIELD_4:def 1;

then H2: the carrier of E c= the carrier of K by C0SP1:def 3;

H3: ( the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,F)) = the carrier of K ) by FIELD_4:def 6;

F is Subring of E by FIELD_4:def 1;

then H4: the carrier of F c= the carrier of E by C0SP1:def 3;

B1: the carrier of (VecSp (E,F)) c= the carrier of (VecSp (K,F)) by H1, H3, C0SP1:def 3;

B2: 0. (VecSp (E,F)) = 0. E by FIELD_4:def 6

.= 0. K by H1, C0SP1:def 3

.= 0. (VecSp (K,F)) by FIELD_4:def 6 ;

B3: the addF of (VecSp (E,F)) = the addF of E by FIELD_4:def 6

.= the addF of K || the carrier of E by H1, C0SP1:def 3

.= the addF of (VecSp (K,F)) || the carrier of E by FIELD_4:def 6

.= the addF of (VecSp (K,F)) || the carrier of (VecSp (E,F)) by FIELD_4:def 6 ;

B4: the lmult of (VecSp (E,F)) = the multF of E | [: the carrier of F, the carrier of (VecSp (E,F)):] by H3, FIELD_4:def 6

.= ( the multF of K || the carrier of E) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H1, C0SP1:def 3

.= the multF of K | [: the carrier of F, the carrier of (VecSp (E,F)):] by H4, H3, ZFMISC_1:96, RELAT_1:74

.= ( the multF of K | [: the carrier of F, the carrier of K:]) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H2, H3, ZFMISC_1:96, RELAT_1:74

.= the lmult of (VecSp (K,F)) | [: the carrier of F, the carrier of (VecSp (E,F)):] by FIELD_4:def 6 ;

thus VecSp (E,F) is Subspace of VecSp (K,F) by B1, B2, B3, B4, VECTSP_4:def 2; :: thesis: verum