let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is additive
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is additive
let f be Monomorphism of K,F; :: thesis: ( K,F are_disjoint implies emb_iso f is additive )
assume AS: K,F are_disjoint ; :: thesis: emb_iso f is additive
set g = emb_iso f;
set R = embField f;

now :: thesis: for a, b being Element of (embField f) holds (emb_iso f) . (a + b) = ((emb_iso f) . a) + ((emb_iso f) . b)

let a, b be Element of (embField f); :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)
reconsider x = a, y = b as Element of carr f by defemb;

per cases ( ( x in [#] K & y in [#] K ) or ( x in [#] K & not y in [#] K ) or ( y in [#] K & not x in [#] K ) or ( not x in [#] K & not y in [#] K & the addF of F . (x,y) in rng f ) or ( not x in [#] K & not y in [#] K & not the addF of F . (x,y) in rng f ) ) ;

suppose A: ( x in [#] K & y in [#] K ) ; :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of K ;
B: a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= a1 + b1 by defaddf ;
( a in K & b in K ) by A;
then C: ( (emb_iso f) . a = f . a & (emb_iso f) . b = f . b ) by defiso;
a + b in K by B;
hence (emb_iso f) . (a + b) = f . (a + b) by defiso
.= ((emb_iso f) . a) + ((emb_iso f) . b) by C, B, VECTSP_1:def 20 ;
:: thesis: verum

end;

suppose A: ( x in [#] K & not y in [#] K ) ; :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)

then reconsider a1 = a as Element of K ;
reconsider b1 = b as Element of F by A, Lm1;
reconsider fa = f . a1 as Element of F ;
B: a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= fa + b1 by A, defaddf ;
( a in K & not b in K ) by A;
then C: ( (emb_iso f) . a = f . a & (emb_iso f) . b = b ) by defiso;
not fa + b1 in K by AS, XBOOLE_0:def 4;
hence (emb_iso f) . (a + b) = ((emb_iso f) . a) + ((emb_iso f) . b) by C, B, defiso; :: thesis: verum

end;

suppose A: ( y in [#] K & not x in [#] K ) ; :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)

then reconsider b1 = b as Element of K ;
reconsider a1 = a as Element of F by A, Lm1;
reconsider fb = f . b1 as Element of F ;
B: a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= a1 + fb by A, defaddf ;
( not a in K & b in K ) by A;
then C: ( (emb_iso f) . a = a & (emb_iso f) . b = f . b ) by defiso;
not a1 + fb in K by AS, XBOOLE_0:def 4;
hence (emb_iso f) . (a + b) = ((emb_iso f) . a) + ((emb_iso f) . b) by C, B, defiso; :: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & the addF of F . (x,y) in rng f ) ; :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= (f ") . (a1 + b1) by A, defaddf ;
( not a in K & not b in K ) by A;
then D: ( (emb_iso f) . a = a & (emb_iso f) . b = b ) by defiso;
a1 + b1 in dom (f ") by A, FUNCT_1:33;
then (f ") . (a1 + b1) in rng (f ") by FUNCT_1:3;
then (f ") . (a1 + b1) in K ;
hence (emb_iso f) . (a + b) = f . ((f ") . (a1 + b1)) by C, defiso
.= ((emb_iso f) . a) + ((emb_iso f) . b) by D, A, FUNCT_1:35 ;
:: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & not the addF of F . (x,y) in rng f ) ; :: thesis: (emb_iso f) . (b₁ + b₂) = ((emb_iso f) . b₁) + ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= a1 + b1 by A, defaddf ;
( not a in K & not b in K ) by A;
then D: ( (emb_iso f) . a = a & (emb_iso f) . b = b ) by defiso;
not a1 + b1 in K by AS, XBOOLE_0:def 4;
hence (emb_iso f) . (a + b) = ((emb_iso f) . a) + ((emb_iso f) . b) by D, C, defiso; :: thesis: verum

end;

end;

end;

hence emb_iso f is additive ; :: thesis: verum