cfuncdom.miz



    begin

    reserve x1,x2,z for set;

    reserve A,B for non empty set;

    reserve f,g,h for Element of ( Funcs (A, COMPLEX ));

    definition

      let A be set;

      :: CFUNCDOM:def1

      func ComplexFuncAdd (A) -> BinOp of ( Funcs (A, COMPLEX )) means

      : Def1: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it . (f,g)) = ( addcomplex .: (f,g));

      existence

      proof

        deffunc F( Element of ( Funcs (A, COMPLEX )), Element of ( Funcs (A, COMPLEX ))) = ( addcomplex .: ($1,$2));

        consider F be BinOp of ( Funcs (A, COMPLEX )) such that

         A1: for x,y be Element of ( Funcs (A, COMPLEX )) holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take F;

        let f,g be Element of ( Funcs (A, COMPLEX ));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( Funcs (A, COMPLEX )) such that

         A2: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it1 . (f,g)) = ( addcomplex .: (f,g)) and

         A3: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it2 . (f,g)) = ( addcomplex .: (f,g));

        now

          let f,g be Element of ( Funcs (A, COMPLEX ));

          

          thus (it1 . (f,g)) = ( addcomplex .: (f,g)) by A2

          .= (it2 . (f,g)) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster ( ComplexFuncAdd A) -> complex-functions-valued;

      coherence ;

    end

    definition

      let A be set;

      :: CFUNCDOM:def2

      func ComplexFuncMult (A) -> BinOp of ( Funcs (A, COMPLEX )) means

      : Def2: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it . (f,g)) = ( multcomplex .: (f,g));

      existence

      proof

        deffunc F( Element of ( Funcs (A, COMPLEX )), Element of ( Funcs (A, COMPLEX ))) = ( multcomplex .: ($1,$2));

        consider F be BinOp of ( Funcs (A, COMPLEX )) such that

         A1: for x,y be Element of ( Funcs (A, COMPLEX )) holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take F;

        let f,g be Element of ( Funcs (A, COMPLEX ));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( Funcs (A, COMPLEX )) such that

         A2: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it1 . (f,g)) = ( multcomplex .: (f,g)) and

         A3: for f,g be Element of ( Funcs (A, COMPLEX )) holds (it2 . (f,g)) = ( multcomplex .: (f,g));

        now

          let f,g be Element of ( Funcs (A, COMPLEX ));

          

          thus (it1 . (f,g)) = ( multcomplex .: (f,g)) by A2

          .= (it2 . (f,g)) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster ( ComplexFuncMult A) -> complex-functions-valued;

      coherence ;

    end

    definition

      let A be non empty set;

      :: CFUNCDOM:def3

      func ComplexFuncExtMult (A) -> Function of [: COMPLEX , ( Funcs (A, COMPLEX )):], ( Funcs (A, COMPLEX )) means

      : Def3: for z be Complex, f be Element of ( Funcs (A, COMPLEX )), x be Element of A holds ((it . [z, f]) . x) = (z * (f . x));

      existence

      proof

        deffunc F( Element of COMPLEX , Element of ( Funcs (A, COMPLEX ))) = ( multcomplex [;] ($1,$2));

        consider F be Function of [: COMPLEX , ( Funcs (A, COMPLEX )):], ( Funcs (A, COMPLEX )) such that

         A1: for z be Element of COMPLEX , f be Element of ( Funcs (A, COMPLEX )) holds (F . (z,f)) = F(z,f) from BINOP_1:sch 4;

        take F;

        let z be Complex, f be Element of ( Funcs (A, COMPLEX )), x be Element of A;

        

         A2: z in COMPLEX by XCMPLX_0:def 2;

        then (F . (z,f)) = ( multcomplex [;] (z,f)) by A1;

        

        hence ((F . [z, f]) . x) = ( multcomplex . (z,(f . x))) by FUNCOP_1: 53, A2

        .= (z * (f . x)) by BINOP_2:def 5;

      end;

      uniqueness

      proof

        let it1,it2 be Function of [: COMPLEX , ( Funcs (A, COMPLEX )):], ( Funcs (A, COMPLEX )) such that

         A3: for z be Complex, f be Element of ( Funcs (A, COMPLEX )), x be Element of A holds ((it1 . [z, f]) . x) = (z * (f . x)) and

         A4: for z be Complex, f be Element of ( Funcs (A, COMPLEX )), x be Element of A holds ((it2 . [z, f]) . x) = (z * (f . x));

        now

          let z be Element of COMPLEX , f be Element of ( Funcs (A, COMPLEX ));

          now

            let x be Element of A;

            

            thus ((it1 . [z, f]) . x) = (z * (f . x)) by A3

            .= ((it2 . [z, f]) . x) by A4;

          end;

          hence (it1 . (z,f)) = (it2 . (z,f)) by FUNCT_2: 63;

        end;

        hence thesis;

      end;

    end

    registration

      let A be non empty set;

      cluster ( ComplexFuncExtMult A) -> complex-functions-valued;

      coherence ;

    end

    definition

      let A;

      :: CFUNCDOM:def4

      func ComplexFuncZero (A) -> Element of ( Funcs (A, COMPLEX )) equals (A --> 0 );

      coherence

      proof

        (A --> 0c ) is Function of A, COMPLEX ;

        hence thesis by FUNCT_2: 8;

      end;

    end

    definition

      let A;

      :: CFUNCDOM:def5

      func ComplexFuncUnit (A) -> Element of ( Funcs (A, COMPLEX )) equals (A --> 1r );

      coherence by FUNCT_2: 8;

    end

    

     Lm1: for x be Element of A, f be Function of A, B holds x in ( dom f)

    proof

      let x be Element of A;

      let f be Function of A, B;

      x in A;

      hence thesis by FUNCT_2:def 1;

    end;

    theorem :: CFUNCDOM:1

    

     Th1: h = (( ComplexFuncAdd A) . (f,g)) iff for x be Element of A holds (h . x) = ((f . x) + (g . x))

    proof

       A1:

      now

        assume

         A2: for x be Element of A holds (h . x) = ((f . x) + (g . x));

        now

          let x be Element of A;

          

           A3: x in ( dom ( addcomplex .: (f,g))) by Lm1;

          

          thus ((( ComplexFuncAdd A) . (f,g)) . x) = (( addcomplex .: (f,g)) . x) by Def1

          .= ( addcomplex . ((f . x),(g . x))) by A3, FUNCOP_1: 22

          .= ((f . x) + (g . x)) by BINOP_2:def 3

          .= (h . x) by A2;

        end;

        hence h = (( ComplexFuncAdd A) . (f,g)) by FUNCT_2: 63;

      end;

      now

        assume

         A4: h = (( ComplexFuncAdd A) . (f,g));

        let x be Element of A;

        

         A5: x in ( dom ( addcomplex .: (f,g))) by Lm1;

        

        thus (h . x) = (( addcomplex .: (f,g)) . x) by A4, Def1

        .= ( addcomplex . ((f . x),(g . x))) by A5, FUNCOP_1: 22

        .= ((f . x) + (g . x)) by BINOP_2:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: CFUNCDOM:2

    

     Th2: h = (( ComplexFuncMult A) . (f,g)) iff for x be Element of A holds (h . x) = ((f . x) * (g . x))

    proof

       A1:

      now

        assume

         A2: for x be Element of A holds (h . x) = ((f . x) * (g . x));

        now

          let x be Element of A;

          

           A3: x in ( dom ( multcomplex .: (f,g))) by Lm1;

          

          thus ((( ComplexFuncMult A) . (f,g)) . x) = (( multcomplex .: (f,g)) . x) by Def2

          .= ( multcomplex . ((f . x),(g . x))) by A3, FUNCOP_1: 22

          .= ((f . x) * (g . x)) by BINOP_2:def 5

          .= (h . x) by A2;

        end;

        hence h = (( ComplexFuncMult A) . (f,g)) by FUNCT_2: 63;

      end;

      now

        assume

         A4: h = (( ComplexFuncMult A) . (f,g));

        let x be Element of A;

        

         A5: x in ( dom ( multcomplex .: (f,g))) by Lm1;

        

        thus (h . x) = (( multcomplex .: (f,g)) . x) by A4, Def2

        .= ( multcomplex . ((f . x),(g . x))) by A5, FUNCOP_1: 22

        .= ((f . x) * (g . x)) by BINOP_2:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: CFUNCDOM:3

    ( ComplexFuncZero A) <> ( ComplexFuncUnit A)

    proof

      set a = the Element of A;

      (( ComplexFuncZero A) . a) = 0c by FUNCOP_1: 7;

      hence thesis by COMPLEX1:def 4, FUNCOP_1: 7;

    end;

    reserve a,b for Complex;

    theorem :: CFUNCDOM:4

    

     Th4: h = (( ComplexFuncExtMult A) . [a, f]) iff for x be Element of A holds (h . x) = (a * (f . x))

    proof

      thus h = (( ComplexFuncExtMult A) . [a, f]) implies for x be Element of A holds (h . x) = (a * (f . x)) by Def3;

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

      now

        assume

         A1: for x be Element of A holds (h . x) = (a * (f . x));

        for x be Element of A holds (h . x) = ((( ComplexFuncExtMult A) . [a, f]) . x)

        proof

          let x be Element of A;

          

          thus (h . x) = (a * (f . x)) by A1

          .= ((( ComplexFuncExtMult A) . [a, f]) . x) by Def3;

        end;

        hence h = (( ComplexFuncExtMult A) . [a, f]) by FUNCT_2: 63;

      end;

      hence thesis;

    end;

    theorem :: CFUNCDOM:5

    

     Th5: (( ComplexFuncAdd A) . (f,g)) = (( ComplexFuncAdd A) . (g,f))

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncAdd A) . (f,g)) . x) = ((g . x) + (f . x)) by Th1

        .= ((( ComplexFuncAdd A) . (g,f)) . x) by Th1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:6

    

     Th6: (( ComplexFuncAdd A) . (f,(( ComplexFuncAdd A) . (g,h)))) = (( ComplexFuncAdd A) . ((( ComplexFuncAdd A) . (f,g)),h))

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncAdd A) . (f,(( ComplexFuncAdd A) . (g,h)))) . x) = ((f . x) + ((( ComplexFuncAdd A) . (g,h)) . x)) by Th1

        .= ((f . x) + ((g . x) + (h . x))) by Th1

        .= (((f . x) + (g . x)) + (h . x))

        .= (((( ComplexFuncAdd A) . (f,g)) . x) + (h . x)) by Th1

        .= ((( ComplexFuncAdd A) . ((( ComplexFuncAdd A) . (f,g)),h)) . x) by Th1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:7

    

     Th7: (( ComplexFuncMult A) . (f,g)) = (( ComplexFuncMult A) . (g,f))

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncMult A) . (f,g)) . x) = ((g . x) * (f . x)) by Th2

        .= ((( ComplexFuncMult A) . (g,f)) . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:8

    

     Th8: (( ComplexFuncMult A) . (f,(( ComplexFuncMult A) . (g,h)))) = (( ComplexFuncMult A) . ((( ComplexFuncMult A) . (f,g)),h))

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncMult A) . (f,(( ComplexFuncMult A) . (g,h)))) . x) = ((f . x) * ((( ComplexFuncMult A) . (g,h)) . x)) by Th2

        .= ((f . x) * ((g . x) * (h . x))) by Th2

        .= (((f . x) * (g . x)) * (h . x))

        .= (((( ComplexFuncMult A) . (f,g)) . x) * (h . x)) by Th2

        .= ((( ComplexFuncMult A) . ((( ComplexFuncMult A) . (f,g)),h)) . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:9

    

     Th9: (( ComplexFuncMult A) . (( ComplexFuncUnit A),f)) = f

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncMult A) . (( ComplexFuncUnit A),f)) . x) = ((( ComplexFuncUnit A) . x) * (f . x)) by Th2

        .= ( 1r * (f . x)) by FUNCOP_1: 7

        .= (f . x) by COMPLEX1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:10

    

     Th10: (( ComplexFuncAdd A) . (( ComplexFuncZero A),f)) = f

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncAdd A) . (( ComplexFuncZero A),f)) . x) = ((( ComplexFuncZero A) . x) + (f . x)) by Th1

        .= ( 0c + (f . x)) by FUNCOP_1: 7

        .= (f . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:11

    

     Th11: (( ComplexFuncAdd A) . (f,(( ComplexFuncExtMult A) . [( - 1r ), f]))) = ( ComplexFuncZero A)

    proof

      reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of A;

        set y = (f . x);

        

        thus ((( ComplexFuncAdd A) . (f,(( ComplexFuncExtMult A) . [mj, f]))) . x) = ((f . x) + ((( ComplexFuncExtMult A) . [mj, f]) . x)) by Th1

        .= ((f . x) + (mj * y)) by Th4

        .= (( ComplexFuncZero A) . x) by COMPLEX1:def 4, FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:12

    

     Th12: (( ComplexFuncExtMult A) . [ 1r , f]) = f

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncExtMult A) . [ 1r , f]) . x) = ( 1r * (f . x)) by Th4

        .= (f . x) by COMPLEX1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:13

    

     Th13: for a,b be Complex holds (( ComplexFuncExtMult A) . [a, (( ComplexFuncExtMult A) . [b, f])]) = (( ComplexFuncExtMult A) . [(a * b), f])

    proof

      let a,b be Complex;

      reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider ab = (a * b) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of A;

        

        thus ((( ComplexFuncExtMult A) . [a, (( ComplexFuncExtMult A) . [b, f])]) . x) = (a * ((( ComplexFuncExtMult A) . [b, f]) . x)) by Th4

        .= (a * (b * (f . x))) by Th4

        .= ((a * b) * (f . x))

        .= ((( ComplexFuncExtMult A) . [ab, f]) . x) by Th4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:14

    

     Th14: for a,b be Complex holds (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, f]))) = (( ComplexFuncExtMult A) . [(a + b), f])

    proof

      let a,b be Complex;

      reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider ab = (a + b) as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of A;

        

        thus ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, f]))) . x) = (((( ComplexFuncExtMult A) . [a, f]) . x) + ((( ComplexFuncExtMult A) . [b, f]) . x)) by Th1

        .= ((a * (f . x)) + ((( ComplexFuncExtMult A) . [b, f]) . x)) by Th4

        .= ((a * (f . x)) + (b * (f . x))) by Th4

        .= ((a + b) * (f . x))

        .= ((( ComplexFuncExtMult A) . [ab, f]) . x) by Th4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm2: for a be Complex holds (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [a, g]))) = (( ComplexFuncExtMult A) . [a, (( ComplexFuncAdd A) . (f,g))])

    proof

      let a be Complex;

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of A;

        

        thus ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [a, g]))) . x) = (((( ComplexFuncExtMult A) . [a, f]) . x) + ((( ComplexFuncExtMult A) . [a, g]) . x)) by Th1

        .= ((a * (f . x)) + ((( ComplexFuncExtMult A) . [a, g]) . x)) by Th4

        .= ((a * (f . x)) + (a * (g . x))) by Th4

        .= (a * ((f . x) + (g . x)))

        .= (a * ((( ComplexFuncAdd A) . (f,g)) . x)) by Th1

        .= ((( ComplexFuncExtMult A) . [a, (( ComplexFuncAdd A) . (f,g))]) . x) by Th4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:15

    

     Th15: (( ComplexFuncMult A) . (f,(( ComplexFuncAdd A) . (g,h)))) = (( ComplexFuncAdd A) . ((( ComplexFuncMult A) . (f,g)),(( ComplexFuncMult A) . (f,h))))

    proof

      now

        let x be Element of A;

        

        thus ((( ComplexFuncMult A) . (f,(( ComplexFuncAdd A) . (g,h)))) . x) = ((f . x) * ((( ComplexFuncAdd A) . (g,h)) . x)) by Th2

        .= ((f . x) * ((g . x) + (h . x))) by Th1

        .= (((f . x) * (g . x)) + ((f . x) * (h . x)))

        .= (((( ComplexFuncMult A) . (f,g)) . x) + ((f . x) * (h . x))) by Th2

        .= (((( ComplexFuncMult A) . (f,g)) . x) + ((( ComplexFuncMult A) . (f,h)) . x)) by Th2

        .= ((( ComplexFuncAdd A) . ((( ComplexFuncMult A) . (f,g)),(( ComplexFuncMult A) . (f,h)))) . x) by Th1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:16

    

     Th16: (( ComplexFuncMult A) . ((( ComplexFuncExtMult A) . [a, f]),g)) = (( ComplexFuncExtMult A) . [a, (( ComplexFuncMult A) . (f,g))])

    proof

      reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

      now

        let x be Element of A;

        

        thus ((( ComplexFuncMult A) . ((( ComplexFuncExtMult A) . [a, f]),g)) . x) = (((( ComplexFuncExtMult A) . [a, f]) . x) * (g . x)) by Th2

        .= ((a * (f . x)) * (g . x)) by Th4

        .= (a * ((f . x) * (g . x)))

        .= (a * ((( ComplexFuncMult A) . (f,g)) . x)) by Th2

        .= ((( ComplexFuncExtMult A) . [a, (( ComplexFuncMult A) . (f,g))]) . x) by Th4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    theorem :: CFUNCDOM:17

    

     Th17: ex f, g st (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0 )) & for z st z in A holds (z = x1 implies (g . z) = 0 ) & (z <> x1 implies (g . z) = 1r )

    proof

      deffunc G( object) = 1r ;

      deffunc F( object) = 0c ;

      defpred P[ object] means $1 = x1;

      

       A1: for z be object st z in A holds ( P[z] implies G(z) in COMPLEX ) & ( not P[z] implies F(z) in COMPLEX );

      consider f be Function of A, COMPLEX such that

       A2: for z be object st z in A holds ( P[z] implies (f . z) = G(z)) & ( not P[z] implies (f . z) = F(z)) from FUNCT_2:sch 5( A1);

      

       A3: for z be object st z in A holds ( P[z] implies F(z) in COMPLEX ) & ( not P[z] implies G(z) in COMPLEX );

      consider g be Function of A, COMPLEX such that

       A4: for z be object st z in A holds ( P[z] implies (g . z) = F(z)) & ( not P[z] implies (g . z) = G(z)) from FUNCT_2:sch 5( A3);

      reconsider f, g as Element of ( Funcs (A, COMPLEX )) by FUNCT_2: 8;

      take f, g;

      thus thesis by A2, A4;

    end;

    theorem :: CFUNCDOM:18

    

     Th18: x1 in A & x2 in A & x1 <> x2 & (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0 )) & (for z st z in A holds (z = x1 implies (g . z) = 0 ) & (z <> x1 implies (g . z) = 1r )) implies for a, b st (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A) holds a = 0c & b = 0c

    proof

      assume that

       A1: x1 in A and

       A2: x2 in A and

       A3: x1 <> x2 and

       A4: (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0 )) & for z st z in A holds (z = x1 implies (g . z) = 0 ) & (z <> x1 implies (g . z) = 1r );

      

       A5: (f . x2) = 0c & (g . x2) = 1r by A2, A3, A4;

      

       A6: (f . x1) = 1r & (g . x1) = 0c by A1, A4;

      let a, b;

      reconsider x1, x2 as Element of A by A1, A2;

      assume

       A7: (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A);

      reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;

      

       A8: 0c = ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) . x2) by FUNCOP_1: 7, A7

      .= (((( ComplexFuncExtMult A) . [a, f]) . x2) + ((( ComplexFuncExtMult A) . [b, g]) . x2)) by Th1

      .= ((a * (f . x2)) + ((( ComplexFuncExtMult A) . [b, g]) . x2)) by Th4

      .= ( 0c + (b * 1r )) by A5, Th4

      .= b by COMPLEX1:def 4;

       0c = ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) . x1) by A7, FUNCOP_1: 7

      .= (((( ComplexFuncExtMult A) . [a, f]) . x1) + ((( ComplexFuncExtMult A) . [b, g]) . x1)) by Th1

      .= ((a * (f . x1)) + ((( ComplexFuncExtMult A) . [b, g]) . x1)) by Th4

      .= (a + (b * 0c )) by A6, Th4, COMPLEX1:def 4

      .= a;

      hence thesis by A8;

    end;

    theorem :: CFUNCDOM:19

    x1 in A & x2 in A & x1 <> x2 implies ex f, g st for a, b st (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A) holds a = 0 & b = 0

    proof

      assume

       A1: x1 in A & x2 in A & x1 <> x2;

      consider f, g such that

       A2: (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0c )) & for z st z in A holds (z = x1 implies (g . z) = 0c ) & (z <> x1 implies (g . z) = 1r ) by Th17;

      take f, g;

      let a, b;

      assume (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A);

      hence thesis by A1, A2, Th18;

    end;

    theorem :: CFUNCDOM:20

    

     Th20: A = {x1, x2} & x1 <> x2 & (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0 )) & (for z st z in A holds (z = x1 implies (g . z) = 0 ) & (z <> x1 implies (g . z) = 1r )) implies for h holds ex a, b st h = (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g])))

    proof

      assume that

       A1: A = {x1, x2} and

       A2: x1 <> x2 and

       A3: (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0 )) & for z st z in A holds (z = x1 implies (g . z) = 0 ) & (z <> x1 implies (g . z) = 1r );

      x2 in A by A1, TARSKI:def 2;

      then

       A4: (f . x2) = 0c & (g . x2) = 1r by A2, A3;

      x1 in A by A1, TARSKI:def 2;

      then

       A5: (f . x1) = 1r & (g . x1) = 0c by A3;

      let h;

      reconsider x1, x2 as Element of A by A1, TARSKI:def 2;

      take a = (h . x1), b = (h . x2);

      now

        let x be Element of A;

        

         A6: x = x1 or x = x2 by A1, TARSKI:def 2;

        

         A7: ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) . x2) = (((( ComplexFuncExtMult A) . [a, f]) . x2) + ((( ComplexFuncExtMult A) . [b, g]) . x2)) by Th1

        .= ((a * (f . x2)) + ((( ComplexFuncExtMult A) . [b, g]) . x2)) by Th4

        .= ( 0c + (b * 1r )) by A4, Th4

        .= (h . x2) by COMPLEX1:def 4;

        ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) . x1) = (((( ComplexFuncExtMult A) . [a, f]) . x1) + ((( ComplexFuncExtMult A) . [b, g]) . x1)) by Th1

        .= ((a * (f . x1)) + ((( ComplexFuncExtMult A) . [b, g]) . x1)) by Th4

        .= (a + (b * 0c )) by A5, Th4, COMPLEX1:def 4

        .= (h . x1);

        hence (h . x) = ((( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) . x) by A6, A7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFUNCDOM:21

    A = {x1, x2} & x1 <> x2 implies ex f, g st for h holds ex a, b st h = (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g])))

    proof

      assume

       A1: A = {x1, x2} & x1 <> x2;

      consider f, g such that

       A2: (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0c )) & for z st z in A holds (z = x1 implies (g . z) = 0c ) & (z <> x1 implies (g . z) = 1r ) by Th17;

      take f, g;

      let h;

      thus thesis by A1, A2, Th20;

    end;

    theorem :: CFUNCDOM:22

    

     Th22: A = {x1, x2} & x1 <> x2 implies ex f, g st (for a, b st (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A) holds a = 0 & b = 0 ) & for h holds ex a, b st h = (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g])))

    proof

      assume that

       A1: A = {x1, x2} and

       A2: x1 <> x2;

      consider f, g such that

       A3: (for z st z in A holds (z = x1 implies (f . z) = 1r ) & (z <> x1 implies (f . z) = 0c )) & for z st z in A holds (z = x1 implies (g . z) = 0c ) & (z <> x1 implies (g . z) = 1r ) by Th17;

      take f, g;

      x1 in A & x2 in A by A1, TARSKI:def 2;

      hence thesis by A1, A2, A3, Th18, Th20;

    end;

    definition

      let A;

      :: CFUNCDOM:def6

      func ComplexVectSpace (A) -> strict non empty CLSStruct equals CLSStruct (# ( Funcs (A, COMPLEX )), ( ComplexFuncZero A), ( ComplexFuncAdd A), ( ComplexFuncExtMult A) #);

      coherence ;

    end

    reserve C for strict non empty CLSStruct,

u,v,w for Element of C;

    registration

      let A;

      cluster ( ComplexVectSpace A) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        let C such that

         A1: C = ( ComplexVectSpace A);

        thus (u + v) = (v + u) by Th5, A1;

        thus ((u + v) + w) = (u + (v + w)) by Th6, A1;

        thus (u + ( 0. C)) = u

        proof

          reconsider v = u as Element of ( Funcs (A, COMPLEX )) by A1;

          

          thus (u + ( 0. C)) = (( ComplexFuncAdd A) . (( ComplexFuncZero A),v)) by Th5, A1

          .= u by Th10;

        end;

        thus u is right_complementable

        proof

          reconsider v = u as Element of ( Funcs (A, COMPLEX )) by A1;

          reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

          reconsider w = (( ComplexFuncExtMult A) . [mj, v]) as VECTOR of C by A1;

          take w;

          thus thesis by Th11, A1;

        end;

        thus for a be Complex, u,v be VECTOR of C holds (a * (u + v)) = ((a * u) + (a * v)) by Lm2, A1;

        thus for a,b be Complex, v be VECTOR of C holds ((a + b) * v) = ((a * v) + (b * v)) by Th14, A1;

        thus for a,b be Complex, v be VECTOR of C holds ((a * b) * v) = (a * (b * v)) by Th13, A1;

        thus ( 1r * v) = v by Th12, A1;

      end;

    end

    

     Lm3: ex A, x1, x2 st A = {x1, x2} & x1 <> x2

    proof

      reconsider A = {1, 2} as non empty set;

      take A;

      thus thesis;

    end;

    theorem :: CFUNCDOM:23

    ex V be strict ComplexLinearSpace st ex u,v be VECTOR of V st (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w be VECTOR of V holds ex a, b st w = ((a * u) + (b * v))

    proof

      consider A, x1, x2 such that

       A1: A = {x1, x2} & x1 <> x2 by Lm3;

      take V = ( ComplexVectSpace A);

      consider f, g such that

       A2: for a, b st (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) = ( ComplexFuncZero A) holds a = 0c & b = 0c and

       A3: for h holds ex a, b st h = (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) by A1, Th22;

      reconsider u = f, v = g as VECTOR of V;

      take u, v;

      thus for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 by A2;

      thus for w be VECTOR of V holds ex a, b st w = ((a * u) + (b * v))

      proof

        let w be VECTOR of V;

        reconsider h = w as Element of ( Funcs (A, COMPLEX ));

        consider a, b such that

         A4: h = (( ComplexFuncAdd A) . ((( ComplexFuncExtMult A) . [a, f]),(( ComplexFuncExtMult A) . [b, g]))) by A3;

        h = ((a * u) + (b * v)) by A4;

        hence thesis;

      end;

    end;

    definition

      let A;

      :: CFUNCDOM:def7

      func CRing (A) -> doubleLoopStr equals doubleLoopStr (# ( Funcs (A, COMPLEX )), ( ComplexFuncAdd A), ( ComplexFuncMult A), ( ComplexFuncUnit A), ( ComplexFuncZero A) #);

      correctness ;

    end

    registration

      let A;

      cluster ( CRing A) -> non empty strict;

      coherence ;

    end

     Lm4:

    now

      let A;

      let x,e be Element of ( CRing A);

      assume e = ( ComplexFuncUnit A);

      hence (e * x) = x by Th9;

      hence (x * e) = x by Th7;

    end;

    registration

      let A;

      cluster ( CRing A) -> unital;

      coherence

      proof

        reconsider e = ( ComplexFuncUnit A) as Element of ( CRing A);

        take e;

        thus thesis by Lm4;

      end;

    end

    theorem :: CFUNCDOM:24

    

     Th24: for x,y,z be Element of ( CRing A) holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( CRing A))) = x & x is right_complementable & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( CRing A))) = x & (( 1. ( CRing A)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x))

    proof

      let x,y,z be Element of ( CRing A);

      set IT = ( CRing A);

      reconsider f = x as Element of ( Funcs (A, COMPLEX ));

      thus (x + y) = (y + x) by Th5;

      thus ((x + y) + z) = (x + (y + z)) by Th6;

      

      thus (x + ( 0. ( CRing A))) = (( ComplexFuncAdd A) . (( ComplexFuncZero A),f)) by Th5

      .= x by Th10;

      thus ex t be Element of ( CRing A) st (x + t) = ( 0. ( CRing A))

      proof

        reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

        set h = (( ComplexFuncExtMult A) . [mj, f]);

        reconsider t = h as Element of IT;

        take t;

        thus thesis by Th11;

      end;

      thus (x * y) = (y * x) by Th7;

      thus ((x * y) * z) = (x * (y * z)) by Th8;

      

      thus (x * ( 1. ( CRing A))) = (( ComplexFuncMult A) . (( ComplexFuncUnit A),f)) by Th7

      .= x by Th9;

      hence (( 1. ( CRing A)) * x) = x by Th7;

      thus (x * (y + z)) = ((x * y) + (x * z)) by Th15;

      

      hence ((y + z) * x) = ((x * y) + (x * z)) by Th7

      .= ((y * x) + (x * z)) by Th7

      .= ((y * x) + (z * x)) by Th7;

    end;

    theorem :: CFUNCDOM:25

    ( CRing A) is commutative Ring

    proof

      for x,y,z be Element of ( CRing A) holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( CRing A))) = x & x is right_complementable & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( CRing A))) = x & (( 1. ( CRing A)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) by Th24;

      hence thesis by ALGSTR_0:def 16, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 6, VECTSP_1:def 7;

    end;

    definition

      struct ( doubleLoopStr, CLSStruct) ComplexAlgebraStr (# the carrier -> set,

the multF, addF -> BinOp of the carrier,

the Mult -> Function of [: COMPLEX , the carrier:], the carrier,

the OneF, ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for ComplexAlgebraStr;

      existence

      proof

        set X = the non empty set, m = the BinOp of X, M = the Function of [: COMPLEX , X:], X, u = the Element of X;

        take ComplexAlgebraStr (# X, m, m, M, u, u #);

        thus the carrier of ComplexAlgebraStr (# X, m, m, M, u, u #) is non empty;

      end;

    end

    definition

      let A;

      :: CFUNCDOM:def8

      func CAlgebra (A) -> strict ComplexAlgebraStr equals ComplexAlgebraStr (# ( Funcs (A, COMPLEX )), ( ComplexFuncMult A), ( ComplexFuncAdd A), ( ComplexFuncExtMult A), ( ComplexFuncUnit A), ( ComplexFuncZero A) #);

      correctness ;

    end

    registration

      let A;

      cluster ( CAlgebra A) -> non empty;

      coherence ;

    end

     Lm5:

    now

      let A;

      let x,e be Element of ( CAlgebra A);

      assume e = ( ComplexFuncUnit A);

      hence (e * x) = x by Th9;

      hence (x * e) = x by Th7;

    end;

    registration

      let A;

      cluster ( CAlgebra A) -> unital;

      coherence

      proof

        reconsider e = ( ComplexFuncUnit A) as Element of ( CAlgebra A);

        take e;

        thus thesis by Lm5;

      end;

    end

    theorem :: CFUNCDOM:26

    for x,y,z be Element of ( CAlgebra A), a, b holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( CAlgebra A))) = x & x is right_complementable & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( CAlgebra A))) = x & (x * (y + z)) = ((x * y) + (x * z)) & (a * (x * y)) = ((a * x) * y) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x))

    proof

      let x,y,z be Element of ( CAlgebra A);

      let a, b;

      set IT = ( CAlgebra A);

      reconsider f = x as Element of ( Funcs (A, COMPLEX ));

      thus (x + y) = (y + x) by Th5;

      thus ((x + y) + z) = (x + (y + z)) by Th6;

      

      thus (x + ( 0. ( CAlgebra A))) = (( ComplexFuncAdd A) . (( ComplexFuncZero A),f)) by Th5

      .= x by Th10;

      thus ex t be Element of ( CAlgebra A) st (x + t) = ( 0. ( CAlgebra A))

      proof

        reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

        set h = (( ComplexFuncExtMult A) . [mj, f]);

        reconsider t = h as Element of IT;

        take t;

        thus thesis by Th11;

      end;

      thus (x * y) = (y * x) by Th7;

      thus ((x * y) * z) = (x * (y * z)) by Th8;

      

      thus (x * ( 1. ( CAlgebra A))) = (( ComplexFuncMult A) . (( ComplexFuncUnit A),f)) by Th7

      .= x by Th9;

      thus (x * (y + z)) = ((x * y) + (x * z)) by Th15;

      thus (a * (x * y)) = ((a * x) * y) by Th16;

      thus (a * (x + y)) = ((a * x) + (a * y)) by Lm2;

      thus ((a + b) * x) = ((a * x) + (b * x)) by Th14;

      thus thesis by Th13;

    end;

    definition

      let IT be non empty ComplexAlgebraStr;

      :: CFUNCDOM:def9

      attr IT is vector-associative means for x,y be Element of IT, a holds (a * (x * y)) = ((a * x) * y);

    end

    registration

      let A;

      cluster ( CAlgebra A) -> strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative;

      coherence

      proof

        set C = ( CAlgebra A);

        thus C is strict;

        thus C is Abelian by Th5;

        thus C is add-associative by Th6;

        thus C is right_zeroed

        proof

          let x be Element of C;

          reconsider f = x as Element of ( Funcs (A, COMPLEX ));

          

          thus (x + ( 0. C)) = (( ComplexFuncAdd A) . (( ComplexFuncZero A),f)) by Th5

          .= x by Th10;

        end;

        thus C is right_complementable

        proof

          let x be Element of C;

          reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

          reconsider f = x as Element of ( Funcs (A, COMPLEX ));

          reconsider t = (( ComplexFuncExtMult A) . [mj, f]) as Element of C;

          take t;

          thus thesis by Th11;

        end;

        thus C is commutative by Th7;

        thus C is associative by Th8;

        thus C is right_unital

        proof

          let x be Element of C;

          reconsider f = x as Element of ( Funcs (A, COMPLEX ));

          

          thus (x * ( 1. C)) = (( ComplexFuncMult A) . (( ComplexFuncUnit A),f)) by Th7

          .= x by Th9;

        end;

        thus C is right-distributive by Th15;

        thus C is vector-distributive by Lm2;

        thus C is scalar-distributive by Th14;

        thus C is scalar-associative by Th13;

        let x,y be Element of C;

        let a;

        thus thesis by Th16;

      end;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative for non empty ComplexAlgebraStr;

      existence

      proof

        take ( CAlgebra { 0 });

        thus thesis;

      end;

    end

    definition

      mode ComplexAlgebra is Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative non empty ComplexAlgebraStr;

    end

    theorem :: CFUNCDOM:27

    ( CAlgebra A) is ComplexAlgebra;

    theorem :: CFUNCDOM:28

    ( 1. ( CRing A)) = ( ComplexFuncUnit A);

    theorem :: CFUNCDOM:29

    ( 1. ( CAlgebra A)) = ( ComplexFuncUnit A);