let F be Field; :: thesis: for E1 being FieldExtension of F
for E2 being b₁ -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 st ( for a being Element of E1 st a in F holds
h . a = a ) holds
h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))
let E1 be FieldExtension of F; :: thesis: for E2 being E1 -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 st ( for a being Element of E1 st a in F holds
h . a = a ) holds
h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))
let E2 be E1 -homomorphic FieldExtension of F; :: thesis: for h being Homomorphism of E1,E2 st ( for a being Element of E1 st a in F holds
h . a = a ) holds
h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))
let h be Homomorphism of E1,E2; :: thesis: ( ( for a being Element of E1 st a in F holds
h . a = a ) implies h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
assume AS: for a being Element of E1 st a in F holds
h . a = a ; :: thesis: h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))
H: dom h = the carrier of E1 by FUNCT_2:def 1
.= the carrier of (VecSp (E1,F)) by FIELD_4:def 6 ;
rng h c= the carrier of E2 ;
then rng h c= the carrier of (VecSp (E2,F)) by FIELD_4:def 6;
then reconsider f = h as Function of (VecSp (E1,F)),(VecSp (E2,F)) by H, FUNCT_2:2;

now :: thesis: for x, y being Element of (VecSp (E1,F)) holds f . (x + y) = (f . x) + (f . y)

let x, y be Element of (VecSp (E1,F)); :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider a = x, b = y as Element of E1 by FIELD_4:def 6;
x + y = a + b by FIELD_4:def 6;
hence f . (x + y) = (h . a) + (h . b) by VECTSP_1:def 20
.= (f . x) + (f . y) by FIELD_4:def 6 ;
:: thesis: verum

end;

then A: f is additive ;

now :: thesis: for a being Scalar of F
for x being Vector of (VecSp (E1,F)) holds f . (a * x) = a * (f . x)

let a be Scalar of F; :: thesis: for x being Vector of (VecSp (E1,F)) holds f . (a * x) = a * (f . x)
let x be Vector of (VecSp (E1,F)); :: thesis: f . (a * x) = a * (f . x)
reconsider v = x as Element of E1 by FIELD_4:def 6;
F is Subring of E1 by FIELD_4:def 1;
then the carrier of F c= the carrier of E1 by C0SP1:def 3;
then reconsider u1 = a as Element of E1 ;
F is Subring of E2 by FIELD_4:def 1;
then the carrier of F c= the carrier of E2 by C0SP1:def 3;
then reconsider u2 = a as Element of E2 ;
I: [u1,v] in [: the carrier of F, the carrier of E1:] by ZFMISC_1:def 2;
H: a * x = ( the multF of E1 | [: the carrier of F, the carrier of E1:]) . (u1,v) by FIELD_4:def 6
.= u1 * v by I, FUNCT_1:49 ;
J: [u2,(h . v)] in [: the carrier of F, the carrier of E2:] by ZFMISC_1:def 2;
K: a in F ;
thus f . (a * x) = (h . u1) * (h . v) by H, GROUP_6:def 6
.= u2 * (h . v) by AS, K
.= ( the multF of E2 | [: the carrier of F, the carrier of E2:]) . (u2,(h . v)) by J, FUNCT_1:49
.= a * (f . x) by FIELD_4:def 6 ; :: thesis: verum

end;

hence h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) by A, MOD_2:def 2; :: thesis: verum