field_2.miz



    begin

    reserve R for Ring,

S for R -monomorphic Ring,

K for Field,

F for K -monomorphic Field,

T for K -monomorphic comRing;

    definition

      let R, S;

      let f be Monomorphism of R, S;

      :: original: "

      redefine

      func f " -> Function of ( rng f), R ;

      coherence

      proof

        ( dom f) = ( [#] R) & ( rng f) c= ( [#] S) by FUNCT_2:def 1;

        then f is Function of ( [#] R), ( rng f) by FUNCT_2: 2;

        hence thesis by FUNCT_2: 25;

      end;

    end

    theorem :: FIELD_2:1

    

     Th1: for f be Monomorphism of R, S, a,b be Element of ( rng f) holds ((f " ) . (a + b)) = (((f " ) . a) + ((f " ) . b)) & ((f " ) . (a * b)) = (((f " ) . a) * ((f " ) . b))

    proof

      let f be Monomorphism of R, S, a,b be Element of ( rng f);

      consider x be object such that

       A1: x in ( [#] R) & (f . x) = a by FUNCT_2: 11;

      reconsider x as Element of R by A1;

      consider y be object such that

       A2: y in ( [#] R) & (f . y) = b by FUNCT_2: 11;

      reconsider y as Element of R by A2;

      

       A3: ( [#] R) = ( dom f) by FUNCT_2:def 1;

      then

       A4: ((f " ) . b) = y by A2, FUNCT_1: 34;

      

       A5: ( [#] R) = ( dom f) by FUNCT_2:def 1;

      (f . (x + y)) = (a + b) by A1, A2, VECTSP_1:def 20;

      

      hence ((f " ) . (a + b)) = (x + y) by A5, FUNCT_1: 34

      .= (((f " ) . a) + ((f " ) . b)) by A1, A3, A4, FUNCT_1: 34;

      (f . (x * y)) = (a * b) by A1, A2, GROUP_6:def 6;

      

      hence ((f " ) . (a * b)) = (x * y) by A5, FUNCT_1: 34

      .= (((f " ) . a) * ((f " ) . b)) by A1, A3, A4, FUNCT_1: 34;

    end;

    theorem :: FIELD_2:2

    

     Th2: for f be Monomorphism of R, S, a be Element of ( rng f) holds ((f " ) . a) = ( 0. R) iff a = ( 0. S)

    proof

      let f be Monomorphism of R, S, a be Element of ( rng f);

       A1:

      now

        assume ((f " ) . a) = ( 0. R);

        then (f . ( 0. R)) = a by FUNCT_1: 35;

        hence a = ( 0. S) by RING_2: 6;

      end;

      

       A2: ( dom f) = ( [#] R) by FUNCT_2:def 1;

      now

        assume a = ( 0. S);

        then (f . ( 0. R)) = a by RING_2: 6;

        hence ((f " ) . a) = ( 0. R) by A2, FUNCT_1: 34;

      end;

      hence thesis by A1;

    end;

    theorem :: FIELD_2:3

    

     Th3: for f be Monomorphism of R, S holds ((f " ) . ( 1. S)) = ( 1. R) & ((f " ) . ( 0. S)) = ( 0. R)

    proof

      let f be Monomorphism of R, S;

      

       A1: ( [#] R) = ( dom f) by FUNCT_2:def 1;

      (f . ( 1_ R)) = ( 1_ S) by GROUP_1:def 13;

      hence ((f " ) . ( 1. S)) = ( 1. R) by A1, FUNCT_1: 34;

      (f . ( 0. R)) = ( 0. S) by RING_2: 6;

      then

      reconsider o = ( 0. S) as Element of ( rng f) by FUNCT_2: 4;

      ((f " ) . ( 0. S)) = ((f " ) . (o + o)) = (((f " ) . o) + ((f " ) . o)) by Th1;

      hence thesis by RLVECT_1: 9;

    end;

    theorem :: FIELD_2:4

    for f be Monomorphism of R, S holds (f " ) is one-to-one onto

    proof

      let f be Monomorphism of R, S;

      ( rng (f " )) = ( dom f) by FUNCT_1: 33

      .= ( [#] R) by FUNCT_2:def 1;

      hence thesis;

    end;

    theorem :: FIELD_2:5

    

     Th4: for f be Monomorphism of R, S, a be Element of R holds (f . a) = ( 0. S) iff a = ( 0. R)

    proof

      let f be Monomorphism of R, S, a be Element of R;

      now

        assume (f . a) = ( 0. S);

        then (f . a) = (f . ( 0. R)) by RING_2: 6;

        hence a = ( 0. R) by FUNCT_2: 19;

      end;

      hence thesis by RING_2: 6;

    end;

    theorem :: FIELD_2:6

    

     Th5: for f be Monomorphism of K, F, a be Element of K st a <> ( 0. K) holds (f . (a " )) = ((f . a) " )

    proof

      let f be Monomorphism of K, F, x be Element of K;

      assume

       AS: x <> ( 0. K);

      

       A1: ((f . (x " )) * (f . x)) = (f . ((x " ) * x)) by GROUP_6:def 6

      .= (f . ( 1_ K)) by AS, VECTSP_1:def 10

      .= ( 1_ F) by GROUP_1:def 13

      .= ( 1. F);

      (f . x) <> ( 0. F) by AS, Th4;

      hence thesis by A1, VECTSP_1:def 10;

    end;

    notation

      let R,S be Ring;

      synonym R,S are_disjoint for R misses S;

    end

    definition

      let R,S be Ring;

      :: original: are_disjoint

      redefine

      :: FIELD_2:def1

      pred R,S are_disjoint means (( [#] R) /\ ( [#] S)) = {} ;

      compatibility by TSEP_1:def 3, XBOOLE_0:def 7;

    end

    definition

      let R, S;

      let f be Monomorphism of R, S;

      :: FIELD_2:def2

      func carr f -> non empty set equals ((( [#] S) \ ( rng f)) \/ ( [#] R));

      coherence ;

    end

    

     Lm1: for f be Monomorphism of R, S, a be Element of ( carr f) st not a in ( [#] R) holds a in ( [#] S) & not a in ( rng f)

    proof

      let f be Monomorphism of R, S, a be Element of ( carr f);

      assume not a in ( [#] R);

      then a in (( [#] S) \ ( rng f)) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 5;

    end;

    

     Lm2: for f be Monomorphism of R, S, a,b be Element of ( carr f) st not a in ( [#] R) & b in ( [#] R) holds (the addF of S . (a,(f . b))) in (( [#] S) \ ( rng f))

    proof

      let f be Monomorphism of R, S, a,b be Element of ( carr f);

      assume

       A1: not a in ( [#] R) & b in ( [#] R);

      then

      reconsider y = b as Element of ( [#] R);

      

       A2: a in (( [#] S) \ ( rng f)) by A1, XBOOLE_0:def 3;

      then

       A3: a in ( [#] S) & not a in ( rng f) by XBOOLE_0:def 5;

      reconsider x = a as Element of ( [#] S) by A2;

      reconsider fy = (f . y) as Element of ( [#] S);

      now

        assume (the addF of S . (x,(f . y))) in ( rng f);

        then

        consider c be object such that

         A4: c in ( dom f) & (f . c) = (the addF of S . (x,(f . y))) by FUNCT_1:def 3;

        reconsider z = c as Element of ( [#] R) by A4;

        ((f . z) - fy) = ((x + fy) + ( - fy)) by A4

        .= (x + (fy + ( - fy))) by RLVECT_1:def 3

        .= (x + ( 0. S)) by RLVECT_1: 5;

        then

         A5: x = (f . (z - y)) by RING_2: 8;

        ( dom f) = ( [#] R) by FUNCT_2:def 1;

        hence contradiction by A3, A5, FUNCT_1:def 3;

      end;

      hence (the addF of S . (a,(f . b))) in (( [#] S) \ ( rng f)) by XBOOLE_0:def 5;

    end;

    

     Lm3: for f be Monomorphism of R, S, a,b be Element of ( carr f) st a in ( [#] R) & not b in ( [#] R) holds (the addF of S . ((f . a),b)) in (( [#] S) \ ( rng f))

    proof

      let f be Monomorphism of R, S, a,b be Element of ( carr f);

      assume

       A1: a in ( [#] R) & not b in ( [#] R);

      then

      reconsider x = a as Element of ( [#] R);

      

       A2: b in (( [#] S) \ ( rng f)) by A1, XBOOLE_0:def 3;

      then

       A3: b in ( [#] S) & not (b in ( rng f)) by XBOOLE_0:def 5;

      reconsider y = b as Element of ( [#] S) by A2;

      reconsider fx = (f . x) as Element of ( [#] S);

      now

        assume (the addF of S . ((f . x),y)) in ( rng f);

        then

        consider c be object such that

         A4: c in ( dom f) & (f . c) = (the addF of S . ((f . x),y)) by FUNCT_1:def 3;

        reconsider z = c as Element of ( [#] R) by A4;

        ((f . z) - fx) = ((fx + y) + ( - fx)) by A4

        .= (y + (fx + ( - fx))) by RLVECT_1:def 3

        .= (y + ( 0. S)) by RLVECT_1: 5;

        then

         A5: y = (f . (z - x)) by RING_2: 8;

        ( dom f) = ( [#] R) by FUNCT_2:def 1;

        hence contradiction by A3, A5, FUNCT_1:def 3;

      end;

      hence (the addF of S . ((f . a),b)) in (( [#] S) \ ( rng f)) by XBOOLE_0:def 5;

    end;

    

     Lm4: for f be Monomorphism of K, T, a,b be Element of ( carr f) st not a in ( [#] K) & b in ( [#] K) & b <> ( 0. K) holds (the multF of T . (a,(f . b))) in (( [#] T) \ ( rng f))

    proof

      let f be Monomorphism of K, T, a,b be Element of ( carr f);

      assume

       A1: not a in ( [#] K) & b in ( [#] K) & b <> ( 0. K);

      then

      reconsider y = b as Element of ( [#] K);

      reconsider fy1 = (f . (y " )) as Element of T;

      

       A2: a in (( [#] T) \ ( rng f)) by A1, XBOOLE_0:def 3;

      then

       A3: a in ( [#] T) & not (a in ( rng f)) by XBOOLE_0:def 5;

      reconsider x = a as Element of ( [#] T) by A2;

      reconsider fy = (f . y) as Element of ( [#] T);

      now

        assume (the multF of T . (x,(f . y))) in ( rng f);

        then

        consider c be object such that

         A4: c in ( dom f) & (f . c) = (the multF of T . (x,(f . y))) by FUNCT_1:def 3;

        reconsider z = c as Element of ( [#] K) by A4;

        ((f . z) * fy1) = ((x * fy) * fy1) by A4

        .= (x * (fy * fy1)) by GROUP_1:def 3

        .= (x * (f . (y * (y " )))) by GROUP_6:def 6

        .= (x * (f . ((y " ) * y))) by GROUP_1:def 12

        .= (x * (f . ( 1_ K))) by A1, VECTSP_1:def 10

        .= (x * ( 1_ T)) by GROUP_1:def 13

        .= x;

        then

         A5: x = (f . (z * (y " ))) by GROUP_6:def 6;

        ( dom f) = ( [#] K) by FUNCT_2:def 1;

        hence contradiction by A3, A5, FUNCT_1:def 3;

      end;

      hence (the multF of T . (a,(f . b))) in (( [#] T) \ ( rng f)) by XBOOLE_0:def 5;

    end;

    

     Lm5: for f be Monomorphism of K, T, a,b be Element of ( carr f) st not b in ( [#] K) & a in ( [#] K) & a <> ( 0. K) holds (the multF of T . ((f . a),b)) in (( [#] T) \ ( rng f))

    proof

      let f be Monomorphism of K, T, a,b be Element of ( carr f);

      assume

       A1: not b in ( [#] K) & a in ( [#] K) & a <> ( 0. K);

      then

      reconsider x = a as Element of ( [#] K);

      reconsider fx1 = (f . (x " )) as Element of T;

      

       A2: b in (( [#] T) \ ( rng f)) by A1, XBOOLE_0:def 3;

      then

       A3: b in ( [#] T) & not (b in ( rng f)) by XBOOLE_0:def 5;

      reconsider y = b as Element of ( [#] T) by A2;

      reconsider fx = (f . x) as Element of ( [#] T);

      now

        assume (the multF of T . ((f . x),y)) in ( rng f);

        then

        consider c be object such that

         A4: c in ( dom f) & (f . c) = (the multF of T . ((f . x),y)) by FUNCT_1:def 3;

        reconsider z = c as Element of ( [#] K) by A4;

        ((f . z) * fx1) = (((f . x) * y) * fx1) by A4

        .= ((y * (f . x)) * fx1) by GROUP_1:def 12

        .= (y * (fx * fx1)) by GROUP_1:def 3

        .= (y * (f . (x * (x " )))) by GROUP_6:def 6

        .= (y * (f . ((x " ) * x))) by GROUP_1:def 12

        .= (y * (f . ( 1_ K))) by A1, VECTSP_1:def 10

        .= (y * ( 1_ T)) by GROUP_1:def 13

        .= y;

        then

         A5: y = (f . (z * (x " ))) by GROUP_6:def 6;

        ( dom f) = ( [#] K) by FUNCT_2:def 1;

        hence contradiction by A3, A5, FUNCT_1:def 3;

      end;

      hence (the multF of T . ((f . a),b)) in (( [#] T) \ ( rng f)) by XBOOLE_0:def 5;

    end;

    definition

      let R be Ring, S be R -monomorphic Ring;

      let f be Monomorphism of R, S;

      let a,b be Element of ( carr f);

      :: FIELD_2:def3

      func addemb (f,a,b) -> Element of ( carr f) equals

      : defaddf: (the addF of R . (a,b)) if a in ( [#] R) & b in ( [#] R),

(the addF of S . ((f . a),b)) if a in ( [#] R) & not b in ( [#] R),

(the addF of S . (a,(f . b))) if b in ( [#] R) & not a in ( [#] R),

((f " ) . (the addF of S . (a,b))) if not a in ( [#] R) & not b in ( [#] R) & (the addF of S . (a,b)) in ( rng f)

      otherwise (the addF of S . (a,b));

      coherence

      proof

        set AddR = the addF of R;

        set AddS = the addF of S;

        thus (a in ( [#] R) & b in ( [#] R)) implies (AddR . (a,b)) is Element of ( carr f)

        proof

          assume a in ( [#] R) & b in ( [#] R);

          then

          reconsider x = a, y = b as Element of ( [#] R);

          (AddR . (x,y)) in ((( [#] S) \ ( rng f)) \/ ( [#] R)) by XBOOLE_0:def 3;

          hence thesis;

        end;

        (a in ( [#] R) & not b in ( [#] R)) implies (AddS . ((f . a),b)) in (( [#] S) \ ( rng f)) by Lm3;

        hence (a in ( [#] R) & not b in ( [#] R)) implies (AddS . ((f . a),b)) is Element of ( carr f) by XBOOLE_0:def 3;

        (b in ( [#] R) & not a in ( [#] R)) implies (AddS . (a,(f . b))) in (( [#] S) \ ( rng f)) by Lm2;

        hence (b in ( [#] R) & not a in ( [#] R)) implies (AddS . (a,(f . b))) is Element of ( carr f) by XBOOLE_0:def 3;

        thus ( not a in ( [#] R) & not b in ( [#] R) & (AddS . (a,b)) in ( rng f)) implies ((f " ) . (AddS . (a,b))) is Element of ( carr f)

        proof

          assume

           B1: not a in ( [#] R) & not b in ( [#] R) & (AddS . (a,b)) in ( rng f);

          

           B2: ( rng (f " )) = ( dom f) by FUNCT_1: 33

          .= ( [#] R) by FUNCT_2:def 1;

          (AddS . (a,b)) in ( dom (f " )) by B1, FUNCT_1: 33;

          then ((f " ) . (AddS . (a,b))) in ( [#] R) by B2, FUNCT_1: 3;

          hence thesis by XBOOLE_0:def 3;

        end;

        ( not a in ( [#] R) & not b in ( [#] R) & not (AddS . (a,b)) in ( rng f)) implies (AddS . (a,b)) is Element of ( carr f)

        proof

          assume

           A1: not a in ( [#] R) & not b in ( [#] R) & not (AddS . (a,b)) in ( rng f);

          then a in (( [#] S) \ ( rng f)) & b in (( [#] S) \ ( rng f)) by XBOOLE_0:def 3;

          then

          reconsider a1 = a, b1 = b as Element of ( [#] S);

          (AddS . (a1,b1)) in (( [#] S) \ ( rng f)) by A1, XBOOLE_0:def 5;

          hence (AddS . (a,b)) is Element of ( carr f) by XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

      consistency ;

    end

    definition

      let R be Ring;

      let S be R -monomorphic Ring;

      let f be Monomorphism of R, S;

      :: FIELD_2:def4

      func addemb f -> BinOp of ( carr f) means

      : defadd: for a,b be Element of ( carr f) holds (it . (a,b)) = ( addemb (f,a,b));

      existence

      proof

        deffunc O( Element of ( carr f), Element of ( carr f)) = ( addemb (f,$1,$2));

        consider F be BinOp of ( carr f) such that

         A1: for a,b be Element of ( carr f) holds (F . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( carr f) such that

         A2: for a,b be Element of ( carr f) holds (F1 . (a,b)) = ( addemb (f,a,b)) and

         A3: for a,b be Element of ( carr f) holds (F2 . (a,b)) = ( addemb (f,a,b));

        now

          let a,b be Element of ( carr f);

          

          thus (F1 . (a,b)) = ( addemb (f,a,b)) by A2

          .= (F2 . (a,b)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      let a,b be Element of ( carr f);

      :: FIELD_2:def5

      func multemb (f,a,b) -> Element of ( carr f) equals

      : defmultf: (the multF of K . (a,b)) if a in ( [#] K) & b in ( [#] K),

( 0. K) if a = ( 0. K) or b = ( 0. K),

(the multF of T . ((f . a),b)) if a in ( [#] K) & a <> ( 0. K) & not b in ( [#] K),

(the multF of T . (a,(f . b))) if b in ( [#] K) & b <> ( 0. K) & not a in ( [#] K),

((f " ) . (the multF of T . (a,b))) if not a in ( [#] K) & not b in ( [#] K) & (the multF of T . (a,b)) in ( rng f)

      otherwise (the multF of T . (a,b));

      coherence

      proof

        thus (a in ( [#] K) & b in ( [#] K)) implies (the multF of K . (a,b)) is Element of ( carr f)

        proof

          assume a in ( [#] K) & b in ( [#] K);

          then

          reconsider x = a, y = b as Element of ( [#] K);

          (the multF of K . (x,y)) in ((( [#] T) \ ( rng f)) \/ ( [#] K)) by XBOOLE_0:def 3;

          hence thesis;

        end;

        thus (a = ( 0. K) or b = ( 0. K)) implies ( 0. K) is Element of ( carr f);

        (a in ( [#] K) & a <> ( 0. K) & not b in ( [#] K)) implies (the multF of T . ((f . a),b)) in (( [#] T) \ ( rng f)) by Lm5;

        hence (a in ( [#] K) & a <> ( 0. K) & not b in ( [#] K)) implies (the multF of T . ((f . a),b)) is Element of ( carr f) by XBOOLE_0:def 3;

        (b in ( [#] K) & b <> ( 0. K) & not a in ( [#] K)) implies (the multF of T . (a,(f . b))) in (( [#] T) \ ( rng f)) by Lm4;

        hence (b in ( [#] K) & b <> ( 0. K) & not a in ( [#] K)) implies (the multF of T . (a,(f . b))) is Element of ( carr f) by XBOOLE_0:def 3;

        thus ( not a in ( [#] K) & not b in ( [#] K)) & (the multF of T . (a,b)) in ( rng f) implies ((f " ) . (the multF of T . (a,b))) is Element of ( carr f)

        proof

          assume

           A1: not a in ( [#] K) & not b in ( [#] K) & (the multF of T . (a,b)) in ( rng f);

          

           A2: ( rng (f " )) = ( dom f) by FUNCT_1: 33

          .= ( [#] K) by FUNCT_2:def 1;

          (the multF of T . (a,b)) in ( dom (f " )) by A1, FUNCT_1: 33;

          then ((f " ) . (the multF of T . (a,b))) in ( [#] K) by A2, FUNCT_1: 3;

          hence thesis by XBOOLE_0:def 3;

        end;

        ( not a in ( [#] K) & not b in ( [#] K) & not (the multF of T . (a,b)) in ( rng f)) implies (the multF of T . (a,b)) is Element of ( carr f)

        proof

          assume

           A3: not a in ( [#] K) & not b in ( [#] K) & not (the multF of T . (a,b)) in ( rng f);

          then a in (( [#] T) \ ( rng f)) & b in (( [#] T) \ ( rng f)) by XBOOLE_0:def 3;

          then

          reconsider a1 = a, b1 = b as Element of ( [#] T);

          (the multF of T . (a1,b1)) in (( [#] T) \ ( rng f)) by A3, XBOOLE_0:def 5;

          hence (the multF of T . (a,b)) is Element of ( carr f) by XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

      consistency

      proof

        let x be Element of ( carr f);

        now

          assume

           A1: a in ( [#] K) & b in ( [#] K) & (a = ( 0. K) or b = ( 0. K));

          then

          reconsider a1 = a, b1 = b as Element of K;

          per cases by A1;

            suppose a = ( 0. K);

            

            then ( 0. K) = (a1 * b1)

            .= (the multF of K . (a,b));

            hence (x = (the multF of K . (a,b)) iff x = ( 0. K));

          end;

            suppose b = ( 0. K);

            

            then ( 0. K) = (a1 * b1)

            .= (the multF of K . (a,b));

            hence (x = (the multF of K . (a,b)) iff x = ( 0. K));

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      :: FIELD_2:def6

      func multemb f -> BinOp of ( carr f) means

      : defmult: for a,b be Element of ( carr f) holds (it . (a,b)) = ( multemb (f,a,b));

      existence

      proof

        deffunc O( Element of ( carr f), Element of ( carr f)) = ( multemb (f,$1,$2));

        consider F be BinOp of ( carr f) such that

         A1: for a,b be Element of ( carr f) holds (F . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( carr f) such that

         A2: for a,b be Element of ( carr f) holds (F1 . (a,b)) = ( multemb (f,a,b)) and

         A3: for a,b be Element of ( carr f) holds (F2 . (a,b)) = ( multemb (f,a,b));

        now

          let a,b be Element of ( carr f);

          

          thus (F1 . (a,b)) = ( multemb (f,a,b)) by A2

          .= (F2 . (a,b)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      :: FIELD_2:def7

      func embField f -> strict doubleLoopStr means

      : defemb: the carrier of it = ( carr f) & the addF of it = ( addemb f) & the multF of it = ( multemb f) & the OneF of it = ( 1. K) & the ZeroF of it = ( 0. K);

      existence

      proof

        reconsider e = ( 1. K), o = ( 0. K) as Element of ( carr f) by XBOOLE_0:def 3;

        take doubleLoopStr (# ( carr f), ( addemb f), ( multemb f), e, o #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      cluster ( embField f) -> non degenerated;

      coherence

      proof

        ( 0. ( embField f)) = ( 0. K) & ( 1. ( embField f)) = ( 1. K) by defemb;

        hence thesis;

      end;

    end

    

     Lm6: for f be Monomorphism of K, T st (K,T) are_disjoint holds for a,b be Element of ( embField f) st a in ( [#] K) & not b in ( [#] K) holds for a1,b1 be Element of ( carr f) st a1 = a & b1 = b holds (a + b) = (the addF of T . ((f . a1),b1)) & (b + a) = (the addF of T . (b1,(f . a1))) & not (a + b) in ( [#] K) & not (b + a) in ( [#] K)

    proof

      let f be Monomorphism of K, T;

      assume

       A1: (K,T) are_disjoint ;

      let a,b be Element of ( embField f);

      assume

       A2: a in ( [#] K) & not b in ( [#] K);

      let a1,b1 be Element of ( carr f);

      assume

       A3: a1 = a & b1 = b;

      

      thus

       A4: (a + b) = (( addemb f) . (a,b)) by defemb

      .= ( addemb (f,a1,b1)) by defadd, A3

      .= (the addF of T . ((f . a1),b1)) by A2, A3, defaddf;

      

      thus

       A5: (b + a) = (( addemb f) . (b,a)) by defemb

      .= ( addemb (f,b1,a1)) by defadd, A3

      .= (the addF of T . (b1,(f . a1))) by A3, A2, defaddf;

      (the addF of T . ((f . a1),b1)) in (( [#] T) \ ( rng f)) by A2, A3, Lm3;

      hence not (a + b) in ( [#] K) by A1, A4, XBOOLE_0:def 4;

      (the addF of T . (b1,(f . a1))) in (( [#] T) \ ( rng f)) by A3, A2, Lm2;

      hence not (b + a) in ( [#] K) by A1, A5, XBOOLE_0:def 4;

    end;

    

     Lm7: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of K st a1 = a & b1 = b holds (a + b) = (a1 + b1) & (b + a) = (b1 + a1)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of K;

      assume

       A1: a1 = a & b1 = b;

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus (a + b) = (( addemb f) . (a,b)) by defemb

      .= ( addemb (f,ac,bc)) by defadd

      .= (a1 + b1) by A1, defaddf;

      

      thus (b + a) = (( addemb f) . (b,a)) by defemb

      .= ( addemb (f,bc,ac)) by defadd

      .= (b1 + a1) by A1, defaddf;

    end;

    

     Lm8: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T st (K,T) are_disjoint & not a in ( [#] K) & not b in ( [#] K) & not (the addF of T . (a,b)) in ( rng f) & a1 = a & b1 = b holds (a + b) = (a1 + b1) & (b + a) = (b1 + a1) & not (a + b) in ( [#] K) & not (b + a) in ( [#] K)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T;

      assume

       AS1: (K,T) are_disjoint & not a in ( [#] K) & not b in ( [#] K) & not (the addF of T . (a,b)) in ( rng f) & a1 = a & b1 = b;

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus

       D: (a + b) = (( addemb f) . (a,b)) by defemb

      .= ( addemb (f,ac,bc)) by defadd

      .= (a1 + b1) by AS1, defaddf;

      

       C: (the addF of T . (a1,b1)) = (a1 + b1)

      .= (b1 + a1)

      .= (the addF of T . (b1,a1));

      

      thus

       E: (b + a) = (( addemb f) . (b,a)) by defemb

      .= ( addemb (f,bc,ac)) by defadd

      .= (b1 + a1) by C, AS1, defaddf;

      thus not (a + b) in ( [#] K) by D, AS1, XBOOLE_0:def 4;

      thus not (b + a) in ( [#] K) by E, AS1, XBOOLE_0:def 4;

    end;

    

     Lm9: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T st not a in ( [#] K) & not b in ( [#] K) & (the addF of T . (a,b)) in ( rng f) & a1 = a & b1 = b holds (a + b) = ((f " ) . (a1 + b1)) & (b + a) = ((f " ) . (b1 + a1)) & (a + b) in ( [#] K) & (b + a) in ( [#] K)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T;

      assume

       AS: not a in ( [#] K) & not b in ( [#] K) & (the addF of T . (a,b)) in ( rng f) & a1 = a & b1 = b;

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus

       D: (a + b) = (( addemb f) . (a,b)) by defemb

      .= ( addemb (f,ac,bc)) by defadd

      .= ((f " ) . (a1 + b1)) by AS, defaddf;

      

       C: (the addF of T . (a1,b1)) = (a1 + b1)

      .= (b1 + a1)

      .= (the addF of T . (b1,a1));

      

      thus

       E: (b + a) = (( addemb f) . (b,a)) by defemb

      .= ( addemb (f,bc,ac)) by defadd

      .= ((f " ) . (b1 + a1)) by C, AS, defaddf;

      (a1 + b1) in ( dom (f " )) by AS, FUNCT_1: 33;

      then

       F: ((f " ) . (a1 + b1)) in ( rng (f " )) by FUNCT_1:def 3;

      hence (a + b) in ( [#] K) by D;

      thus (b + a) in ( [#] K) by E, F;

    end;

    

     Lm10: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of ( carr f) st (K,T) are_disjoint & a in ( [#] K) & a <> ( 0. K) & not b in ( [#] K) & a1 = a & b1 = b holds (a * b) = (the multF of T . ((f . a1),b1)) & (b * a) = (the multF of T . (b1,(f . a1))) & not (a * b) in ( [#] K) & not (b * a) in ( [#] K)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of ( carr f);

      assume

       AS: (K,T) are_disjoint & a in ( [#] K) & a <> ( 0. K) & not b in ( [#] K) & a1 = a & b1 = b;

      

      thus

       C1: (a * b) = (( multemb f) . (a,b)) by defemb

      .= ( multemb (f,a1,b1)) by defmult, AS

      .= (the multF of T . ((f . a1),b1)) by AS, defmultf;

      

      thus

       D1: (b * a) = (( multemb f) . (b,a)) by defemb

      .= ( multemb (f,b1,a1)) by defmult, AS

      .= (the multF of T . (b1,(f . a1))) by AS, defmultf;

      (the multF of T . ((f . a1),b1)) in (( [#] T) \ ( rng f)) by AS, Lm5;

      hence not (a * b) in ( [#] K) by AS, C1, XBOOLE_0:def 4;

      (the multF of T . (b1,(f . a1))) in (( [#] T) \ ( rng f)) by AS, Lm4;

      hence not (b * a) in ( [#] K) by AS, D1, XBOOLE_0:def 4;

    end;

    

     Lm11: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of K st a1 = a & b1 = b holds (a * b) = (a1 * b1) & (b * a) = (b1 * a1)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of K;

      assume

       B1: a1 = a & b1 = b;

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus (a * b) = (( multemb f) . (a,b)) by defemb

      .= ( multemb (f,ac,bc)) by defmult

      .= (a1 * b1) by B1, defmultf;

      

      thus (b * a) = (( multemb f) . (b,a)) by defemb

      .= ( multemb (f,bc,ac)) by defmult

      .= (b1 * a1) by B1, defmultf;

    end;

    

     Lm12: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T st (K,T) are_disjoint & not a in ( [#] K) & not b in ( [#] K) & not (the multF of T . (a,b)) in ( rng f) & a1 = a & b1 = b holds (a * b) = (a1 * b1) & (b * a) = (b1 * a1) & not (a * b) in ( [#] K) & not (b * a) in ( [#] K)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T;

      assume

       AS: (K,T) are_disjoint & not a in ( [#] K) & not b in ( [#] K) & not (the multF of T . (a,b)) in ( rng f) & a1 = a & b1 = b;

      then

       B1: a <> ( 0. K) & b <> ( 0. K);

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus

       D1: (a * b) = (( multemb f) . (a,b)) by defemb

      .= ( multemb (f,ac,bc)) by defmult

      .= (a1 * b1) by B1, AS, defmultf;

      

       C1: (the multF of T . (a1,b1)) = (a1 * b1)

      .= (b1 * a1) by GROUP_1:def 12

      .= (the multF of T . (b1,a1));

      

      thus (b * a) = (( multemb f) . (b,a)) by defemb

      .= ( multemb (f,bc,ac)) by defmult

      .= (b1 * a1) by B1, C1, AS, defmultf;

      hence not (a * b) in ( [#] K) & not (b * a) in ( [#] K) by D1, AS, XBOOLE_0:def 4;

    end;

    

     Lm13: for f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T st not a in ( [#] K) & not b in ( [#] K) & (the multF of T . (a,b)) in ( rng f) & a1 = a & b1 = b holds (a * b) = ((f " ) . (a1 * b1)) & (b * a) = ((f " ) . (b1 * a1)) & (a * b) in ( [#] K) & (b * a) in ( [#] K)

    proof

      let f be Monomorphism of K, T, a,b be Element of ( embField f), a1,b1 be Element of T;

      assume

       AS: not a in ( [#] K) & not b in ( [#] K) & (the multF of T . (a,b)) in ( rng f) & a1 = a & b1 = b;

      reconsider ac = a, bc = b as Element of ( carr f) by defemb;

      

      thus

       D1: (a * b) = (( multemb f) . (a,b)) by defemb

      .= ( multemb (f,ac,bc)) by defmult

      .= ((f " ) . (a1 * b1)) by AS, defmultf;

      

       C1: (the multF of T . (a1,b1)) = (a1 * b1)

      .= (b1 * a1) by GROUP_1:def 12

      .= (the multF of T . (b1,a1));

      

      thus

       E1: (b * a) = (( multemb f) . (b,a)) by defemb

      .= ( multemb (f,bc,ac)) by defmult

      .= ((f " ) . (b1 * a1)) by C1, AS, defmultf;

      (a1 * b1) in ( dom (f " )) by AS, FUNCT_1: 33;

      then

       G1: ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

      hence (a * b) in ( [#] K) by D1;

      ((f " ) . (a1 * b1)) in ( dom f) by G1, FUNCT_1: 33;

      then ((f " ) . (b1 * a1)) in ( dom f) by GROUP_1:def 12;

      hence (b * a) in ( [#] K) by E1;

    end;

    registration

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      cluster ( embField f) -> Abelian right_zeroed;

      coherence

      proof

        thus ( embField f) is Abelian

        proof

          now

            let a,b be Element of ( embField f);

            reconsider x = a, y = b as Element of ( carr f) by defemb;

            per cases ;

              suppose x in ( [#] K) & y in ( [#] K);

              then

              reconsider a1 = a, b1 = b as Element of K;

              

              thus (a + b) = (a1 + b1) by Lm7

              .= (b + a) by Lm7;

            end;

              suppose

               A2: x in ( [#] K) & not y in ( [#] K);

              then

              reconsider a1 = a as Element of K;

              reconsider b1 = b as Element of T by A2, Lm1;

              reconsider fa = (f . a1) as Element of T;

              

              thus (a + b) = (( addemb f) . (x,y)) by defemb

              .= ( addemb (f,x,y)) by defadd

              .= (fa + b1) by A2, defaddf

              .= (b1 + fa)

              .= ( addemb (f,y,x)) by A2, defaddf

              .= (( addemb f) . (y,x)) by defadd

              .= (b + a) by defemb;

            end;

              suppose

               A3: y in ( [#] K) & not x in ( [#] K);

              then

              reconsider b1 = b as Element of K;

              reconsider a1 = a as Element of T by A3, Lm1;

              reconsider fb = (f . b1) as Element of T;

              

              thus (a + b) = (( addemb f) . (x,y)) by defemb

              .= ( addemb (f,x,y)) by defadd

              .= (a1 + fb) by A3, defaddf

              .= (fb + a1)

              .= ( addemb (f,y,x)) by A3, defaddf

              .= (( addemb f) . (y,x)) by defadd

              .= (b + a) by defemb;

            end;

              suppose

               A4: not x in ( [#] K) & not y in ( [#] K) & (the addF of T . (x,y)) in ( rng f);

              then

              reconsider a1 = a, b1 = b as Element of T by Lm1;

              

               B1: (the addF of T . (a,b)) = (a1 + b1)

              .= (b1 + a1)

              .= (the addF of T . (b,a));

              

              thus (a + b) = (( addemb f) . (x,y)) by defemb

              .= ( addemb (f,x,y)) by defadd

              .= ((f " ) . (a1 + b1)) by A4, defaddf

              .= ( addemb (f,y,x)) by A4, B1, defaddf

              .= (( addemb f) . (y,x)) by defadd

              .= (b + a) by defemb;

            end;

              suppose

               A5: not x in ( [#] K) & not y in ( [#] K) & not (the addF of T . (x,y)) in ( rng f);

              then

              reconsider a1 = a, b1 = b as Element of T by Lm1;

              

               B2: (the addF of T . (a,b)) = (a1 + b1)

              .= (b1 + a1)

              .= (the addF of T . (b,a));

              

              thus (a + b) = (( addemb f) . (x,y)) by defemb

              .= ( addemb (f,x,y)) by defadd

              .= (a1 + b1) by A5, defaddf

              .= ( addemb (f,y,x)) by A5, B2, defaddf

              .= (( addemb f) . (y,x)) by defadd

              .= (b + a) by defemb;

            end;

          end;

          hence thesis;

        end;

        now

          let a be Element of ( embField f);

          reconsider x = a as Element of ( carr f) by defemb;

          reconsider o = ( 0. ( embField f)) as Element of ( carr f) by defemb;

          

           B1: (a + ( 0. ( embField f))) = (( addemb f) . (x,o)) by defemb

          .= ( addemb (f,x,o)) by defadd;

          

           C1: ( 0. ( embField f)) = ( 0. K) by defemb;

          per cases ;

            suppose x in ( [#] K);

            then

            reconsider a1 = a as Element of K;

            ( addemb (f,x,o)) = (a1 + ( 0. K)) by C1, defaddf;

            hence (a + ( 0. ( embField f))) = a by B1;

          end;

            suppose

             A1: not x in ( [#] K);

            then

            reconsider a1 = a as Element of T by Lm1;

            ( addemb (f,x,o)) = (the addF of T . (a,(f . o))) by A1, C1, defaddf

            .= (a1 + ( 0. T)) by C1, RING_2: 6;

            hence (a + ( 0. ( embField f))) = a by B1;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_2:7

    

     Th6: for f be Monomorphism of K, T st (K,T) are_disjoint holds ( embField f) is add-associative

    proof

      let f be Monomorphism of K, T;

      assume

       AS: (K,T) are_disjoint ;

      now

        let a,b,c be Element of ( embField f);

        reconsider x = a, y = b, z = c as Element of ( carr f) by defemb;

        per cases ;

          suppose

           X: x in ( [#] K);

          then

          reconsider a1 = a as Element of K;

          per cases ;

            suppose

             Y: y in ( [#] K);

            then

            reconsider b1 = b as Element of K;

            

             X0: (a + b) = (a1 + b1) by Lm7;

            then

            reconsider ab = (a + b) as Element of ( carr f) by XBOOLE_0:def 3;

            per cases ;

              suppose z in ( [#] K);

              then

              reconsider c1 = c as Element of K;

              

               X1: (b + c) = (b1 + c1) by Lm7;

              then

              reconsider bc = (b + c) as Element of ( carr f) by XBOOLE_0:def 3;

              

              thus ((a + b) + c) = (( addemb f) . ((a + b),z)) by defemb

              .= ( addemb (f,ab,z)) by defadd

              .= ((a1 + b1) + c1) by X0, defaddf

              .= (a1 + (b1 + c1)) by RLVECT_1:def 3

              .= ( addemb (f,x,bc)) by X1, defaddf

              .= (( addemb f) . (x,(b + c))) by defadd

              .= (a + (b + c)) by defemb;

            end;

              suppose

               Z: not z in ( [#] K);

              then

              reconsider c1 = c as Element of T by Lm1;

              reconsider bc = (b + c) as Element of ( carr f) by defemb;

              reconsider fa = (f . a1), fb = (f . b1) as Element of T;

              

               X1: (f . (a1 + b1)) = (fa + fb) by VECTSP_1:def 20;

              

               X2: (b + c) = (fb + c1) by AS, Y, Z, Lm6;

              

               X3: not (fb + c1) in ( [#] K) by AS, XBOOLE_0:def 4;

              

              thus ((a + b) + c) = (( addemb f) . ((a + b),z)) by defemb

              .= ( addemb (f,ab,z)) by defadd

              .= ((fa + fb) + c1) by X1, X0, defaddf, Z

              .= (fa + (fb + c1)) by RLVECT_1:def 3

              .= ( addemb (f,x,bc)) by X3, X2, defaddf

              .= (( addemb f) . (x,(b + c))) by defadd

              .= (a + (b + c)) by defemb;

            end;

          end;

            suppose

             Y: not y in ( [#] K);

            then

            reconsider b1 = b as Element of T by Lm1;

            reconsider fa = (f . a1) as Element of T;

            

             X0: (a + b) = (fa + b1) by AS, X, Y, Lm6;

            then

            reconsider ab = (fa + b1) as Element of ( carr f) by defemb;

            

             X1: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

            per cases ;

              suppose

               Z: z in ( [#] K);

              then

              reconsider c1 = c as Element of K;

              reconsider fc = (f . c1) as Element of T;

              

               X2: (b + c) = (b1 + fc) by AS, Y, Z, Lm6;

              then

              reconsider bc = (b1 + fc) as Element of ( carr f) by defemb;

              

               X3: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

              

              thus ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

              .= ( addemb (f,ab,z)) by defadd

              .= ((fa + b1) + fc) by X1, defaddf

              .= (fa + (b1 + fc)) by RLVECT_1:def 3

              .= ( addemb (f,x,bc)) by X3, defaddf

              .= (( addemb f) . (x,bc)) by defadd

              .= (a + (b + c)) by X2, defemb;

            end;

              suppose

               Z: not z in ( [#] K);

              then

              reconsider c1 = c as Element of T by Lm1;

              reconsider fa1 = (f . a1) as Element of ( rng f) by FUNCT_2: 4;

              

               K5: (the addF of T . (ab,z)) = ((fa + b1) + c1)

              .= (fa + (b1 + c1)) by RLVECT_1:def 3;

              per cases ;

                suppose

                 K: (the addF of T . (ab,z)) in ( rng f);

                

                 X2: ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((f " ) . ((fa + b1) + c1)) by X1, Z, defaddf, K

                .= ((f " ) . (fa + (b1 + c1))) by RLVECT_1:def 3;

                 K1:

                now

                  assume

                   K7: not (the addF of T . (y,z)) in ( rng f);

                  

                   X4: not (the addF of T . (b1,c1)) in ( [#] K) by AS, XBOOLE_0:def 4;

                  

                   X3: (b + c) = (b1 + c1) by AS, K7, Y, Z, Lm8;

                  (b1 + c1) in (( [#] T) \ ( rng f)) by K7, XBOOLE_0:def 5;

                  then

                  reconsider bc1 = (b1 + c1) as Element of ( carr f) by XBOOLE_0:def 3;

                  reconsider bce = bc1 as Element of ( embField f) by X3;

                  (the addF of T . ((f . a),bce)) in (( [#] T) \ ( rng f)) by X, X4, Lm3;

                  hence contradiction by K5, K, XBOOLE_0:def 5;

                end;

                then

                 X3: (b + c) = ((f " ) . (b1 + c1)) by Y, Z, Lm9;

                ((f " ) . (b1 + c1)) in ( [#] K) by K1, FUNCT_2: 5;

                then

                reconsider bc = ((f " ) . (b1 + c1)) as Element of ( carr f) by XBOOLE_0:def 3;

                reconsider bc1 = (b1 + c1) as Element of ( rng f) by K1;

                

                thus ((a + b) + c) = (((f " ) . fa1) + ((f " ) . bc1)) by Th1, X2

                .= (a1 + ((f " ) . bc1)) by FUNCT_2: 26

                .= ( addemb (f,x,bc)) by defaddf

                .= (( addemb f) . (x,bc)) by defadd

                .= (a + (b + c)) by X3, defemb;

              end;

                suppose

                 K0: not (the addF of T . (ab,z)) in ( rng f);

                

                 X2: ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((fa + b1) + c1) by X1, Z, defaddf, K0

                .= (fa + (b1 + c1)) by RLVECT_1:def 3;

                 K1:

                now

                  assume

                   K7: (the addF of T . (y,z)) in ( rng f);

                  

                   X7: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                  consider x be object such that

                   X6: x in ( dom f) & (b1 + c1) = (f . x) by K7, FUNCT_1:def 3;

                  reconsider xx = x as Element of K by X6;

                  (f . (a1 + xx)) = (fa + (b1 + c1)) by X6, VECTSP_1:def 20;

                  hence contradiction by K5, K0, X7, FUNCT_1: 3;

                end;

                then (b1 + c1) in (( [#] T) \ ( rng f)) by XBOOLE_0:def 5;

                then

                reconsider bc = (b1 + c1) as Element of ( carr f) by XBOOLE_0:def 3;

                

                 X3: (b + c) = (b1 + c1) by AS, Y, Z, K1, Lm8;

                 not (b1 + c1) in ( [#] K) by AS, XBOOLE_0:def 4;

                

                hence ((a + b) + c) = ( addemb (f,x,bc)) by X2, defaddf

                .= (( addemb f) . (x,bc)) by defadd

                .= (a + (b + c)) by X3, defemb;

              end;

            end;

          end;

        end;

          suppose

           X4: not x in ( [#] K);

          then

          reconsider a1 = a as Element of T by Lm1;

          per cases ;

            suppose

             Y0: y in ( [#] K);

            then

            reconsider b1 = b as Element of K;

            

             X0: (a + b) = (a1 + (f . b1)) by AS, X4, Y0, Lm6;

            reconsider ab = (a + b) as Element of ( carr f) by defemb;

            reconsider fb = (f . b1) as Element of T;

            

             X2: not ab in ( [#] K) by AS, X4, Y0, Lm6;

            per cases ;

              suppose z in ( [#] K);

              then

              reconsider c1 = c as Element of K;

              reconsider fc = (f . c1) as Element of T;

              

               X3: (b + c) = (b1 + c1) by Lm7;

              then

              reconsider bc = (b + c) as Element of ( carr f) by XBOOLE_0:def 3;

              

              thus ((a + b) + c) = (( addemb f) . (ab,z)) by defemb

              .= ( addemb (f,ab,z)) by defadd

              .= ((a1 + fb) + fc) by X0, X2, defaddf

              .= (a1 + (fb + fc)) by RLVECT_1:def 3

              .= (a1 + (f . (b1 + c1))) by VECTSP_1:def 20

              .= ( addemb (f,x,bc)) by defaddf, X3, X4

              .= (( addemb f) . (x,bc)) by defadd

              .= (a + (b + c)) by defemb;

            end;

              suppose

               Z0: not z in ( [#] K);

              then

              reconsider c1 = c as Element of T by Lm1;

              

               X3: (b + c) = ((f . b1) + c1) by AS, Y0, Z0, Lm6;

              reconsider bc = (b + c) as Element of ( carr f) by defemb;

              

               X5: not (b + c) in ( [#] K) by AS, Y0, Z0, Lm6;

              

               K5: (the addF of T . (ab,z)) = ((a1 + fb) + c1) by AS, X4, Y0, Lm6

              .= (a1 + (fb + c1)) by RLVECT_1:def 3

              .= (the addF of T . (x,bc)) by AS, Y0, Z0, Lm6;

              per cases ;

                suppose

                 K0: not (the addF of T . (ab,z)) in ( rng f);

                

                thus ((a + b) + c) = (( addemb f) . (ab,z)) by defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((a1 + fb) + c1) by X0, K0, X2, Z0, defaddf

                .= (a1 + (fb + c1)) by RLVECT_1:def 3

                .= ( addemb (f,x,bc)) by K0, K5, X3, X4, X5, defaddf

                .= (( addemb f) . (x,bc)) by defadd

                .= (a + (b + c)) by defemb;

              end;

                suppose

                 K1: (the addF of T . (ab,z)) in ( rng f);

                

                thus ((a + b) + c) = (( addemb f) . (ab,z)) by defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((f " ) . (the addF of T . (ab,z))) by K1, X2, Z0, defaddf

                .= ( addemb (f,x,bc)) by K1, K5, X4, X5, defaddf

                .= (( addemb f) . (x,bc)) by defadd

                .= (a + (b + c)) by defemb;

              end;

            end;

          end;

            suppose

             Y0: not y in ( [#] K);

            then

            reconsider b1 = b as Element of T by Lm1;

            per cases ;

              suppose

               K2: not (the addF of T . (x,y)) in ( rng f);

              

               K1: not (the addF of T . (a1,b1)) in ( [#] K) by AS, XBOOLE_0:def 4;

              

               X0: (a + b) = (a1 + b1) by K2, Y0, X4, AS, Lm8;

              (a1 + b1) in (( [#] T) \ ( rng f)) by K2, XBOOLE_0:def 5;

              then

              reconsider ab = (a1 + b1) as Element of ( carr f) by XBOOLE_0:def 3;

              

               D: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

              per cases ;

                suppose

                 Z: z in ( [#] K);

                then

                reconsider c1 = c as Element of K;

                

                 X1: (b + c) = (b1 + (f . c1)) by AS, Y0, Z, Lm6;

                ( [#] ( embField f)) = ( carr f) by defemb;

                then

                 X3: (b1 + (f . c1)) in (( [#] T) \ ( rng f)) by Y0, Lm2;

                

                 X2: not (b1 + (f . c1)) in ( [#] K) by AS, XBOOLE_0:def 4;

                reconsider bc = (b1 + (f . c1)) as Element of ( carr f) by X3, XBOOLE_0:def 3;

                

                 X4a: ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((a1 + b1) + (f . c1)) by K1, defaddf

                .= (a1 + (b1 + (f . c1))) by RLVECT_1:def 3;

                

                 X5: (the addF of T . (x,bc)) = (a1 + (b1 + (f . c1)))

                .= ((a1 + b1) + (f . c1)) by RLVECT_1:def 3

                .= (the addF of T . (ab,(f . z)));

                (the addF of T . (ab,(f . z))) in (( [#] T) \ ( rng f)) by D, Lm2, Z;

                then not (the addF of T . (x,bc)) in ( rng f) by X5, XBOOLE_0:def 5;

                

                hence ((a + b) + c) = ( addemb (f,x,bc)) by X4, X2, X4a, defaddf

                .= (( addemb f) . (x,bc)) by defadd

                .= (a + (b + c)) by X1, defemb;

              end;

                suppose

                 Z: not z in ( [#] K);

                then

                reconsider c1 = c as Element of T by Lm1;

                

                 K5: (the addF of T . (ab,z)) = ((a1 + b1) + c1)

                .= (a1 + (b1 + c1)) by RLVECT_1:def 3

                .= (the addF of T . (a1,(b1 + c1)));

                per cases ;

                  suppose

                   K: not (the addF of T . (ab,z)) in ( rng f);

                  per cases ;

                    suppose

                     K6: not (the addF of T . (b1,c1)) in ( rng f);

                    then

                     X1: (b + c) = (b1 + c1) by AS, Y0, Z, Lm8;

                    

                     K9: (the addF of T . (b1,c1)) in (( [#] T) \ ( rng f)) by K6, XBOOLE_0:def 5;

                    

                     K8: not (b1 + c1) in ( [#] K) by AS, XBOOLE_0:def 4;

                    reconsider bc = (b1 + c1) as Element of ( carr f) by K9, XBOOLE_0:def 3;

                    

                    thus ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                    .= ( addemb (f,ab,z)) by defadd

                    .= ((a1 + b1) + c1) by D, Z, defaddf, K

                    .= ( addemb (f,x,bc)) by X4, K5, K, K8, defaddf

                    .= (( addemb f) . (x,bc)) by defadd

                    .= (a + (b + c)) by X1, defemb;

                  end;

                    suppose

                     K6: (the addF of T . (b1,c1)) in ( rng f);

                    then

                     X1: (b + c) = ((f " ) . (b1 + c1)) by Y0, Z, Lm9;

                    (b1 + c1) in ( dom (f " )) by K6, FUNCT_1: 33;

                    then ((f " ) . (b1 + c1)) in ( rng (f " )) by FUNCT_1: 3;

                    then

                    reconsider bc1 = ((f " ) . (b1 + c1)) as Element of ( [#] K);

                    reconsider bc = bc1 as Element of ( carr f) by XBOOLE_0:def 3;

                    

                    thus ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                    .= ( addemb (f,ab,z)) by defadd

                    .= ((a1 + b1) + c1) by D, Z, defaddf, K

                    .= (a1 + (b1 + c1)) by RLVECT_1:def 3

                    .= (a1 + (f . bc1)) by K6, FUNCT_1: 35

                    .= ( addemb (f,x,bc)) by X4, defaddf

                    .= (( addemb f) . (x,bc)) by defadd

                    .= (a + (b + c)) by X1, defemb;

                  end;

                end;

                  suppose

                   K7: (the addF of T . (ab,z)) in ( rng f);

                   K6:

                  now

                    assume (the addF of T . (b1,c1)) in ( rng f);

                    then

                    consider x be object such that

                     H1: x in ( dom f) & (f . x) = (b1 + c1) by FUNCT_1:def 3;

                    consider y be object such that

                     H2: y in ( dom f) & (f . y) = ((a1 + b1) + c1) by K7, FUNCT_1:def 3;

                    reconsider xx = x, yy = y as Element of K by H1, H2;

                    

                     X1: (f . (yy - xx)) = ((f . yy) - (f . xx)) by RING_2: 8

                    .= ((a1 + (b1 + c1)) - (b1 + c1)) by H1, H2, RLVECT_1:def 3

                    .= (a1 + ((b1 + c1) + ( - (b1 + c1)))) by RLVECT_1:def 3

                    .= (a1 + ( 0. T)) by RLVECT_1: 5;

                    ( dom f) = ( [#] K) by FUNCT_2:def 1;

                    then a1 in ( rng f) by X1, FUNCT_1:def 3;

                    hence contradiction by X4, Lm1;

                  end;

                  then

                   X1: (b + c) = (b1 + c1) by AS, Y0, Z, Lm8;

                  (b1 + c1) in (( [#] T) \ ( rng f)) by K6, XBOOLE_0:def 5;

                  then

                  reconsider bc = (b1 + c1) as Element of ( carr f) by XBOOLE_0:def 3;

                  

                   K9: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                  

                  thus ((a + b) + c) = (( addemb f) . (ab,z)) by X0, defemb

                  .= ( addemb (f,ab,z)) by defadd

                  .= ((f " ) . ((a1 + b1) + c1)) by D, Z, defaddf, K7

                  .= ( addemb (f,x,bc)) by X4, K5, K7, defaddf, K9

                  .= (( addemb f) . (x,bc)) by defadd

                  .= (a + (b + c)) by X1, defemb;

                end;

              end;

            end;

              suppose

               L: (the addF of T . (x,y)) in ( rng f);

              then

               Z1: (a + b) = ((f " ) . (a1 + b1)) by X4, Y0, Lm9;

              (a1 + b1) in ( dom (f " )) by L, FUNCT_1: 33;

              then ((f " ) . (a1 + b1)) in ( rng (f " )) by FUNCT_1: 3;

              then

              reconsider ab1 = ((f " ) . (a1 + b1)) as Element of ( [#] K);

              reconsider ab = ab1 as Element of ( carr f) by XBOOLE_0:def 3;

              per cases ;

                suppose

                 Z: z in ( [#] K);

                then

                reconsider c1 = c as Element of K;

                

                 Z2: (b + c) = (b1 + (f . c1)) by AS, Y0, Z, Lm6;

                then

                 L0: (b + c) in (( [#] T) \ ( rng f)) by Lm2, Y0, Z;

                reconsider bc1 = (b1 + (f . c1)) as Element of T;

                reconsider bc = bc1 as Element of ( carr f) by Z2, L0, XBOOLE_0:def 3;

                

                 Z3: ((a + b) + c) = (( addemb f) . (ab,z)) by Z1, defemb

                .= ( addemb (f,ab,z)) by defadd

                .= (ab1 + c1) by defaddf;

                

                 Z4: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                

                 Z9: ( dom f) = ( [#] K) & ( rng f) c= ( [#] T) by FUNCT_2:def 1;

                

                 L2: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                then

                reconsider fc1 = (f . c1) as Element of ( rng f) by FUNCT_1:def 3;

                reconsider ffc1 = ((f " ) . fc1) as Element of K;

                ((f " ) . fc1) = c1 by L2, FUNCT_1: 34;

                then

                 Z5: ((f " ) . ((a1 + b1) + fc1)) = (ab1 + c1) by L, Th1;

                consider x1 be object such that

                 Z6: x1 in ( dom f) & (f . x1) = (a1 + b1) by L, FUNCT_1:def 3;

                reconsider xx = x1 as Element of K by Z6;

                (f . (xx + c1)) = ((a1 + b1) + (f . c1)) by Z6, VECTSP_1:def 20;

                then ((a1 + b1) + (f . c1)) in ( rng f) by Z9, FUNCT_1:def 3;

                then

                 L1: (a1 + (b1 + (f . c1))) in ( rng f) by RLVECT_1:def 3;

                

                thus (a + (b + c)) = (( addemb f) . (x,bc)) by Z2, defemb

                .= ( addemb (f,x,bc)) by defadd

                .= ((f " ) . (a1 + bc1)) by L1, Z4, X4, defaddf

                .= ((a + b) + c) by Z3, Z5, RLVECT_1:def 3;

              end;

                suppose

                 Z: not z in ( [#] K);

                then

                reconsider c1 = c as Element of T by Lm1;

                

                 Z2: ((a + b) + c) = (( addemb f) . (ab,z)) by Z1, defemb

                .= ( addemb (f,ab,z)) by defadd

                .= ((f . ab1) + c1) by Z, defaddf

                .= ((a1 + b1) + c1) by L, FUNCT_1: 35

                .= (a1 + (b1 + c1)) by RLVECT_1:def 3;

                (the addF of T . ((f . ab),z)) in (( [#] T) \ ( rng f)) by Z, Lm3;

                then ((a1 + b1) + c1) in (( [#] T) \ ( rng f)) by FUNCT_1: 35, L;

                then (a1 + (b1 + c1)) in (( [#] T) \ ( rng f)) by RLVECT_1:def 3;

                then

                 U2: not (the addF of T . (a,(b1 + c1))) in ( rng f) by XBOOLE_0:def 5;

                per cases ;

                  suppose

                   L1: not (the addF of T . (y,z)) in ( rng f);

                  then

                   X3: (b + c) = (b1 + c1) by AS, Y0, Z, Lm8;

                  

                   X4a: (b1 + c1) in (( [#] T) \ ( rng f)) by L1, XBOOLE_0:def 5;

                  reconsider bc1 = (b1 + c1) as Element of T;

                  reconsider bc = bc1 as Element of ( carr f) by X4a, XBOOLE_0:def 3;

                   not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                  

                  hence ((a + b) + c) = ( addemb (f,x,bc)) by Z2, U2, X4, defaddf

                  .= (( addemb f) . (x,bc)) by defadd

                  .= (a + (b + c)) by X3, defemb;

                end;

                  suppose

                   K6: (the addF of T . (y,z)) in ( rng f);

                  then

                   X1: (b + c) = ((f " ) . (b1 + c1)) by Y0, Z, Lm9;

                  (b1 + c1) in ( dom (f " )) by K6, FUNCT_1: 33;

                  then ((f " ) . (b1 + c1)) in ( rng (f " )) by FUNCT_1: 3;

                  then

                  reconsider bc1 = ((f " ) . (b1 + c1)) as Element of ( [#] K);

                  reconsider bc = bc1 as Element of ( carr f) by XBOOLE_0:def 3;

                  

                  thus ((a + b) + c) = (a1 + (f . bc1)) by Z2, K6, FUNCT_1: 35

                  .= ( addemb (f,x,bc)) by X4, defaddf

                  .= (( addemb f) . (x,bc)) by defadd

                  .= (a + (b + c)) by X1, defemb;

                end;

              end;

            end;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_2:8

    

     Th7: for f be Monomorphism of K, T st (K,T) are_disjoint holds ( embField f) is right_complementable

    proof

      let f be Monomorphism of K, T;

      assume

       AS: (K,T) are_disjoint ;

      now

        let a be Element of ( embField f);

        reconsider x = a as Element of ( carr f) by defemb;

        per cases ;

          suppose x in ( [#] K);

          then

          reconsider a1 = a as Element of K;

          a1 is right_complementable;

          then

          consider b1 be Element of K such that

           B1: (a1 + b1) = ( 0. K);

          reconsider y = b1 as Element of ( carr f) by XBOOLE_0:def 3;

          reconsider b = y as Element of ( embField f) by defemb;

          (a + b) = (a1 + b1) by Lm7

          .= ( 0. ( embField f)) by B1, defemb;

          hence a is right_complementable;

        end;

          suppose

           A2: not x in ( [#] K);

          then

          reconsider a1 = a as Element of T by Lm1;

          a1 is right_complementable;

          then

          consider b1 be Element of T such that

           B2: (a1 + b1) = ( 0. T);

          ( dom f) = ( [#] K) & (the addF of T . (a1,b1)) = (f . ( 0. K)) by B2, RING_2: 6, FUNCT_2:def 1;

          then

           D0: (the addF of T . (a1,b1)) in ( rng f) by FUNCT_1: 3;

          then

           D1: not (the addF of T . (a1,b1)) in (( [#] T) \ ( rng f)) by XBOOLE_0:def 5;

          per cases ;

            suppose b1 in ( rng f);

            then

            consider b1r be object such that

             C1: b1r in ( dom f) & (f . b1r) = b1 by FUNCT_1:def 3;

            reconsider b1r as Element of K by C1;

            ( [#] ( embField f)) = ( carr f) by defemb;

            then

            reconsider bx = b1r as Element of ( embField f) by XBOOLE_0:def 3;

            reconsider y = bx as Element of ( carr f) by defemb;

            

             C2: ( [#] ( embField f)) = ( carr f) by defemb;

            then (the addF of T . (a1,(f . bx))) in ( [#] K) by Lm2, A2, D1, C1;

            hence a is right_complementable by Lm2, A2, D1, C1, C2;

          end;

            suppose not b1 in ( rng f);

            then b1 in (( [#] T) \ ( rng f)) by XBOOLE_0:def 5;

            then

            reconsider y = b1 as Element of ( carr f) by XBOOLE_0:def 3;

            reconsider b = y as Element of ( embField f) by defemb;

            

             E1: not b in ( [#] K) by AS, XBOOLE_0:def 4;

            

             Y1: ( dom f) = ( [#] K) & (f . ( 0. K)) = ( 0. T) by RING_2: 6, FUNCT_2:def 1;

            (a + b) = ((f " ) . ( 0. T)) by A2, B2, D0, E1, Lm9

            .= ( 0. K) by Y1, FUNCT_1: 32

            .= ( 0. ( embField f)) by defemb;

            hence a is right_complementable;

          end;

        end;

      end;

      hence thesis;

    end;

    registration

      let K be Field, T be K -monomorphic comRing;

      let f be Monomorphism of K, T;

      cluster ( embField f) -> commutative well-unital;

      coherence

      proof

        thus ( embField f) is commutative

        proof

          now

            let a,b be Element of ( embField f);

            reconsider x = a, y = b as Element of ( carr f) by defemb;

            per cases ;

              suppose x in ( [#] K) & y in ( [#] K);

              then

              reconsider a1 = a, b1 = b as Element of K;

              

              thus (a * b) = (a1 * b1) by Lm11

              .= (b1 * a1) by GROUP_1:def 12

              .= (b * a) by Lm11;

            end;

              suppose

               A: a = ( 0. K) or b = ( 0. K);

              per cases by A;

                suppose

                 A1: a = ( 0. K);

                

                thus (a * b) = (( multemb f) . (x,y)) by defemb

                .= ( multemb (f,x,y)) by defmult

                .= ( 0. K) by A1, defmultf

                .= ( multemb (f,y,x)) by A1, defmultf

                .= (( multemb f) . (y,x)) by defmult

                .= (b * a) by defemb;

              end;

                suppose

                 A1: b = ( 0. K);

                

                thus (a * b) = (( multemb f) . (x,y)) by defemb

                .= ( multemb (f,x,y)) by defmult

                .= ( 0. K) by A1, defmultf

                .= ( multemb (f,y,x)) by A1, defmultf

                .= (( multemb f) . (y,x)) by defmult

                .= (b * a) by defemb;

              end;

            end;

              suppose

               A: x in ( [#] K) & x <> ( 0. K) & not y in ( [#] K);

              then

              reconsider a1 = a as Element of K;

              reconsider b1 = b as Element of T by A, Lm1;

              reconsider fa = (f . a1) as Element of T;

              

              thus (a * b) = (( multemb f) . (x,y)) by defemb

              .= ( multemb (f,x,y)) by defmult

              .= (fa * b1) by A, defmultf

              .= (b1 * fa) by GROUP_1:def 12

              .= ( multemb (f,y,x)) by A, defmultf

              .= (( multemb f) . (y,x)) by defmult

              .= (b * a) by defemb;

            end;

              suppose

               A: y in ( [#] K) & y <> ( 0. K) & not x in ( [#] K);

              then

              reconsider b1 = b as Element of K;

              reconsider a1 = a as Element of T by A, Lm1;

              reconsider fb = (f . b1) as Element of T;

              

              thus (a * b) = (( multemb f) . (x,y)) by defemb

              .= ( multemb (f,x,y)) by defmult

              .= (a1 * fb) by A, defmultf

              .= (fb * a1) by GROUP_1:def 12

              .= ( multemb (f,y,x)) by A, defmultf

              .= (( multemb f) . (y,x)) by defmult

              .= (b * a) by defemb;

            end;

              suppose

               A: not x in ( [#] K) & not y in ( [#] K) & (the multF of T . (x,y)) in ( rng f);

              then

              reconsider a1 = a, b1 = b as Element of T by Lm1;

              

               B: (the multF of T . (a,b)) = (a1 * b1)

              .= (b1 * a1) by GROUP_1:def 12

              .= (the multF of T . (b,a));

              

              thus (a * b) = (( multemb f) . (x,y)) by defemb

              .= ( multemb (f,x,y)) by defmult

              .= ((f " ) . (a1 * b1)) by A, defmultf

              .= ( multemb (f,y,x)) by A, B, defmultf

              .= (( multemb f) . (y,x)) by defmult

              .= (b * a) by defemb;

            end;

              suppose

               A: not x in ( [#] K) & not y in ( [#] K) & not ((the multF of T . (x,y)) in ( rng f));

              then

              reconsider a1 = a, b1 = b as Element of T by Lm1;

              

               C: a <> ( 0. K) & b <> ( 0. K) by A;

              

               B: (the multF of T . (a,b)) = (a1 * b1)

              .= (b1 * a1) by GROUP_1:def 12

              .= (the multF of T . (b,a));

              

              thus (a * b) = (( multemb f) . (x,y)) by defemb

              .= ( multemb (f,x,y)) by defmult

              .= (the multF of T . (a,b)) by C, A, defmultf

              .= ( multemb (f,y,x)) by C, A, B, defmultf

              .= (( multemb f) . (y,x)) by defmult

              .= (b * a) by defemb;

            end;

          end;

          hence thesis;

        end;

        thus ( embField f) is well-unital

        proof

          now

            let a be Element of ( embField f);

            reconsider x = a as Element of ( carr f) by defemb;

            reconsider e = ( 1. ( embField f)) as Element of ( carr f) by defemb;

            

             B: (a * ( 1. ( embField f))) = (( multemb f) . (x,e)) by defemb

            .= ( multemb (f,x,e)) by defmult;

            

             D: (( 1. ( embField f)) * a) = (( multemb f) . (e,x)) by defemb

            .= ( multemb (f,e,x)) by defmult;

            

             C: ( 1. ( embField f)) = ( 1. K) by defemb;

            per cases ;

              suppose x in ( [#] K);

              then

              reconsider a1 = a as Element of K;

              ( multemb (f,x,e)) = (a1 * ( 1. K)) by C, defmultf;

              hence (a * ( 1. ( embField f))) = a by B;

              ( multemb (f,e,x)) = (( 1. K) * a1) by C, defmultf;

              hence (( 1. ( embField f)) * a) = a by D;

            end;

              suppose

               A: not x in ( [#] K);

              then

              reconsider a1 = a as Element of T by Lm1;

              

               E: e in ( [#] K) & e <> ( 0. K) by C;

              

              then ( multemb (f,x,e)) = (the multF of T . (a1,(f . e))) by A, defmultf

              .= (the multF of T . (a1,(f . ( 1_ K)))) by defemb

              .= (a1 * ( 1_ T)) by GROUP_1:def 13;

              hence (a * ( 1. ( embField f))) = a by B;

              ( multemb (f,e,x)) = (the multF of T . ((f . e),a1)) by E, A, defmultf

              .= (the multF of T . ((f . ( 1_ K)),a1)) by defemb

              .= (( 1_ T) * a1) by GROUP_1:def 13;

              hence (( 1. ( embField f)) * a) = a by D;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: FIELD_2:9

    

     Th8: for f be Monomorphism of K, F st (K,F) are_disjoint holds ( embField f) is associative

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      now

        let a,b,c be Element of ( embField f);

        reconsider x = a, y = b, z = c as Element of ( carr f) by defemb;

        per cases ;

          suppose

           O: a = ( 0. K) or b = ( 0. K) or c = ( 0. K);

          reconsider bb = b, ab = (a * b), bc = (b * c) as Element of ( carr f) by defemb;

          per cases by O;

            suppose

             A: a = ( 0. K);

            

             A1: (a * b) = (( multemb f) . (x,bb)) by defemb

            .= ( multemb (f,x,bb)) by defmult

            .= ( 0. K) by A, defmultf;

            

             A2: ((a * b) * c) = (( multemb f) . (ab,z)) by defemb

            .= ( multemb (f,ab,z)) by defmult

            .= ( 0. K) by A1, defmultf;

            

            thus (a * (b * c)) = (( multemb f) . (x,bc)) by defemb

            .= ( multemb (f,x,bc)) by defmult

            .= ((a * b) * c) by A2, A, defmultf;

          end;

            suppose

             A: b = ( 0. K) or c = ( 0. K);

            

             A1: (b * c) = (( multemb f) . (y,z)) by defemb

            .= ( multemb (f,y,z)) by defmult

            .= ( 0. K) by A, defmultf;

            

             A2: (a * (b * c)) = (( multemb f) . (x,bc)) by defemb

            .= ( multemb (f,x,bc)) by defmult

            .= ( 0. K) by A1, defmultf;

            per cases by A;

              suppose

               A3: b = ( 0. K);

              

               A4: (a * b) = (( multemb f) . (x,bb)) by defemb

              .= ( multemb (f,x,bb)) by defmult

              .= ( 0. K) by A3, defmultf;

              

              thus ((a * b) * c) = (( multemb f) . (ab,z)) by defemb

              .= ( multemb (f,ab,z)) by defmult

              .= (a * (b * c)) by A4, A2, defmultf;

            end;

              suppose

               A3: c = ( 0. K);

              

              thus ((a * b) * c) = (( multemb f) . (ab,z)) by defemb

              .= ( multemb (f,ab,z)) by defmult

              .= (a * (b * c)) by A3, A2, defmultf;

            end;

          end;

        end;

          suppose

           O: a <> ( 0. K) & b <> ( 0. K) & c <> ( 0. K);

          per cases ;

            suppose

             X: x in ( [#] K);

            then

            reconsider a1 = a as Element of K;

            per cases ;

              suppose

               Y: y in ( [#] K);

              then

              reconsider b1 = b as Element of K;

              

               X0: (a * b) = (a1 * b1) by Lm11;

              then

              reconsider ab = (a * b) as Element of ( carr f) by XBOOLE_0:def 3;

              per cases ;

                suppose z in ( [#] K);

                then

                reconsider c1 = c as Element of K;

                

                 X1: (b * c) = (b1 * c1) by Lm11;

                then

                reconsider bc = (b * c) as Element of ( carr f) by XBOOLE_0:def 3;

                

                thus ((a * b) * c) = (( multemb f) . ((a * b),z)) by defemb

                .= ( multemb (f,ab,z)) by defmult

                .= ((a1 * b1) * c1) by X0, defmultf

                .= (a1 * (b1 * c1)) by GROUP_1:def 3

                .= ( multemb (f,x,bc)) by X1, defmultf

                .= (( multemb f) . (x,(b * c))) by defmult

                .= (a * (b * c)) by defemb;

              end;

                suppose

                 Z: not z in ( [#] K);

                then

                reconsider c1 = c as Element of F by Lm1;

                reconsider bc = (b * c) as Element of ( carr f) by defemb;

                reconsider fa = (f . a1), fb = (f . b1) as Element of F;

                

                 X1: (f . (a1 * b1)) = (fa * fb) by GROUP_6:def 6;

                

                 X2: (b * c) = (fb * c1) by AS, O, Y, Z, Lm10;

                

                 X3: not (fb * c1) in ( [#] K) by AS, XBOOLE_0:def 4;

                

                thus ((a * b) * c) = (( multemb f) . ((a * b),z)) by defemb

                .= ( multemb (f,ab,z)) by defmult

                .= ((fa * fb) * c1) by O, VECTSP_2:def 1, X1, X0, defmultf, Z

                .= (fa * (fb * c1)) by GROUP_1:def 3

                .= ( multemb (f,x,bc)) by O, X3, X2, defmultf

                .= (( multemb f) . (x,(b * c))) by defmult

                .= (a * (b * c)) by defemb;

              end;

            end;

              suppose

               Y: not y in ( [#] K);

              then

              reconsider b1 = b as Element of F by Lm1;

              reconsider fa = (f . a1) as Element of F;

              

               X0: (a * b) = (fa * b1) by AS, O, X, Y, Lm10;

              then

              reconsider ab = (fa * b1) as Element of ( carr f) by defemb;

              

               X1: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

              per cases ;

                suppose

                 Z: z in ( [#] K);

                then

                reconsider c1 = c as Element of K;

                reconsider fc = (f . c1) as Element of F;

                

                 X2: (b * c) = (b1 * fc) by AS, O, Y, Z, Lm10;

                then

                reconsider bc = (b1 * fc) as Element of ( carr f) by defemb;

                

                 X3: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                

                thus ((a * b) * c) = ((fa * b1) * fc) by AS, O, X1, X0, Z, Lm10

                .= (fa * (b1 * fc)) by GROUP_1:def 3

                .= (a * (b * c)) by AS, O, X, X2, X3, Lm10;

              end;

                suppose

                 Z: not z in ( [#] K);

                then

                reconsider c1 = c as Element of F by Lm1;

                reconsider fa1 = (f . a1) as Element of ( rng f) by FUNCT_2: 4;

                

                 K5: (the multF of F . (ab,z)) = ((fa * b1) * c1)

                .= (fa * (b1 * c1)) by GROUP_1:def 3;

                per cases ;

                  suppose

                   K: (the multF of F . (ab,z)) in ( rng f);

                  

                   X2: ((a * b) * c) = (( multemb f) . (ab,z)) by X0, defemb

                  .= ( multemb (f,ab,z)) by defmult

                  .= ((f " ) . ((fa * b1) * c1)) by X1, Z, defmultf, K

                  .= ((f " ) . (fa * (b1 * c1))) by GROUP_1:def 3;

                   K1:

                  now

                    assume

                     K7: not (the multF of F . (y,z)) in ( rng f);

                    

                     X4: not (the multF of F . (b1,c1)) in ( [#] K) by AS, XBOOLE_0:def 4;

                    

                     X3: (b * c) = (b1 * c1) by AS, Y, Z, Lm12, K7;

                    (b1 * c1) in (( [#] F) \ ( rng f)) by K7, XBOOLE_0:def 5;

                    then

                    reconsider bc1 = (b1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                    reconsider bce = bc1 as Element of ( embField f) by X3;

                    (the multF of F . ((f . a),bce)) in (( [#] F) \ ( rng f)) by O, X, X4, Lm5;

                    hence contradiction by K5, K, XBOOLE_0:def 5;

                  end;

                  then

                   X3: (b * c) = ((f " ) . (b1 * c1)) by Y, Z, Lm13;

                  ((f " ) . (b1 * c1)) in ( [#] K) by K1, FUNCT_2: 5;

                  then

                  reconsider bc = ((f " ) . (b1 * c1)) as Element of ( carr f) by XBOOLE_0:def 3;

                  reconsider bc1 = (b1 * c1) as Element of ( rng f) by K1;

                  

                  thus ((a * b) * c) = (((f " ) . fa1) * ((f " ) . bc1)) by Th1, X2

                  .= (a1 * ((f " ) . bc1)) by FUNCT_2: 26

                  .= ( multemb (f,x,bc)) by defmultf

                  .= (( multemb f) . (x,bc)) by defmult

                  .= (a * (b * c)) by X3, defemb;

                end;

                  suppose

                   K: not (the multF of F . (ab,z)) in ( rng f);

                  

                   X4: ab <> ( 0. K) by AS, XBOOLE_0:def 4;

                  

                   X2: ((a * b) * c) = (( multemb f) . (ab,z)) by X0, defemb

                  .= ( multemb (f,ab,z)) by defmult

                  .= ((fa * b1) * c1) by O, X4, X1, Z, defmultf, K

                  .= (fa * (b1 * c1)) by GROUP_1:def 3;

                   K1:

                  now

                    assume

                     K7: (the multF of F . (y,z)) in ( rng f);

                    

                     X7: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                    consider x be object such that

                     X6: x in ( dom f) & (b1 * c1) = (f . x) by K7, FUNCT_1:def 3;

                    reconsider xx = x as Element of K by X6;

                    (f . (a1 * xx)) = (fa * (b1 * c1)) by X6, GROUP_6:def 6;

                    hence contradiction by K5, K, X7, FUNCT_1: 3;

                  end;

                  then (b1 * c1) in (( [#] F) \ ( rng f)) by XBOOLE_0:def 5;

                  then

                  reconsider bc = (b1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                  

                   X3: (b * c) = (b1 * c1) by AS, K1, Y, Z, Lm12;

                   not (b1 * c1) in ( [#] K) by AS, XBOOLE_0:def 4;

                  

                  hence ((a * b) * c) = ( multemb (f,x,bc)) by O, X2, defmultf

                  .= (( multemb f) . (x,bc)) by defmult

                  .= (a * (b * c)) by X3, defemb;

                end;

              end;

            end;

          end;

            suppose

             X: not x in ( [#] K);

            then

            reconsider a1 = a as Element of F by Lm1;

            per cases ;

              suppose

               Y: y in ( [#] K);

              then

              reconsider b1 = b as Element of K;

              

               X0: (a * b) = (a1 * (f . b1)) by AS, O, X, Y, Lm10;

              reconsider ab = (a * b) as Element of ( carr f) by defemb;

              reconsider fb = (f . b1) as Element of F;

              

               X2: not ab in ( [#] K) by AS, O, X, Y, Lm10;

              per cases ;

                suppose z in ( [#] K);

                then

                reconsider c1 = c as Element of K;

                reconsider fc = (f . c1) as Element of F;

                

                 X3: (b * c) = (b1 * c1) by Lm11;

                then

                reconsider bc = (b * c) as Element of ( carr f) by XBOOLE_0:def 3;

                

                thus ((a * b) * c) = (( multemb f) . (ab,z)) by defemb

                .= ( multemb (f,ab,z)) by defmult

                .= ((a1 * fb) * fc) by O, X0, X2, defmultf

                .= (a1 * (fb * fc)) by GROUP_1:def 3

                .= (a1 * (f . (b1 * c1))) by GROUP_6:def 6

                .= ( multemb (f,x,bc)) by defmultf, X3, X, O, VECTSP_2:def 1

                .= (( multemb f) . (x,bc)) by defmult

                .= (a * (b * c)) by defemb;

              end;

                suppose

                 Z: not z in ( [#] K);

                then

                reconsider c1 = c as Element of F by Lm1;

                

                 X3: (b * c) = ((f . b1) * c1) by AS, O, Y, Z, Lm10;

                reconsider bc = (b * c) as Element of ( carr f) by defemb;

                

                 X5: not (b * c) in ( [#] K) by AS, O, Y, Z, Lm10;

                

                 K5: (the multF of F . (ab,z)) = ((a1 * fb) * c1) by AS, O, X, Y, Lm10

                .= (a1 * (fb * c1)) by GROUP_1:def 3

                .= (the multF of F . (x,bc)) by AS, O, Y, Z, Lm10;

                per cases ;

                  suppose

                   K: not (the multF of F . (ab,z)) in ( rng f);

                  

                  hence ((a * b) * c) = ((a1 * fb) * c1) by AS, X0, X2, Z, Lm12

                  .= (a1 * (fb * c1)) by GROUP_1:def 3

                  .= (a * (b * c)) by AS, K, K5, X3, X, X5, Lm12;

                end;

                  suppose

                   K: (the multF of F . (ab,z)) in ( rng f);

                  

                  thus ((a * b) * c) = (( multemb f) . (ab,z)) by defemb

                  .= ( multemb (f,ab,z)) by defmult

                  .= ((f " ) . (the multF of F . (ab,z))) by K, X2, Z, defmultf

                  .= ( multemb (f,x,bc)) by K, K5, X, X5, defmultf

                  .= (( multemb f) . (x,bc)) by defmult

                  .= (a * (b * c)) by defemb;

                end;

              end;

            end;

              suppose

               Y: not y in ( [#] K);

              then

              reconsider b1 = b as Element of F by Lm1;

              per cases ;

                suppose

                 K: not (the multF of F . (x,y)) in ( rng f);

                then

                 X0: (a * b) = (a1 * b1) by AS, Y, X, Lm12;

                (a1 * b1) in (( [#] F) \ ( rng f)) by K, XBOOLE_0:def 5;

                then

                reconsider ab = (a1 * b1) as Element of ( carr f) by XBOOLE_0:def 3;

                

                 D: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                per cases ;

                  suppose

                   Z: z in ( [#] K);

                  then

                  reconsider c1 = c as Element of K;

                  

                   X1: (b * c) = (b1 * (f . c1)) by AS, O, Y, Z, Lm10;

                  ( [#] ( embField f)) = ( carr f) by defemb;

                  then

                   X3: (b1 * (f . c1)) in (( [#] F) \ ( rng f)) by O, Y, Lm4;

                  

                   X2: not (b1 * (f . c1)) in ( [#] K) by AS, XBOOLE_0:def 4;

                  reconsider bc = (b1 * (f . c1)) as Element of ( carr f) by X3, XBOOLE_0:def 3;

                  

                   X4: ((a * b) * c) = ((a1 * b1) * (f . c1)) by AS, O, X0, Z, D, Lm10

                  .= (a1 * (b1 * (f . c1))) by GROUP_1:def 3;

                  

                   X5: (the multF of F . (x,bc)) = (a1 * (b1 * (f . c1)))

                  .= ((a1 * b1) * (f . c1)) by GROUP_1:def 3

                  .= (the multF of F . (ab,(f . z)));

                  (the multF of F . (ab,(f . z))) in (( [#] F) \ ( rng f)) by O, D, Lm4, Z;

                  then

                   H: not (the multF of F . (x,bc)) in ( rng f) by X5, XBOOLE_0:def 5;

                  bc <> ( 0. K) by AS, XBOOLE_0:def 4;

                  

                  hence ((a * b) * c) = ( multemb (f,x,bc)) by O, H, X, X2, X4, defmultf

                  .= (( multemb f) . (x,bc)) by defmult

                  .= (a * (b * c)) by X1, defemb;

                end;

                  suppose

                   Z: not z in ( [#] K);

                  then

                  reconsider c1 = c as Element of F by Lm1;

                  

                   K5: (the multF of F . (ab,z)) = ((a1 * b1) * c1)

                  .= (a1 * (b1 * c1)) by GROUP_1:def 3

                  .= (the multF of F . (a1,(b1 * c1)));

                  per cases ;

                    suppose

                     K: not (the multF of F . (ab,z)) in ( rng f);

                    per cases ;

                      suppose

                       K6: not (the multF of F . (b1,c1)) in ( rng f);

                      

                       X1: (b * c) = (( multemb f) . (y,z)) by defemb

                      .= ( multemb (f,y,z)) by defmult

                      .= (b1 * c1) by O, defmultf, Y, Z, K6;

                      

                       K9: (the multF of F . (b1,c1)) in (( [#] F) \ ( rng f)) by K6, XBOOLE_0:def 5;

                      

                       K8: not (b1 * c1) in ( [#] K) by AS, XBOOLE_0:def 4;

                      reconsider bc = (b1 * c1) as Element of ( carr f) by K9, XBOOLE_0:def 3;

                      

                       X4: ab <> ( 0. K) & bc <> ( 0. K) by AS, XBOOLE_0:def 4;

                      

                      thus ((a * b) * c) = (( multemb f) . (ab,z)) by X0, defemb

                      .= ( multemb (f,ab,z)) by defmult

                      .= ((a1 * b1) * c1) by X4, O, D, Z, defmultf, K

                      .= ( multemb (f,x,bc)) by X4, O, X, K5, K, K8, defmultf

                      .= (( multemb f) . (x,bc)) by defmult

                      .= (a * (b * c)) by X1, defemb;

                    end;

                      suppose

                       K6: (the multF of F . (b1,c1)) in ( rng f);

                      

                       X1: (b * c) = (( multemb f) . (y,z)) by defemb

                      .= ( multemb (f,y,z)) by defmult

                      .= ((f " ) . (b1 * c1)) by defmultf, Y, Z, K6;

                      (b1 * c1) in ( dom (f " )) by K6, FUNCT_1: 33;

                      then ((f " ) . (b1 * c1)) in ( rng (f " )) by FUNCT_1: 3;

                      then

                      reconsider bc1 = ((f " ) . (b1 * c1)) as Element of ( [#] K);

                      reconsider bc = bc1 as Element of ( carr f) by XBOOLE_0:def 3;

                      

                       M0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                      (f . ( 0. K)) = ( 0. F) by RING_2: 6;

                      then

                       M1: ( 0. F) in ( rng f) by M0, FUNCT_1:def 3;

                      then

                       M2: c1 <> ( 0. F) by Z, Lm1;

                      b1 <> ( 0. F) by M1, Y, Lm1;

                      then (b1 * c1) <> ( 0. F) by M2, VECTSP_2:def 1;

                      then

                       X4: bc <> ( 0. K) & ab <> ( 0. K) by AS, XBOOLE_0:def 4, K6, Th2;

                      

                      thus ((a * b) * c) = (( multemb f) . (ab,z)) by X0, defemb

                      .= ( multemb (f,ab,z)) by defmult

                      .= ((a1 * b1) * c1) by X4, O, D, Z, defmultf, K

                      .= (a1 * (b1 * c1)) by GROUP_1:def 3

                      .= (a1 * (f . bc1)) by K6, FUNCT_1: 35

                      .= ( multemb (f,x,bc)) by X4, X, defmultf

                      .= (( multemb f) . (x,bc)) by defmult

                      .= (a * (b * c)) by X1, defemb;

                    end;

                  end;

                    suppose

                     K7: (the multF of F . (ab,z)) in ( rng f);

                     K6:

                    now

                      assume (the multF of F . (b1,c1)) in ( rng f);

                      then

                      consider x be object such that

                       H1: x in ( dom f) & (f . x) = (b1 * c1) by FUNCT_1:def 3;

                      consider y be object such that

                       H2: y in ( dom f) & (f . y) = ((a1 * b1) * c1) by K7, FUNCT_1:def 3;

                      reconsider xx = x, yy = y as Element of K by H1, H2;

                      

                       B3h: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                      

                       B3a: a in ( [#] F) & not (a in ( rng f)) by X, Lm1;

                      (f . ( 0. K)) = ( 0. F) by RING_2: 6;

                      then ( 0. F) in ( rng f) by B3h, FUNCT_1:def 3;

                      then

                       OO: a1 <> ( 0. F) & b1 <> ( 0. F) & c1 <> ( 0. F) by X, Y, Z, Lm1;

                      then xx <> ( 0. K) by H1, RING_2: 6, VECTSP_2:def 1;

                      

                      then (f . (xx " )) = ((b1 * c1) " ) by Th5, H1

                      .= ((c1 " ) * (b1 " )) by OO, VECTSP_2: 11

                      .= ((b1 " ) * (c1 " )) by GROUP_1:def 12;

                      

                      then ((f . yy) * (f . (xx " ))) = ((a1 * (b1 * c1)) * ((b1 " ) * (c1 " ))) by H2, GROUP_1:def 3

                      .= (a1 * ((b1 * c1) * ((b1 " ) * (c1 " )))) by GROUP_1:def 3

                      .= (a1 * (b1 * (c1 * ((b1 " ) * (c1 " ))))) by GROUP_1:def 3

                      .= (a1 * (b1 * (c1 * ((c1 " ) * (b1 " ))))) by GROUP_1:def 12

                      .= (a1 * (b1 * ((c1 * (c1 " )) * (b1 " )))) by GROUP_1:def 3

                      .= (a1 * (b1 * (((c1 " ) * c1) * (b1 " )))) by GROUP_1:def 12

                      .= (a1 * (b1 * (( 1. F) * (b1 " )))) by OO, VECTSP_1:def 10

                      .= (a1 * ((b1 " ) * b1)) by GROUP_1:def 12

                      .= (a1 * ( 1. F)) by OO, VECTSP_1:def 10;

                      then

                       B4: a1 = (f . (yy * (xx " ))) by GROUP_6:def 6;

                      ( dom f) = ( [#] K) by FUNCT_2:def 1;

                      hence contradiction by B3a, B4, FUNCT_1:def 3;

                    end;

                    

                     X1: (b * c) = (( multemb f) . (y,z)) by defemb

                    .= ( multemb (f,y,z)) by defmult

                    .= (b1 * c1) by O, defmultf, Y, Z, K6;

                    (b1 * c1) in (( [#] F) \ ( rng f)) by K6, XBOOLE_0:def 5;

                    then

                    reconsider bc = (b1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                    

                     K9: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                    

                    thus ((a * b) * c) = (( multemb f) . (ab,z)) by X0, defemb

                    .= ( multemb (f,ab,z)) by defmult

                    .= ((f " ) . ((a1 * b1) * c1)) by D, Z, defmultf, K7

                    .= ( multemb (f,x,bc)) by X, K5, K7, defmultf, K9

                    .= (( multemb f) . (x,bc)) by defmult

                    .= (a * (b * c)) by X1, defemb;

                  end;

                end;

              end;

                suppose

                 L: (the multF of F . (x,y)) in ( rng f);

                

                 Z1: (a * b) = (( multemb f) . (x,y)) by defemb

                .= ( multemb (f,x,y)) by defmult

                .= ((f " ) . (a1 * b1)) by defmultf, X, Y, L;

                (a1 * b1) in ( dom (f " )) by L, FUNCT_1: 33;

                then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1: 3;

                then

                reconsider ab1 = ((f " ) . (a1 * b1)) as Element of ( [#] K);

                reconsider ab = ab1 as Element of ( carr f) by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   Z: z in ( [#] K);

                  then

                  reconsider c1 = c as Element of K;

                  

                   Z2: (b * c) = (( multemb f) . (y,z)) by defemb

                  .= ( multemb (f,y,z)) by defmult

                  .= (b1 * (f . c1)) by O, defmultf, Y;

                  then

                   L0: (b * c) in (( [#] F) \ ( rng f)) by O, Lm4, Y, Z;

                  reconsider bc1 = (b1 * (f . c1)) as Element of F;

                  reconsider bc = bc1 as Element of ( carr f) by Z2, L0, XBOOLE_0:def 3;

                  

                   Z3: ((a * b) * c) = (( multemb f) . (ab,z)) by Z1, defemb

                  .= ( multemb (f,ab,z)) by defmult

                  .= (ab1 * c1) by defmultf;

                  

                   Z4: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                  

                   Z9: ( dom f) = ( [#] K) & ( rng f) c= ( [#] F) by FUNCT_2:def 1;

                  

                   L2: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                  then

                  reconsider fc1 = (f . c1) as Element of ( rng f) by FUNCT_1:def 3;

                  reconsider ffc1 = ((f " ) . fc1) as Element of K;

                  ((f " ) . fc1) = c1 by L2, FUNCT_1: 34;

                  then

                   Z5: ((f " ) . ((a1 * b1) * fc1)) = (ab1 * c1) by L, Th1;

                  consider x1 be object such that

                   Z6: x1 in ( dom f) & (f . x1) = (a1 * b1) by L, FUNCT_1:def 3;

                  reconsider xx = x1 as Element of K by Z6;

                  (f . (xx * c1)) = ((a1 * b1) * (f . c1)) by Z6, GROUP_6:def 6;

                  then ((a1 * b1) * (f . c1)) in ( rng f) by Z9, FUNCT_1:def 3;

                  then

                   L1: (a1 * (b1 * (f . c1))) in ( rng f) by GROUP_1:def 3;

                  

                  thus (a * (b * c)) = (( multemb f) . (x,bc)) by Z2, defemb

                  .= ( multemb (f,x,bc)) by defmult

                  .= ((f " ) . (a1 * bc1)) by L1, Z4, X, defmultf

                  .= ((a * b) * c) by Z3, Z5, GROUP_1:def 3;

                end;

                  suppose

                   Z: not z in ( [#] K);

                  then

                  reconsider c1 = c as Element of F by Lm1;

                  

                   M0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                  (f . ( 0. K)) = ( 0. F) by RING_2: 6;

                  then

                   M1: ( 0. F) in ( rng f) by M0, FUNCT_1:def 3;

                  then

                   M2: a1 <> ( 0. F) by X, Lm1;

                  b1 <> ( 0. F) by M1, Y, Lm1;

                  then (a1 * b1) <> ( 0. F) by M2, VECTSP_2:def 1;

                  then

                   Z0: ab <> ( 0. K) by L, Th2;

                  

                   Z2: ((a * b) * c) = (( multemb f) . (ab,z)) by Z1, defemb

                  .= ( multemb (f,ab,z)) by defmult

                  .= ((f . ab1) * c1) by Z, Z0, defmultf

                  .= ((a1 * b1) * c1) by L, FUNCT_1: 35

                  .= (a1 * (b1 * c1)) by GROUP_1:def 3;

                  (f . ((f " ) . (a1 * b1))) = (a1 * b1) by FUNCT_1: 35, L;

                  then ((a1 * b1) * c1) in (( [#] F) \ ( rng f)) by Z0, Z, Lm5;

                  then (a1 * (b1 * c1)) in (( [#] F) \ ( rng f)) by GROUP_1:def 3;

                  then

                   U2: not (the multF of F . (a,(b1 * c1))) in ( rng f) by XBOOLE_0:def 5;

                  per cases ;

                    suppose

                     L1: not (the multF of F . (y,z)) in ( rng f);

                    

                     X3: (b * c) = (( multemb f) . (y,z)) by defemb

                    .= ( multemb (f,y,z)) by defmult

                    .= (b1 * c1) by O, L1, Y, Z, defmultf;

                    

                     X4: (b1 * c1) in (( [#] F) \ ( rng f)) by L1, XBOOLE_0:def 5;

                    reconsider bc1 = (b1 * c1) as Element of F;

                    reconsider bc = bc1 as Element of ( carr f) by X4, XBOOLE_0:def 3;

                     not bc in ( [#] K) & bc <> ( 0. K) by AS, XBOOLE_0:def 4;

                    

                    hence ((a * b) * c) = ( multemb (f,x,bc)) by O, Z2, U2, X, defmultf

                    .= (( multemb f) . (x,bc)) by defmult

                    .= (a * (b * c)) by X3, defemb;

                  end;

                    suppose

                     K6: (the multF of F . (y,z)) in ( rng f);

                    

                     X1: (b * c) = (( multemb f) . (y,z)) by defemb

                    .= ( multemb (f,y,z)) by defmult

                    .= ((f " ) . (b1 * c1)) by defmultf, Y, Z, K6;

                    (b1 * c1) in ( dom (f " )) by K6, FUNCT_1: 33;

                    then ((f " ) . (b1 * c1)) in ( rng (f " )) by FUNCT_1: 3;

                    then

                    reconsider bc1 = ((f " ) . (b1 * c1)) as Element of ( [#] K);

                    reconsider bc = bc1 as Element of ( carr f) by XBOOLE_0:def 3;

                    

                     M0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                    (f . ( 0. K)) = ( 0. F) by RING_2: 6;

                    then

                     M1: ( 0. F) in ( rng f) by M0, FUNCT_1:def 3;

                    then

                     M2: c1 <> ( 0. F) by Z, Lm1;

                    b1 <> ( 0. F) by M1, Y, Lm1;

                    then (b1 * c1) <> ( 0. F) by M2, VECTSP_2:def 1;

                    then

                     X2: bc <> ( 0. K) by K6, Th2;

                    

                    thus ((a * b) * c) = (a1 * (f . bc1)) by Z2, K6, FUNCT_1: 35

                    .= ( multemb (f,x,bc)) by X2, X, defmultf

                    .= (( multemb f) . (x,bc)) by defmult

                    .= (a * (b * c)) by X1, defemb;

                  end;

                end;

              end;

            end;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_2:10

    

     Th9: for f be Monomorphism of K, T st (K,T) are_disjoint holds ( embField f) is distributive

    proof

      let f be Monomorphism of K, T;

      assume

       AS: (K,T) are_disjoint ;

      now

        let a,b,c be Element of ( embField f);

        reconsider x = a, y = b, z = c as Element of ( carr f) by defemb;

        per cases ;

          suppose

           A: a = ( 0. K);

          

           A1: (a * b) = (( multemb f) . (x,y)) by defemb

          .= ( multemb (f,x,y)) by defmult

          .= ( 0. K) by A, defmultf;

          

           A2: (a * c) = (( multemb f) . (x,z)) by defemb

          .= ( multemb (f,x,z)) by defmult

          .= ( 0. K) by A, defmultf;

          reconsider bc = (b + c) as Element of ( carr f) by defemb;

          

          thus

           I: (a * (b + c)) = (( multemb f) . (x,(b + c))) by defemb

          .= ( multemb (f,x,bc)) by defmult

          .= ( 0. K) by A, defmultf

          .= ( 0. ( embField f)) by defemb

          .= (( 0. ( embField f)) + ( 0. ( embField f))) by RLVECT_1:def 4

          .= ((a * b) + ( 0. ( embField f))) by A1, defemb

          .= ((a * b) + (a * c)) by A2, defemb;

          

          thus ((b + c) * a) = (a * (b + c)) by GROUP_1:def 12

          .= ((b * a) + (a * c)) by I, GROUP_1:def 12

          .= ((b * a) + (c * a)) by GROUP_1:def 12;

        end;

          suppose

           A: a <> ( 0. K);

          thus

           I: (a * (b + c)) = ((a * b) + (a * c))

          proof

            per cases ;

              suppose

               B: b = ( 0. K);

              

               A1: (a * b) = (( multemb f) . (x,y)) by defemb

              .= ( multemb (f,x,y)) by defmult

              .= ( 0. K) by B, defmultf;

              (b + c) = (( 0. ( embField f)) + c) by B, defemb

              .= c by RLVECT_1:def 4;

              

              hence (a * (b + c)) = (( 0. ( embField f)) + (a * c)) by RLVECT_1:def 4

              .= ((a * b) + (a * c)) by A1, defemb;

            end;

              suppose

               C: c = ( 0. K);

              

               A1: (a * c) = (( multemb f) . (x,z)) by defemb

              .= ( multemb (f,x,z)) by defmult

              .= ( 0. K) by C, defmultf;

              (b + c) = (b + ( 0. ( embField f))) by C, defemb

              .= b by RLVECT_1:def 4;

              

              hence (a * (b + c)) = ((a * b) + ( 0. ( embField f))) by RLVECT_1:def 4

              .= ((a * b) + (a * c)) by A1, defemb;

            end;

              suppose

               BC: b <> ( 0. K) & c <> ( 0. K);

              per cases ;

                suppose

                 X: x in ( [#] K);

                then

                reconsider a1 = a as Element of K;

                per cases ;

                  suppose

                   Y: y in ( [#] K);

                  then

                  reconsider b1 = b as Element of K;

                  

                   A1: (a * b) = (a1 * b1) by Lm11;

                  reconsider ab = (a * b) as Element of ( carr f) by defemb;

                  per cases ;

                    suppose c in ( [#] K);

                    then

                    reconsider c1 = c as Element of K;

                    

                     A2: (a * c) = (a1 * c1) by Lm11;

                    

                     A3: (b + c) = (b1 + c1) by Lm7;

                    reconsider bc = (b + c), ac = (a * c) as Element of ( carr f) by defemb;

                    

                    thus (a * (b + c)) = (a1 * (b1 + c1)) by A3, Lm11

                    .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7

                    .= ((a * b) + (a * c)) by A2, A1, Lm7;

                  end;

                    suppose

                     Z: not z in ( [#] K);

                    then

                    reconsider c1 = c as Element of T by Lm1;

                    

                     A2: (a * c) = ((f . a1) * c1) by AS, X, Z, A, Lm10;

                    

                     A3: (b + c) = ((f . b1) + c1) by AS, Y, Z, Lm6;

                    then

                    reconsider bc = ((f . b1) + c1) as Element of ( carr f) by defemb;

                    reconsider ac = ((f . a1) * c1) as Element of ( carr f) by A2, defemb;

                    

                     A4: not bc in ( [#] K) by AS, A3, Y, Z, Lm6;

                    

                     A5: not ac in ( [#] K) by A2, AS, A, X, Z, Lm10;

                    

                    thus (a * (b + c)) = (( multemb f) . (x,bc)) by A3, defemb

                    .= ( multemb (f,x,bc)) by defmult

                    .= ((f . a1) * ((f . b1) + c1)) by A, A4, defmultf

                    .= (((f . a1) * (f . b1)) + ((f . a1) * c1)) by VECTSP_1:def 7

                    .= ((f . (a1 * b1)) + ((f . a1) * c1)) by GROUP_6:def 6

                    .= ( addemb (f,ab,ac)) by A5, A1, defaddf

                    .= (( addemb f) . (ab,ac)) by defadd

                    .= ((a * b) + (a * c)) by A2, defemb;

                  end;

                end;

                  suppose

                   Y: not y in ( [#] K);

                  then

                  reconsider b1 = b as Element of T by Lm1;

                  

                   A1: (a * b) = ((f . a1) * b1) by AS, X, Y, A, Lm10;

                  then

                  reconsider ab = ((f . a1) * b1) as Element of ( carr f) by defemb;

                  

                   A5: not ab in ( [#] K) by A1, AS, X, Y, A, Lm10;

                  per cases ;

                    suppose

                     Z: z in ( [#] K);

                    then

                    reconsider c1 = c as Element of K;

                    

                     A2: (a * c) = (a1 * c1) by Lm11;

                    

                     A3: (b + c) = (b1 + (f . c1)) by AS, Y, Z, Lm6;

                    reconsider bc = (b + c), ac = (a * c) as Element of ( carr f) by defemb;

                    

                     A4: not bc in ( [#] K) by AS, Y, Z, Lm6;

                    reconsider fc1 = (f . c1) as Element of T;

                    

                    thus (a * (b + c)) = (( multemb f) . (x,bc)) by defemb

                    .= ( multemb (f,x,bc)) by defmult

                    .= ((f . a1) * (b1 + (f . c1))) by A, A3, A4, defmultf

                    .= (((f . a1) * b1) + ((f . a1) * (f . c1))) by VECTSP_1:def 7

                    .= (((f . a1) * b1) + (f . (a1 * c1))) by GROUP_6:def 6

                    .= ( addemb (f,ab,ac)) by A5, A2, defaddf

                    .= (( addemb f) . (ab,ac)) by defadd

                    .= ((a * b) + (a * c)) by A1, defemb;

                  end;

                    suppose

                     Z: not z in ( [#] K);

                    then

                    reconsider c1 = c as Element of T by Lm1;

                    

                     A2: (a * c) = ((f . a1) * c1) by AS, X, Z, A, Lm10;

                    reconsider ac = (a * c) as Element of ( carr f) by defemb;

                    

                     A6: not ac in ( [#] K) by AS, X, Z, A, Lm10;

                    per cases ;

                      suppose

                       Z1: not (the addF of T . (y,z)) in ( rng f);

                      then

                       A3: (b + c) = (b1 + c1) by AS, Y, Z, Lm8;

                      reconsider bc = (b + c) as Element of ( carr f) by defemb;

                      

                       A4: not bc in ( [#] K) by AS, A3, XBOOLE_0:def 4;

                      then

                       A8: (the multF of T . ((f . x),bc)) in (( [#] T) \ ( rng f)) by A, X, Lm5;

                      (the multF of T . ((f . x),bc)) = ((f . a1) * (b1 + c1)) by Z1, AS, Y, Z, Lm8

                      .= (((f . a1) * b1) + ((f . a1) * c1)) by VECTSP_1:def 7

                      .= (the addF of T . (ab,ac)) by AS, X, Z, A, Lm10;

                      then

                       A7: not (the addF of T . (ab,ac)) in ( rng f) by A8, XBOOLE_0:def 5;

                      

                      thus (a * (b + c)) = (( multemb f) . (x,bc)) by defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= ((f . a1) * (b1 + c1)) by A, A3, A4, defmultf

                      .= (((f . a1) * b1) + ((f . a1) * c1)) by VECTSP_1:def 7

                      .= ( addemb (f,ab,ac)) by A2, A5, A6, A7, defaddf

                      .= (( addemb f) . (ab,ac)) by defadd

                      .= ((a * b) + (a * c)) by A1, defemb;

                    end;

                      suppose

                       Z1: (the addF of T . (y,z)) in ( rng f);

                      then

                       A3: (b + c) = ((f " ) . (b1 + c1)) by Y, Z, Lm9;

                      reconsider bc = (b + c), ac = (a * c) as Element of ( carr f) by defemb;

                      

                       A0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                      (b1 + c1) in ( dom (f " )) by Z1, FUNCT_1: 33;

                      then (b + c) in ( rng (f " )) by A3, FUNCT_1: 3;

                      then

                      reconsider bc1 = (b + c) as Element of K;

                      

                       A9: (f . (a1 * bc1)) = ((f . a1) * (f . bc1)) by GROUP_6:def 6

                      .= ((f . a1) * (b1 + c1)) by Z1, A3, FUNCT_1: 35

                      .= (((f . a1) * b1) + ((f . a1) * c1)) by VECTSP_1:def 7;

                      then

                       A4: (the addF of T . (ab,ac)) in ( rng f) by A0, A2, FUNCT_1:def 3;

                      reconsider fa1 = (f . a1) as Element of ( rng f) by A0, FUNCT_1: 3;

                      reconsider fbc1 = (f . bc1) as Element of ( rng f) by A0, FUNCT_1: 3;

                      

                      thus (a * (b + c)) = (( multemb f) . (x,bc)) by defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= (a1 * bc1) by defmultf

                      .= ((f " ) . (((f . a1) * b1) + ((f . a1) * c1))) by A9, A0, FUNCT_1: 34

                      .= ( addemb (f,ab,ac)) by A2, A4, A5, A6, defaddf

                      .= (( addemb f) . (ab,ac)) by defadd

                      .= ((a * b) + (a * c)) by A1, defemb;

                    end;

                  end;

                end;

              end;

                suppose

                 X: not x in ( [#] K);

                then

                reconsider a1 = a as Element of T by Lm1;

                

                 B0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                per cases ;

                  suppose

                   Y: y in ( [#] K);

                  then

                  reconsider b1 = b as Element of K;

                  

                   A1: (a * b) = (a1 * (f . b1)) by AS, X, Y, BC, Lm10;

                  then

                  reconsider ab = (a1 * (f . b1)) as Element of ( carr f) by defemb;

                  

                   A2: not ab in ( [#] K) by A1, AS, X, Y, BC, Lm10;

                  per cases ;

                    suppose

                     Z: z in ( [#] K);

                    then

                    reconsider c1 = c as Element of K;

                    

                     A3: (a * c) = (a1 * (f . c1)) by AS, X, Z, BC, Lm10;

                    then

                    reconsider ac = (a1 * (f . c1)) as Element of ( carr f) by defemb;

                    

                     A4: not ac in ( [#] K) by A3, AS, X, Z, BC, Lm10;

                    

                     A5: (b + c) = (( addemb f) . (y,z)) by defemb

                    .= ( addemb (f,y,z)) by defadd

                    .= (b1 + c1) by defaddf;

                    then

                    reconsider bc1 = (b + c) as Element of K;

                    reconsider bc = (b + c) as Element of ( carr f) by defemb;

                    per cases ;

                      suppose

                       O: bc = ( 0. K);

                      

                       A6: (a * (b + c)) = (( multemb f) . (x,bc)) by defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= ( 0. K) by O, defmultf;

                      ((a1 * (f . b1)) + (a1 * (f . c1))) = (a1 * ((f . b1) + (f . c1))) by VECTSP_1:def 7

                      .= (a1 * (f . (b1 + c1))) by VECTSP_1:def 20

                      .= (a1 * ( 0. T)) by O, RING_2: 6, A5

                      .= (f . ( 0. K)) by RING_2: 6;

                      then

                       A7: ((a1 * (f . b1)) + (a1 * (f . c1))) in ( rng f) by B0, FUNCT_1: 3;

                      ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by A1, A3, defemb

                      .= ( addemb (f,ab,ac)) by defadd

                      .= ((f " ) . ((a1 * (f . b1)) + (a1 * (f . c1)))) by A4, A2, A7, defaddf

                      .= ((f " ) . (a1 * ((f . b1) + (f . c1)))) by VECTSP_1:def 7

                      .= ((f " ) . (a1 * (f . (b1 + c1)))) by VECTSP_1:def 20

                      .= ((f " ) . (a1 * ( 0. T))) by A5, O, RING_2: 6

                      .= ( 0. K) by Th3;

                      hence thesis by A6;

                    end;

                      suppose

                       O: bc <> ( 0. K);

                      then

                       A6: (the multF of T . (x,(f . bc))) in (( [#] T) \ ( rng f)) by A5, X, Lm4;

                      (the multF of T . (x,(f . bc))) = (a1 * ((f . b1) + (f . c1))) by A5, VECTSP_1:def 20

                      .= ((a1 * (f . b1)) + (a1 * (f . c1))) by VECTSP_1:def 7;

                      then

                       A7: not ((a1 * (f . b1)) + (a1 * (f . c1))) in ( rng f) by A6, XBOOLE_0:def 5;

                      

                      thus (a * (b + c)) = (( multemb f) . (x,bc)) by defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= (a1 * (f . bc1)) by O, X, defmultf

                      .= (a1 * ((f . b1) + (f . c1))) by A5, VECTSP_1:def 20

                      .= ((a1 * (f . b1)) + (a1 * (f . c1))) by VECTSP_1:def 7

                      .= ( addemb (f,ab,ac)) by A2, A4, A7, defaddf

                      .= (( addemb f) . (ab,ac)) by defadd

                      .= ((a * b) + (a * c)) by A1, A3, defemb;

                    end;

                  end;

                    suppose

                     Z: not z in ( [#] K);

                    then

                    reconsider c1 = c as Element of T by Lm1;

                    

                     A3: (b + c) = ((f . b1) + c1) by AS, Y, Z, Lm6;

                    then

                    reconsider bc = ((f . b1) + c1) as Element of ( carr f) by defemb;

                    

                     A4: not bc in ( [#] K) by A3, AS, Lm6, Z, Y;

                    

                     A7: (the multF of T . (x,bc)) = (a1 * ((f . b1) + c1))

                    .= ((a1 * (f . b1)) + (a1 * c1)) by VECTSP_1:def 7;

                    per cases ;

                      suppose

                       Z1: (the multF of T . (x,bc)) in ( rng f);

                       A5:

                      now

                        assume (the multF of T . (x,z)) in ( rng f);

                        then

                        consider yy be object such that

                         C1: yy in ( dom f) & (f . yy) = (a1 * c1) by FUNCT_1:def 3;

                        reconsider yy as Element of ( carr f) by C1, XBOOLE_0:def 3;

                        (the addF of T . (ab,(f . yy))) in (( [#] T) \ ( rng f)) by C1, A2, Lm2;

                        hence contradiction by Z1, A7, C1, XBOOLE_0:def 5;

                      end;

                      then

                       A6: (a * c) = (a1 * c1) by AS, X, Z, Lm12;

                      then

                      reconsider ac = (a1 * c1) as Element of ( carr f) by defemb;

                      

                       A9: not ac in ( [#] K) by A6, AS, X, Z, A5, Lm12;

                      

                      thus (a * (b + c)) = (( multemb f) . (x,bc)) by A3, defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= ((f " ) . (a1 * ((f . b1) + c1))) by Z1, A4, X, defmultf

                      .= ( addemb (f,ab,ac)) by defaddf, Z1, A7, A2, A9

                      .= (( addemb f) . (ab,ac)) by defadd

                      .= ((a * b) + (a * c)) by A1, A6, defemb;

                    end;

                      suppose

                       Z1: not (the multF of T . (x,bc)) in ( rng f);

                      

                       A9: not x = ( 0. K) & not bc = ( 0. K) by X, A3, AS, Lm6, Z, Y;

                      

                       A10: (a * (b + c)) = (( multemb f) . (x,bc)) by A3, defemb

                      .= ( multemb (f,x,bc)) by defmult

                      .= (a1 * ((f . b1) + c1)) by X, A4, Z1, A9, defmultf

                      .= ((a1 * (f . b1)) + (a1 * c1)) by VECTSP_1:def 7;

                      per cases ;

                        suppose

                         Z2: (the multF of T . (x,z)) in ( rng f);

                        

                         A7: (a * c) = (( multemb f) . (x,z)) by defemb

                        .= ( multemb (f,x,z)) by defmult

                        .= ((f " ) . (a1 * c1)) by X, Z2, Z, defmultf;

                        then

                        reconsider ac = ((f " ) . (a1 * c1)) as Element of ( carr f) by defemb;

                        (a1 * c1) in ( dom (f " )) by Z2, FUNCT_1: 33;

                        then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                        then

                        reconsider ac1 = ac as Element of K;

                        ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by A1, A7, defemb

                        .= ( addemb (f,ab,ac)) by defadd

                        .= ((a1 * (f . b1)) + (f . ac1)) by defaddf, A2;

                        hence thesis by A10, Z2, FUNCT_1: 35;

                      end;

                        suppose

                         Z2: not (the multF of T . (x,z)) in ( rng f);

                        

                         A9: (a * c) = (( multemb f) . (x,z)) by defemb

                        .= ( multemb (f,x,z)) by defmult

                        .= (a1 * c1) by X, Z2, A, BC, Z, defmultf;

                        then

                        reconsider ac = (a1 * c1) as Element of ( carr f) by defemb;

                        

                         A8: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                        

                        thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by A1, A9, defemb

                        .= ( addemb (f,ab,ac)) by defadd

                        .= (a * (b + c)) by defaddf, A2, A7, A8, Z1, A10;

                      end;

                    end;

                  end;

                end;

                  suppose

                   Y: not y in ( [#] K);

                  then

                  reconsider b1 = b as Element of T by Lm1;

                  per cases ;

                    suppose

                     Z: z in ( [#] K);

                    then

                    reconsider c1 = c as Element of K;

                    

                     B1: (b + c) = (b1 + (f . c1)) by AS, Y, Z, Lm6;

                    then

                    reconsider bc = (b1 + (f . c1)) as Element of ( carr f) by defemb;

                    

                     B2: not bc in ( [#] K) by Y, Z, AS, Lm6, B1;

                    

                     B3: (a * c) = (a1 * (f . c1)) by AS, X, Z, BC, Lm10;

                    then

                    reconsider ac = (a1 * (f . c1)) as Element of ( carr f) by defemb;

                    

                     B4: not ac in ( [#] K) by B3, X, Z, BC, AS, Lm10;

                    per cases ;

                      suppose

                       Z1: not (the multF of T . (x,y)) in ( rng f);

                      

                       B5: (a * b) = (( multemb f) . (x,y)) by defemb

                      .= ( multemb (f,x,y)) by defmult

                      .= (a1 * b1) by Z1, X, Y, A, BC, defmultf;

                      then

                      reconsider ab = (a1 * b1) as Element of ( carr f) by defemb;

                      

                       B6: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                      

                       Z3: (the addF of T . (ab,ac)) = ((a1 * b1) + (a1 * (f . c1)))

                      .= (a1 * (b1 + (f . c1))) by VECTSP_1:def 7

                      .= (the multF of T . (x,bc));

                      per cases ;

                        suppose

                         Z2: (the multF of T . (x,bc)) in ( rng f);

                        

                        thus (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= ((f " ) . (a1 * (b1 + (f . c1)))) by Z2, B2, X, defmultf

                        .= ( addemb (f,ab,ac)) by defaddf, Z2, Z3, B4, B6

                        .= (( addemb f) . (ab,ac)) by defadd

                        .= ((a * b) + (a * c)) by B3, B5, defemb;

                      end;

                        suppose

                         Z2: not (the multF of T . (x,bc)) in ( rng f);

                        

                         B7: x <> ( 0. K) & bc <> ( 0. K) by X, Y, Z, AS, Lm6, B1;

                        

                        thus (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= (a1 * (b1 + (f . c1))) by B7, X, B2, Z2, defmultf

                        .= ( addemb (f,ab,ac)) by defaddf, Z2, Z3, B4, B6

                        .= (( addemb f) . (ab,ac)) by defadd

                        .= ((a * b) + (a * c)) by B3, B5, defemb;

                      end;

                    end;

                      suppose

                       Z1: (the multF of T . (x,y)) in ( rng f);

                      

                       B5: (a * b) = (( multemb f) . (x,y)) by defemb

                      .= ( multemb (f,x,y)) by defmult

                      .= ((f " ) . (a1 * b1)) by Z1, X, Y, defmultf;

                      (a1 * b1) in ( dom (f " )) by Z1, FUNCT_1: 33;

                      then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

                      then

                      reconsider ab1 = ((f " ) . (a1 * b1)) as Element of K;

                      reconsider ab = ab1 as Element of ( carr f) by B5, defemb;

                      (the addF of T . ((f . ab),ac)) in (( [#] T) \ ( rng f)) by Lm3, B4;

                      then

                       B7: not (the addF of T . ((f . ab),ac)) in ( rng f) by XBOOLE_0:def 5;

                       B9:

                      now

                        assume (the multF of T . (x,bc)) in ( rng f);

                        then

                        consider yy be object such that

                         C1: yy in ( dom f) & (f . yy) = (a1 * (b1 + (f . c1))) by FUNCT_1:def 3;

                        (f . yy) = ((a1 * b1) + (a1 * (f . c1))) by C1, VECTSP_1:def 7

                        .= ((f . ab1) + (a1 * (f . c1))) by Z1, FUNCT_1: 35;

                        hence contradiction by B7, C1, FUNCT_1:def 3;

                      end;

                      

                       B10: a <> ( 0. K) & bc <> ( 0. K) by X, Y, Z, AS, Lm6, B1;

                      

                      thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B5, B3, defemb

                      .= ( addemb (f,ab,ac)) by defadd

                      .= ((f . ab1) + (a1 * (f . c1))) by defaddf, B4

                      .= ((a1 * b1) + (a1 * (f . c1))) by Z1, FUNCT_1: 35

                      .= (a1 * (b1 + (f . c1))) by VECTSP_1:def 7

                      .= ( multemb (f,x,bc)) by B10, X, B2, B9, defmultf

                      .= (( multemb f) . (x,bc)) by defmult

                      .= (a * (b + c)) by B1, defemb;

                    end;

                  end;

                    suppose

                     Z: not z in ( [#] K);

                    then

                    reconsider c1 = c as Element of T by Lm1;

                    per cases ;

                      suppose

                       Z1: (the addF of T . (y,z)) in ( rng f);

                      

                       B1: (b + c) = (( addemb f) . (y,z)) by defemb

                      .= ( addemb (f,y,z)) by defadd

                      .= ((f " ) . (b1 + c1)) by Y, Z, Z1, defaddf;

                      (b1 + c1) in ( dom (f " )) by Z1, FUNCT_1: 33;

                      then ((f " ) . (b1 + c1)) in ( rng (f " )) by FUNCT_1:def 3;

                      then

                      reconsider bc1 = ((f " ) . (b1 + c1)) as Element of K;

                      reconsider bc = bc1 as Element of ( carr f) by B1, defemb;

                      

                       B0: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                      per cases ;

                        suppose

                         B5: bc = ( 0. K);

                        then

                         B2: (b1 + c1) = ( 0. T) by Z1, Th2;

                        

                         B3: (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= ( 0. K) by B5, defmultf;

                        

                         A6: ((a1 * b1) + (a1 * c1)) = (a1 * ( 0. T)) by B2, VECTSP_1:def 7

                        .= (f . ( 0. K)) by RING_2: 6;

                        then

                         A7: ((a1 * b1) + (a1 * c1)) in ( rng f) by B0, FUNCT_1: 3;

                        per cases ;

                          suppose

                           Z2: (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= ((f " ) . (a1 * b1)) by Y, X, Z2, defmultf;

                          (a1 * b1) in ( dom (f " )) by Z2, FUNCT_1: 33;

                          then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ab1 = ((f " ) . (a1 * b1)) as Element of K;

                          reconsider ab = ab1 as Element of ( carr f) by B4, defemb;

                          

                           U: (f . (( 0. K) - ab1)) = ((f . ( 0. K)) - (f . ab1)) by RING_2: 8

                          .= (((a1 * b1) + (a1 * c1)) - (a1 * b1)) by A6, Z2, FUNCT_1: 35

                          .= ((a1 * c1) + ((a1 * b1) - (a1 * b1))) by RLVECT_1:def 3

                          .= ((a1 * c1) + ( 0. T)) by RLVECT_1: 15

                          .= (the multF of T . (x,z));

                          then

                           Z3: (the multF of T . (x,z)) in ( rng f) by B0, FUNCT_1:def 3;

                          

                           B5: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= ((f " ) . (a1 * c1)) by Z, X, Z3, defmultf;

                          

                           B11: (a1 * c1) in ( rng f) by U, B0, FUNCT_1:def 3;

                          then (a1 * c1) in ( dom (f " )) by FUNCT_1: 33;

                          then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                          reconsider ac = ac1 as Element of ( carr f) by B5, defemb;

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B5, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= (ab1 + ac1) by defaddf

                          .= ((f " ) . ((a1 * b1) + (a1 * c1))) by B11, Z2, Th1

                          .= (a * (b + c)) by A6, B3, B0, FUNCT_1: 34;

                        end;

                          suppose

                           Z2: not (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= (a1 * b1) by A, BC, Y, X, Z2, defmultf;

                          (a1 * b1) in (( [#] T) \ ( rng f)) by Z2, XBOOLE_0:def 5;

                          then

                          reconsider ab = (a1 * b1) as Element of ( carr f) by XBOOLE_0:def 3;

                          

                           B9: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                           Z3:

                          now

                            assume

                             Z3: (the multF of T . (x,z)) in ( rng f);

                            

                             B5: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= ((f " ) . (a1 * c1)) by Z, X, Z3, defmultf;

                            (a1 * c1) in ( dom (f " )) by Z3, FUNCT_1: 33;

                            then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                            then

                            reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                            reconsider ac = ac1 as Element of ( carr f) by B5, defemb;

                            

                             B12: (the addF of T . (ab,(f . ac))) in (( [#] T) \ ( rng f)) by B9, Lm2;

                            (the addF of T . (ab,(f . ac))) = ((a1 * b1) + (a1 * c1)) by Z3, FUNCT_1: 35;

                            hence contradiction by B12, A7, XBOOLE_0:def 5;

                          end;

                          

                           B5: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= (a1 * c1) by A, BC, Z, X, Z3, defmultf;

                          (a1 * c1) in (( [#] T) \ ( rng f)) by Z3, XBOOLE_0:def 5;

                          then

                          reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                          

                           B13: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B5, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= ((f " ) . ((a1 * b1) + (a1 * c1))) by A7, B9, B13, defaddf

                          .= (a * (b + c)) by A6, B3, B0, FUNCT_1: 34;

                        end;

                      end;

                        suppose

                         B5: bc <> ( 0. K);

                        then

                         B12: (the multF of T . (x,(f . bc))) in (( [#] T) \ ( rng f)) by X, Lm4;

                        

                         B3: (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= (a1 * (f . bc1)) by B5, X, defmultf

                        .= (a1 * (b1 + c1)) by Z1, FUNCT_1: 35

                        .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7;

                        per cases ;

                          suppose

                           Z2: (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= ((f " ) . (a1 * b1)) by Y, X, Z2, defmultf;

                          (a1 * b1) in ( dom (f " )) by Z2, FUNCT_1: 33;

                          then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ab1 = ((f " ) . (a1 * b1)) as Element of K;

                          reconsider ab = ab1 as Element of ( carr f) by B4, defemb;

                           B7:

                          now

                            assume (the multF of T . (x,z)) in ( rng f);

                            then

                            consider xx be object such that

                             C1: xx in ( dom f) & (f . xx) = (a1 * c1) by FUNCT_1:def 3;

                            reconsider xx as Element of K by C1;

                            consider yy be object such that

                             C2: yy in ( dom f) & (f . yy) = (a1 * b1) by Z2, FUNCT_1:def 3;

                            reconsider yy as Element of K by C2;

                            

                             C3: ( dom f) = ( [#] K) by FUNCT_2:def 1;

                            (the multF of T . (x,(f . bc))) = (a1 * (b1 + c1)) by Z1, FUNCT_1: 35

                            .= ((f . yy) + (f . xx)) by C1, C2, VECTSP_1:def 7

                            .= (f . (xx + yy)) by VECTSP_1:def 20;

                            then (the multF of T . (x,(f . bc))) in ( rng f) by C3, FUNCT_1:def 3;

                            hence contradiction by B12, XBOOLE_0:def 5;

                          end;

                          

                           B8: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= (a1 * c1) by Z, B7, A, BC, X, defmultf;

                          (a1 * c1) in (( [#] T) \ ( rng f)) by B7, XBOOLE_0:def 5;

                          then

                          reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                          

                           B9: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B8, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= ((f . ab1) + (a1 * c1)) by defaddf, B9

                          .= (a * (b + c)) by B3, Z2, FUNCT_1: 35;

                        end;

                          suppose

                           Z2: not (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= (a1 * b1) by A, BC, Y, X, Z2, defmultf;

                          then

                          reconsider ab = (a1 * b1) as Element of ( carr f) by defemb;

                          

                           B5: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                          per cases ;

                            suppose

                             Z3: (the multF of T . (x,z)) in ( rng f);

                            

                             B8: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= ((f " ) . (a1 * c1)) by Z, X, Z3, defmultf;

                            (a1 * c1) in ( dom (f " )) by Z3, FUNCT_1: 33;

                            then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                            then

                            reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                            reconsider ac = ac1 as Element of ( carr f) by B8, defemb;

                            

                            thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B8, defemb

                            .= ( addemb (f,ab,ac)) by defadd

                            .= ((a1 * b1) + (f . ac1)) by defaddf, B5

                            .= (a * (b + c)) by B3, Z3, FUNCT_1: 35;

                          end;

                            suppose

                             Z3: not (the multF of T . (x,z)) in ( rng f);

                            

                             B8: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= (a1 * c1) by Z, Z3, A, BC, X, defmultf;

                            (a1 * c1) in (( [#] T) \ ( rng f)) by Z3, XBOOLE_0:def 5;

                            then

                            reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                            

                             B9: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                            (the multF of T . (x,(f . bc))) = (a1 * (b1 + c1)) by Z1, FUNCT_1: 35

                            .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7

                            .= (the addF of T . (ab,ac));

                            then

                             B10: not (the addF of T . (ab,ac)) in ( rng f) by B12, XBOOLE_0:def 5;

                            

                            thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B8, defemb

                            .= ( addemb (f,ab,ac)) by defadd

                            .= (a * (b + c)) by defaddf, B9, B5, B10, B3;

                          end;

                        end;

                      end;

                    end;

                      suppose

                       Z1: not (the addF of T . (y,z)) in ( rng f);

                      

                       B1: (b + c) = (( addemb f) . (y,z)) by defemb

                      .= ( addemb (f,y,z)) by defadd

                      .= (b1 + c1) by Y, Z, Z1, defaddf;

                      (b1 + c1) in (( [#] T) \ ( rng f)) by Z1, XBOOLE_0:def 5;

                      then

                      reconsider bc = (b1 + c1) as Element of ( carr f) by XBOOLE_0:def 3;

                      

                       B2: not bc in ( [#] K) by AS, XBOOLE_0:def 4;

                      

                       B5: not bc = ( 0. K) by AS, XBOOLE_0:def 4;

                      per cases ;

                        suppose

                         Z2: (the multF of T . (x,bc)) in ( rng f);

                        

                         B3: (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= ((f " ) . (a1 * (b1 + c1))) by Z2, B2, X, defmultf

                        .= ((f " ) . ((a1 * b1) + (a1 * c1))) by VECTSP_1:def 7;

                        per cases ;

                          suppose

                           Z3: (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= ((f " ) . (a1 * b1)) by Y, X, Z3, defmultf;

                          (a1 * b1) in ( dom (f " )) by Z3, FUNCT_1: 33;

                          then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ab1 = ((f " ) . (a1 * b1)) as Element of K;

                          reconsider ab = ab1 as Element of ( carr f) by B4, defemb;

                          

                           B6: (the multF of T . (x,z)) in ( rng f)

                          proof

                            (the multF of T . (x,bc)) = (a1 * (b1 + c1))

                            .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7;

                            then

                            consider xx be object such that

                             C1: xx in ( dom f) & (f . xx) = ((a1 * b1) + (a1 * c1)) by Z2, FUNCT_1:def 3;

                            reconsider xx as Element of K by C1;

                            consider yy be object such that

                             C2: yy in ( dom f) & (f . yy) = (a1 * b1) by Z3, FUNCT_1:def 3;

                            reconsider yy as Element of K by C2;

                            

                             C3: (f . (xx - yy)) = ((f . xx) - (f . yy)) by RING_2: 8

                            .= ((a1 * c1) + ((a1 * b1) + ( - (a1 * b1)))) by C1, C2, RLVECT_1:def 3

                            .= ((a1 * c1) + ( 0. T)) by RLVECT_1: 5;

                            ( [#] K) = ( dom f) by FUNCT_2:def 1;

                            hence thesis by C3, FUNCT_1:def 3;

                          end;

                          

                           B7: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= ((f " ) . (a1 * c1)) by X, Z, B6, defmultf;

                          (a1 * c1) in ( dom (f " )) by B6, FUNCT_1: 33;

                          then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                          reconsider ac = ac1 as Element of ( carr f) by B7, defemb;

                          reconsider abr = (a1 * b1) as Element of ( rng f) by Z3;

                          reconsider acr = (a1 * c1) as Element of ( rng f) by B6;

                          

                           B8: (((f " ) . abr) + ((f " ) . acr)) = ((f " ) . ((a1 * b1) + (a1 * c1))) by Th1;

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B7, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= (a * (b + c)) by defaddf, B8, B3;

                        end;

                          suppose

                           Z3: not (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= (a1 * b1) by A, BC, Y, X, Z3, defmultf;

                          (a1 * b1) in (( [#] T) \ ( rng f)) by Z3, XBOOLE_0:def 5;

                          then

                          reconsider ab = (a1 * b1) as Element of ( carr f) by XBOOLE_0:def 3;

                          reconsider ab1 = ab as Element of T;

                          

                           B6: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                           Z4:

                          now

                            assume

                             Z4a: (the multF of T . (x,z)) in ( rng f);

                            

                             B7: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= ((f " ) . (a1 * c1)) by Z4a, X, Z, defmultf;

                            (a1 * c1) in ( dom (f " )) by Z4a, FUNCT_1: 33;

                            then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                            then

                            reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                            reconsider ac = ac1 as Element of ( carr f) by B7, defemb;

                            

                             U: (the addF of T . (ab,(f . ac))) in (( [#] T) \ ( rng f)) by B6, Lm2;

                            (f . ac1) = (a1 * c1) by Z4a, FUNCT_1: 35;

                            

                            then (ab1 + (f . ac1)) = (a1 * (b1 + c1)) by VECTSP_1:def 7

                            .= (the multF of T . (x,bc));

                            hence contradiction by U, Z2, XBOOLE_0:def 5;

                          end;

                          

                           B7: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= (a1 * c1) by Z4, A, BC, X, Z, defmultf;

                          (a1 * c1) in (( [#] T) \ ( rng f)) by Z4, XBOOLE_0:def 5;

                          then

                          reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                          reconsider ac1 = ac as Element of T;

                          

                           B9: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                          

                           B10: ((a1 * b1) + (a1 * c1)) = (a1 * (b1 + c1)) by VECTSP_1:def 7

                          .= (the multF of T . (x,bc));

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B7, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= (a * (b + c)) by defaddf, B6, B9, B10, Z2, B3;

                        end;

                      end;

                        suppose

                         Z2: not (the multF of T . (x,bc)) in ( rng f);

                        

                         B3: (a * (b + c)) = (( multemb f) . (x,bc)) by B1, defemb

                        .= ( multemb (f,x,bc)) by defmult

                        .= (a1 * (b1 + c1)) by A, Z2, B2, B5, X, defmultf

                        .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7;

                        per cases ;

                          suppose

                           Z3: (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= ((f " ) . (a1 * b1)) by Y, X, Z3, defmultf;

                          (a1 * b1) in ( dom (f " )) by Z3, FUNCT_1: 33;

                          then ((f " ) . (a1 * b1)) in ( rng (f " )) by FUNCT_1:def 3;

                          then

                          reconsider ab1 = ((f " ) . (a1 * b1)) as Element of K;

                          reconsider ab = ab1 as Element of ( carr f) by B4, defemb;

                           Z4:

                          now

                            assume (the multF of T . (x,z)) in ( rng f);

                            then

                            consider yy be object such that

                             C1: yy in ( dom f) & (f . yy) = (a1 * c1) by FUNCT_1:def 3;

                            reconsider yy as Element of K by C1;

                            

                             C2: (the multF of T . (x,bc)) = (a1 * (b1 + c1))

                            .= ((a1 * b1) + (a1 * c1)) by VECTSP_1:def 7;

                            

                             C3: (f . (ab1 + yy)) = ((f . ab1) + (f . yy)) by VECTSP_1:def 20

                            .= ((a1 * b1) + (a1 * c1)) by C1, Z3, FUNCT_1: 35;

                            ( [#] K) = ( dom f) by FUNCT_2:def 1;

                            hence contradiction by C3, C2, Z2, FUNCT_1:def 3;

                          end;

                          

                           B5: (a * c) = (( multemb f) . (x,z)) by defemb

                          .= ( multemb (f,x,z)) by defmult

                          .= (a1 * c1) by A, BC, Z, X, Z4, defmultf;

                          (a1 * c1) in (( [#] T) \ ( rng f)) by Z4, XBOOLE_0:def 5;

                          then

                          reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                          

                           B9: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                          

                          thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B5, defemb

                          .= ( addemb (f,ab,ac)) by defadd

                          .= ((f . ab1) + (a1 * c1)) by defaddf, B9

                          .= (a * (b + c)) by B3, Z3, FUNCT_1: 35;

                        end;

                          suppose

                           Z3: not (the multF of T . (x,y)) in ( rng f);

                          

                           B4: (a * b) = (( multemb f) . (x,y)) by defemb

                          .= ( multemb (f,x,y)) by defmult

                          .= (a1 * b1) by A, BC, Y, X, Z3, defmultf;

                          (a1 * b1) in (( [#] T) \ ( rng f)) by Z3, XBOOLE_0:def 5;

                          then

                          reconsider ab = (a1 * b1) as Element of ( carr f) by XBOOLE_0:def 3;

                          

                           B9: not ab in ( [#] K) by AS, XBOOLE_0:def 4;

                          per cases ;

                            suppose

                             Z4: (the multF of T . (x,z)) in ( rng f);

                            

                             B5: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= ((f " ) . (a1 * c1)) by Z, X, Z4, defmultf;

                            (a1 * c1) in ( dom (f " )) by Z4, FUNCT_1: 33;

                            then ((f " ) . (a1 * c1)) in ( rng (f " )) by FUNCT_1:def 3;

                            then

                            reconsider ac1 = ((f " ) . (a1 * c1)) as Element of K;

                            reconsider ac = ac1 as Element of ( carr f) by B5, defemb;

                            

                            thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B5, defemb

                            .= ( addemb (f,ab,ac)) by defadd

                            .= ((a1 * b1) + (f . ac1)) by defaddf, B9

                            .= (a * (b + c)) by B3, Z4, FUNCT_1: 35;

                          end;

                            suppose

                             Z4: not (the multF of T . (x,z)) in ( rng f);

                            

                             B5: (a * c) = (( multemb f) . (x,z)) by defemb

                            .= ( multemb (f,x,z)) by defmult

                            .= (a1 * c1) by A, BC, Z, X, Z4, defmultf;

                            (a1 * c1) in (( [#] T) \ ( rng f)) by Z4, XBOOLE_0:def 5;

                            then

                            reconsider ac = (a1 * c1) as Element of ( carr f) by XBOOLE_0:def 3;

                            

                             B19: not ac in ( [#] K) by AS, XBOOLE_0:def 4;

                            

                             B20: (the addF of T . (ab,ac)) = ((a1 * b1) + (a1 * c1))

                            .= (a1 * (b1 + c1)) by VECTSP_1:def 7

                            .= (the multF of T . (x,bc));

                            

                            thus ((a * b) + (a * c)) = (( addemb f) . (ab,ac)) by B4, B5, defemb

                            .= ( addemb (f,ab,ac)) by defadd

                            .= (a * (b + c)) by Z2, B3, B9, B19, B20, defaddf;

                          end;

                        end;

                      end;

                    end;

                  end;

                end;

              end;

            end;

          end;

          

          thus ((b + c) * a) = (a * (b + c)) by GROUP_1:def 12

          .= ((b * a) + (a * c)) by I, GROUP_1:def 12

          .= ((b * a) + (c * a)) by GROUP_1:def 12;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_2:11

    

     Th10: for f be Monomorphism of K, F st (K,F) are_disjoint holds ( embField f) is almost_left_invertible

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      now

        let a be Element of ( embField f);

        assume a <> ( 0. ( embField f));

        then

         X: a <> ( 0. K) by defemb;

        reconsider x = a as Element of ( carr f) by defemb;

        per cases ;

          suppose x in ( [#] K);

          then

          reconsider a1 = a as Element of K;

          a1 is left_invertible by X, ALGSTR_0:def 39;

          then

          consider b1 be Element of K such that

           B: (b1 * a1) = ( 1. K);

          reconsider y = b1 as Element of ( carr f) by XBOOLE_0:def 3;

          reconsider b = y as Element of ( embField f) by defemb;

          (b * a) = (a * b) by GROUP_1:def 12

          .= (a1 * b1) by Lm11

          .= (b1 * a1) by GROUP_1:def 12

          .= ( 1. ( embField f)) by B, defemb;

          hence a is left_invertible;

        end;

          suppose

           A: not x in ( [#] K);

          then

           X: x in ( [#] F) & not x in ( rng f) by Lm1;

          reconsider a1 = a as Element of F by A, Lm1;

          

           Z: ( dom f) = ( [#] K) by FUNCT_2:def 1;

          (f . ( 0. K)) = ( 0. F) by RING_2: 6;

          then ( 0. F) in ( rng f) by Z, FUNCT_1:def 3;

          then a1 is left_invertible by X, ALGSTR_0:def 39;

          then

          consider b1 be Element of F such that

           B: (b1 * a1) = ( 1. F);

          

           U: b1 <> ( 0. F) & a1 <> ( 0. F) by B;

          (the multF of F . (a1,b1)) = (a1 * b1)

          .= ( 1_ F) by B, GROUP_1:def 12

          .= (f . ( 1_ K)) by GROUP_1:def 13;

          then

           D: (the multF of F . (a1,b1)) in ( rng f) by Z, FUNCT_1: 3;

          then

           D1: not (the multF of F . (a1,b1)) in (( [#] F) \ ( rng f)) by XBOOLE_0:def 5;

          per cases ;

            suppose b1 in ( rng f);

            then

            consider b1r be object such that

             C1: b1r in ( dom f) & (f . b1r) = b1 by FUNCT_1:def 3;

            reconsider b1r as Element of K by C1;

            ( [#] ( embField f)) = ( carr f) by defemb;

            then

            reconsider bx = b1r as Element of ( embField f) by XBOOLE_0:def 3;

            reconsider y = bx as Element of ( carr f) by defemb;

            

             C4: bx <> ( 0. K) by U, C1, RING_2: 6;

            ( [#] ( embField f)) = ( carr f) by defemb;

            hence a is left_invertible by Lm4, A, D1, C1, C4;

          end;

            suppose not b1 in ( rng f);

            then b1 in (( [#] F) \ ( rng f)) by XBOOLE_0:def 5;

            then b1 is Element of ( carr f) by XBOOLE_0:def 3;

            then

            reconsider b = b1 as Element of ( embField f) by defemb;

            

             E: not b in ( [#] K) by AS, XBOOLE_0:def 4;

            (b * a) = (a * b) by GROUP_1:def 12

            .= ((f " ) . (a1 * b1)) by A, D, E, Lm13

            .= ((f " ) . ( 1_ F)) by B, GROUP_1:def 12

            .= ( 1. K) by Th3

            .= ( 1. ( embField f)) by defemb;

            hence a is left_invertible;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_2:12

    for f be Monomorphism of K, F st (K,F) are_disjoint holds ( embField f) is Field by Th6, Th8, Th9, Th7, Th10;

    definition

      let K be Field;

      let F be K -monomorphic Field;

      let f be Monomorphism of K, F;

      :: FIELD_2:def8

      func emb_iso f -> Function of ( embField f), F means

      : defiso: (for a be Element of ( embField f) st not a in K holds (it . a) = a) & (for a be Element of ( embField f) st a in K holds (it . a) = (f . a));

      existence

      proof

        defpred P[ object, object] means ( not $1 in K & $2 = $1) or ($1 in K & $2 = (f . $1));

        

         M: for x be object st x in ( [#] ( embField f)) holds ex y be object st y in ( [#] F) & P[x, y]

        proof

          let x be object;

          assume

           M0: x in ( [#] ( embField f));

          then

          reconsider x1 = x as Element of ( embField f);

          per cases ;

            suppose

             M1: x in K;

            then

            reconsider a = x as Element of K;

            take b = (f . a);

            thus b in ( [#] F);

            thus thesis by M1;

          end;

            suppose

             M1: not x in K;

            take x;

            reconsider x1 = x as Element of ( carr f) by M0, defemb;

            x1 in ( [#] F) & not x1 in ( rng f) by M1, Lm1;

            hence x in ( [#] F);

            thus thesis by M1;

          end;

        end;

        consider g be Function of ( [#] ( embField f)), ( [#] F) such that

         N: for x be object st x in ( [#] ( embField f)) holds P[x, (g . x)] from FUNCT_2:sch 1( M);

        reconsider g as Function of ( embField f), F;

        take g;

        thus thesis by N;

      end;

      uniqueness

      proof

        let g1,g2 be Function of ( embField f), F;

        assume that

         A1: (for a be Element of ( embField f) st not a in K holds (g1 . a) = a) & (for a be Element of ( embField f) st a in K holds (g1 . a) = (f . a)) and

         A2: (for a be Element of ( embField f) st not a in K holds (g2 . a) = a) & (for a be Element of ( embField f) st a in K holds (g2 . a) = (f . a));

        now

          let o be object;

          assume o in ( [#] ( embField f));

          then

          reconsider a = o as Element of ( embField f);

          per cases ;

            suppose

             A3: a in K;

            

            then (g1 . a) = (f . a) by A1

            .= (g2 . a) by A3, A2;

            hence (g1 . o) = (g2 . o);

          end;

            suppose

             A3: not a in K;

            

            then (g1 . a) = a by A1

            .= (g2 . a) by A3, A2;

            hence (g1 . o) = (g2 . o);

          end;

        end;

        hence g1 = g2;

      end;

    end

    registration

      let K be Field, F be K -monomorphic Field;

      let f be Monomorphism of K, F;

      cluster ( emb_iso f) -> unity-preserving;

      coherence

      proof

        set g = ( emb_iso f), R = ( embField f);

        ( 1. R) = ( 1. K) by defemb;

        then ( 1. R) in K;

        

        then (g . ( 1_ R)) = (f . ( 1. R)) by defiso

        .= (f . ( 1_ K)) by defemb

        .= ( 1_ F) by GROUP_1:def 13;

        hence g is unity-preserving;

      end;

    end

    theorem :: FIELD_2:13

    

     Th11: for f be Monomorphism of K, F st (K,F) are_disjoint holds ( emb_iso f) is additive

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      set g = ( emb_iso f), R = ( embField f);

      now

        let a,b be Element of R;

        reconsider x = a, y = b as Element of ( carr f) by defemb;

        per cases ;

          suppose

           A: x in ( [#] K) & y in ( [#] K);

          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: (g . a) = (f . a) & (g . b) = (f . b) by defiso;

          (a + b) in K by B;

          

          hence (g . (a + b)) = (f . (a + b)) by defiso

          .= ((g . a) + (g . b)) by C, B, VECTSP_1:def 20;

        end;

          suppose

           A: x in ( [#] K) & not y in ( [#] K);

          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: (g . a) = (f . a) & (g . b) = b by defiso;

           not (fa + b1) in K by AS, XBOOLE_0:def 4;

          hence (g . (a + b)) = ((g . a) + (g . b)) by C, B, defiso;

        end;

          suppose

           A: y in ( [#] K) & not x in ( [#] K);

          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: (g . a) = a & (g . b) = (f . b) by defiso;

           not (a1 + fb) in K by AS, XBOOLE_0:def 4;

          hence (g . (a + b)) = ((g . a) + (g . b)) by C, B, defiso;

        end;

          suppose

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

          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: (g . a) = a & (g . 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 (g . (a + b)) = (f . ((f " ) . (a1 + b1))) by C, defiso

          .= ((g . a) + (g . b)) by D, A, FUNCT_1: 35;

        end;

          suppose

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

          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: (g . a) = a & (g . b) = b by defiso;

           not (a1 + b1) in K by AS, XBOOLE_0:def 4;

          hence (g . (a + b)) = ((g . a) + (g . b)) by D, C, defiso;

        end;

      end;

      hence g is additive;

    end;

    theorem :: FIELD_2:14

    

     Th12: for f be Monomorphism of K, F st (K,F) are_disjoint holds ( emb_iso f) is multiplicative

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      set g = ( emb_iso f), R = ( embField f);

      now

        let a,b be Element of R;

        reconsider x = a, y = b as Element of ( carr f) by defemb;

        per cases ;

          suppose

           A1: x in ( [#] K) & y in ( [#] K);

          then

          reconsider a1 = a, b1 = b as Element of K;

          

           B: (a * b) = (a1 * b1) by Lm11;

          a in K & b in K by A1;

          then

           C: (g . a) = (f . a) & (g . b) = (f . b) by defiso;

          (a * b) in K by B;

          

          hence (g . (a * b)) = (f . (a * b)) by defiso

          .= ((g . a) * (g . b)) by C, B, GROUP_6:def 6;

        end;

          suppose

           A2: x = ( 0. K) or y = ( 0. K);

          

           B: (a * b) = (( multemb f) . (x,y)) by defemb

          .= ( multemb (f,x,y)) by defmult

          .= ( 0. K) by A2, defmultf;

          

           X: ( 0. K) in K;

          per cases by A2;

            suppose x = ( 0. K);

            

            then

             C: (g . a) = (f . ( 0. K)) by X, defiso

            .= ( 0. F) by RING_2: 6;

            

            thus (g . (a * b)) = (f . ( 0. K)) by B, X, defiso

            .= ((g . a) * (g . b)) by C, RING_2: 6;

          end;

            suppose y = ( 0. K);

            

            then

             C: (g . b) = (f . ( 0. K)) by X, defiso

            .= ( 0. F) by RING_2: 6;

            

            thus (g . (a * b)) = (f . ( 0. K)) by B, X, defiso

            .= ((g . a) * (g . b)) by C, RING_2: 6;

          end;

        end;

          suppose

           A: x in ( [#] K) & x <> ( 0. K) & not y in ( [#] K);

          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) = (fa * b1) by AS, A, Lm10;

          a in K & not b in K by A;

          then

           C: (g . a) = (f . a) & (g . b) = b by defiso;

           not (a * b) in K by AS, A, Lm10;

          hence (g . (a * b)) = ((g . a) * (g . b)) by B, C, defiso;

        end;

          suppose

           A: y in ( [#] K) & y <> ( 0. K) & not x in ( [#] K);

          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) = (a1 * fb) by AS, A, Lm10;

          b in K & not a in K by A;

          then

           C: (g . a) = a & (g . b) = (f . b) by defiso;

           not (a * b) in K by AS, A, Lm10;

          hence (g . (a * b)) = ((g . a) * (g . b)) by B, C, defiso;

        end;

          suppose

           A: not x in ( [#] K) & not y in ( [#] K) & (the multF of F . (x,y)) in ( rng f);

          then

          reconsider a1 = a, b1 = b as Element of F by Lm1;

          

           C: (a * b) = ((f " ) . (a1 * b1)) by A, Lm13;

           not a in K & not b in K by A;

          then

           D: (g . a) = a & (g . 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 (g . (a * b)) = (f . ((f " ) . (a1 * b1))) by C, defiso

          .= ((g . a) * (g . b)) by D, A, FUNCT_1: 35;

        end;

          suppose

           A: not x in ( [#] K) & not y in ( [#] K) & not ((the multF of F . (x,y)) in ( rng f));

          then

          reconsider a1 = a, b1 = b as Element of F by Lm1;

          

           C: (a * b) = (a1 * b1) by AS, A, Lm12;

           not a in K & not b in K by A;

          then

           D: (g . a) = a & (g . b) = b by defiso;

           not (a1 * b1) in K by AS, XBOOLE_0:def 4;

          hence (g . (a * b)) = ((g . a) * (g . b)) by D, C, defiso;

        end;

      end;

      hence thesis;

    end;

    registration

      let K be Field, F be K -monomorphic Field;

      let f be Monomorphism of K, F;

      cluster ( emb_iso f) -> one-to-one;

      coherence

      proof

        set g = ( emb_iso f);

        

         E: ( [#] ( embField f)) = ( carr f) by defemb;

        

         D: ( dom f) = ( [#] K) by FUNCT_2:def 1;

        

         H: f is one-to-one;

        now

          let x1,x2 be object;

          assume

           A: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

          then

          reconsider c = x2 as Element of ( embField f);

          per cases ;

            suppose x1 in ( [#] K);

            then

            reconsider a = x1 as Element of K;

            a in K;

            then

             B: (f . a) = (g . a) by A, defiso;

            then

             C: (g . a) in ( rng f) by D, FUNCT_1:def 3;

            now

              assume

               C1: not x2 in K;

              (g . c) = x2 by C1, defiso;

              then not x2 in (( [#] F) \ ( rng f)) by C, A, XBOOLE_0:def 5;

              hence contradiction by C1, A, E, XBOOLE_0:def 3;

            end;

            then

            reconsider b = x2 as Element of K;

            b in K;

            then (f . b) = (f . a) by A, B, defiso;

            hence x1 = x2 by H, D;

          end;

            suppose

             Z: not x1 in ( [#] K);

            reconsider a = x1 as Element of ( embField f) by A;

             not a in K by Z;

            then

             B: (g . a) = a by defiso;

             C:

            now

              assume

               C1: x2 in K;

              then

               C2: x2 in ( dom f) by FUNCT_2:def 1;

              reconsider c = x2 as Element of ( embField f) by A;

              a = (f . x2) by A, B, C1, defiso;

              then a in ( rng f) by C2, FUNCT_1:def 3;

              then not a in (( [#] F) \ ( rng f)) by XBOOLE_0:def 5;

              hence contradiction by Z, E, XBOOLE_0:def 3;

            end;

            hence x1 = x2 by A, B, defiso;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_2:15

    

     Th13: for f be Monomorphism of K, F st (K,F) are_disjoint holds ( emb_iso f) is onto

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      set g = ( emb_iso f);

      

       E: ( [#] ( embField f)) = ( carr f) by defemb;

      

       F: ( dom g) = ( [#] ( embField f)) by FUNCT_2:def 1;

       A:

      now

        let o be object;

        assume o in ( [#] F);

        then

        reconsider u = o as Element of F;

        per cases ;

          suppose u in ( rng f);

          then

          consider y be object such that

           B: y in ( dom f) & (f . y) = u by FUNCT_1:def 3;

          reconsider y as Element of K by B;

          reconsider yy = y as Element of ( embField f) by E, XBOOLE_0:def 3;

          y in K;

          then (g . yy) = u by B, defiso;

          hence o in ( rng g) by F, FUNCT_1: 3;

        end;

          suppose not u in ( rng f);

          then u in (( [#] F) \ ( rng f)) by XBOOLE_0:def 5;

          then

          reconsider uu = u as Element of ( embField f) by E, XBOOLE_0:def 3;

           not u in K by AS, XBOOLE_0:def 4;

          then (g . uu) = u by defiso;

          hence o in ( rng g) by F, FUNCT_1: 3;

        end;

      end;

      for o be object st o in ( rng g) holds o in ( [#] F);

      hence g is onto by A, TARSKI: 2;

    end;

    theorem :: FIELD_2:16

    

     Th14: for f be Monomorphism of K, F st (K,F) are_disjoint holds (F,( embField f)) are_isomorphic

    proof

      let f be Monomorphism of K, F;

      assume

       AS: (K,F) are_disjoint ;

      set g = ( emb_iso f);

      g is unity-preserving additive multiplicative by AS, Th11, Th12;

      then g is isomorphism by AS, Th13, MOD_4:def 12;

      hence thesis by QUOFIELD:def 23;

    end;

    theorem :: FIELD_2:17

    

     Th15: for f be Monomorphism of K, F, E be Field st E = ( embField f) holds K is Subfield of E

    proof

      let f be Monomorphism of K, F, E be Field;

      

       A2: ( [#] ( embField f)) = ( carr f) by defemb;

      assume

       A1: E = ( embField f);

      then ( [#] E) = ( carr f) by defemb;

      then

       A3: ( [#] K) c= ( [#] E) by XBOOLE_0:def 3;

      

       A4: ( dom the addF of E) = [:( [#] E), ( [#] E):] by FUNCT_2:def 1;

      set g1 = the addF of K, g2 = (the addF of E | [:( [#] K), ( [#] K):]);

      

       A5: ( dom g2) = (( dom the addF of E) /\ [:( [#] K), ( [#] K):]) by RELAT_1: 61

      .= [:( [#] K), ( [#] K):] by A3, ZFMISC_1: 96, XBOOLE_1: 28, A4

      .= ( dom g1) by FUNCT_2:def 1;

      now

        let x be set;

        assume x in ( dom the addF of K);

        then

        consider x1,x2 be object such that

         A6: x1 in ( [#] K) & x2 in ( [#] K) & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider a = x1, b = x2 as Element of K by A6;

        

         A7: [a, b] in [:( [#] K), ( [#] K):] by ZFMISC_1:def 2;

        reconsider a1 = x1, b1 = x2 as Element of ( embField f) by A6, A2, XBOOLE_0:def 3;

        ((the addF of E || ( [#] K)) . (a,b)) = (a1 + b1) by A1, A7, FUNCT_1: 49

        .= (a + b) by Lm7;

        hence (the addF of K . x) = (g2 . x) by A6;

      end;

      then

       A8: the addF of K = (the addF of E || ( [#] K)) by A5;

      set g1 = the multF of K, g2 = (the multF of E | [:( [#] K), ( [#] K):]);

      

       A9: ( dom the multF of E) = [:( [#] E), ( [#] E):] by FUNCT_2:def 1;

      

       A10: ( dom g2) = (( dom the multF of E) /\ [:( [#] K), ( [#] K):]) by RELAT_1: 61

      .= [:( [#] K), ( [#] K):] by A3, ZFMISC_1: 96, XBOOLE_1: 28, A9

      .= ( dom g1) by FUNCT_2:def 1;

      now

        let x be set;

        assume x in ( dom the multF of K);

        then

        consider x1,x2 be object such that

         A11: x1 in ( [#] K) & x2 in ( [#] K) & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider a = x1, b = x2 as Element of K by A11;

        

         A12: [a, b] in [:( [#] K), ( [#] K):] by ZFMISC_1:def 2;

        reconsider a1 = x1, b1 = x2 as Element of ( embField f) by A11, A2, XBOOLE_0:def 3;

        ((the multF of E || ( [#] K)) . (a,b)) = (a1 * b1) by A1, A12, FUNCT_1: 49

        .= (a * b) by Lm11;

        hence (the multF of K . x) = (g2 . x) by A11;

      end;

      then

       A13: the multF of K = (the multF of E || ( [#] K)) by A10;

      ( 1. E) = ( 1. K) & ( 0. E) = ( 0. K) by defemb, A1;

      hence thesis by A3, A8, A13, EC_PF_1:def 1;

    end;

    theorem :: FIELD_2:18

    

     Th16: (K,F) are_disjoint implies ex E be Field st (E,F) are_isomorphic & K is Subfield of E

    proof

      assume

       AS: (K,F) are_disjoint ;

      set f = the Monomorphism of K, F;

      reconsider E = ( embField f) as Field by AS, Th6, Th8, Th9, Th7, Th10;

      take E;

      thus thesis by AS, Th14, Th15;

    end;

    theorem :: FIELD_2:19

    for K,F be Field st (K,F) are_disjoint holds F is K -monomorphic iff ex E be Field st (E,F) are_isomorphic & K is Subfield of E

    proof

      let K,F be Field;

      assume

       AS: (K,F) are_disjoint ;

      now

        assume ex E be Field st (E,F) are_isomorphic & K is Subfield of E;

        then

        consider E be Field such that

         A: (E,F) are_isomorphic & K is Subfield of E;

        K is Subring of E by A, RING_3: 43;

        then

        consider m be Function of K, E such that

         B: m is RingHomomorphism monomorphism by RING_3:def 3, RING_3: 71;

        consider i be Function of E, F such that

         C: i is RingIsomorphism by A, QUOFIELD:def 23;

        set f = (i * m);

        f is linear by B, C, RINGCAT1: 1;

        hence F is K -monomorphic by B, C, RING_3:def 3;

      end;

      hence thesis by AS, Th16;

    end;