convfun1.miz



    begin

    definition

      let X,Y be non empty RLSStruct;

      :: CONVFUN1:def1

      func Add_in_Prod_of_RLS (X,Y) -> BinOp of [:the carrier of X, the carrier of Y:] means

      : Def1: for z1,z2 be Element of [:the carrier of X, the carrier of Y:], x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y st z1 = [x1, y1] & z2 = [x2, y2] holds (it . (z1,z2)) = [(the addF of X . [x1, x2]), (the addF of Y . [y1, y2])];

      existence

      proof

        defpred P[ set, set, set] means for x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y st $1 = [x1, y1] & $2 = [x2, y2] holds $3 = [(the addF of X . [x1, x2]), (the addF of Y . [y1, y2])];

        set A = [:the carrier of X, the carrier of Y:];

        

         A1: for z1,z2 be Element of A holds ex z3 be Element of A st P[z1, z2, z3]

        proof

          let z1,z2 be Element of A;

          consider x19,y19 be object such that

           A2: x19 in the carrier of X and

           A3: y19 in the carrier of Y and

           A4: z1 = [x19, y19] by ZFMISC_1:def 2;

          consider x29,y29 be object such that

           A5: x29 in the carrier of X and

           A6: y29 in the carrier of Y and

           A7: z2 = [x29, y29] by ZFMISC_1:def 2;

          reconsider y19, y29 as VECTOR of Y by A3, A6;

          reconsider x19, x29 as VECTOR of X by A2, A5;

          reconsider z3 = [(the addF of X . [x19, x29]), (the addF of Y . [y19, y29])] as Element of A;

          take z3;

          let x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y;

          assume that

           A8: z1 = [x1, y1] and

           A9: z2 = [x2, y2];

          

           A10: x2 = x29 by A7, A9, XTUPLE_0: 1;

          

           A11: y1 = y19 by A4, A8, XTUPLE_0: 1;

          x1 = x19 by A4, A8, XTUPLE_0: 1;

          hence thesis by A7, A9, A10, A11, XTUPLE_0: 1;

        end;

        thus ex o be BinOp of A st for a,b be Element of A holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let A1,A2 be BinOp of [:the carrier of X, the carrier of Y:];

        assume

         A12: for z1,z2 be Element of [:the carrier of X, the carrier of Y:], x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y st z1 = [x1, y1] & z2 = [x2, y2] holds (A1 . (z1,z2)) = [(the addF of X . [x1, x2]), (the addF of Y . [y1, y2])];

        assume

         A13: for z1,z2 be Element of [:the carrier of X, the carrier of Y:], x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y st z1 = [x1, y1] & z2 = [x2, y2] holds (A2 . (z1,z2)) = [(the addF of X . [x1, x2]), (the addF of Y . [y1, y2])];

        for z1,z2 be Element of [:the carrier of X, the carrier of Y:] holds (A1 . (z1,z2)) = (A2 . (z1,z2))

        proof

          let z1,z2 be Element of [:the carrier of X, the carrier of Y:];

          consider x1,y1 be object such that

           A14: x1 in the carrier of X and

           A15: y1 in the carrier of Y and

           A16: z1 = [x1, y1] by ZFMISC_1:def 2;

          consider x2,y2 be object such that

           A17: x2 in the carrier of X and

           A18: y2 in the carrier of Y and

           A19: z2 = [x2, y2] by ZFMISC_1:def 2;

          reconsider y1, y2 as VECTOR of Y by A15, A18;

          reconsider x1, x2 as VECTOR of X by A14, A17;

          (A1 . (z1,z2)) = [(the addF of X . [x1, x2]), (the addF of Y . [y1, y2])] by A12, A16, A19;

          hence thesis by A13, A16, A19;

        end;

        hence thesis;

      end;

    end

    definition

      let X,Y be non empty RLSStruct;

      :: CONVFUN1:def2

      func Mult_in_Prod_of_RLS (X,Y) -> Function of [: REAL , [:the carrier of X, the carrier of Y:]:], [:the carrier of X, the carrier of Y:] means

      : Def2: for a be Real, z be Element of [:the carrier of X, the carrier of Y:], x be VECTOR of X, y be VECTOR of Y st z = [x, y] holds (it . (a,z)) = [(the Mult of X . [a, x]), (the Mult of Y . [a, y])];

      existence

      proof

        defpred P[ object, object, object] means for x be VECTOR of X, y be VECTOR of Y st $2 = [x, y] holds $3 = [(the Mult of X . [$1, x]), (the Mult of Y . [$1, y])];

        

         A1: for a1 be Element of REAL , z be Element of [:the carrier of X, the carrier of Y:] holds ex w be Element of [:the carrier of X, the carrier of Y:] st P[a1, z, w]

        proof

          let a1 be Element of REAL , z be Element of [:the carrier of X, the carrier of Y:];

          consider x9,y9 be object such that

           A2: x9 in the carrier of X and

           A3: y9 in the carrier of Y and

           A4: z = [x9, y9] by ZFMISC_1:def 2;

          reconsider y9 as VECTOR of Y by A3;

          reconsider x9 as VECTOR of X by A2;

          reconsider w = [(the Mult of X . [a1, x9]), (the Mult of Y . [a1, y9])] as Element of [:the carrier of X, the carrier of Y:];

          take w;

          for x be VECTOR of X, y be VECTOR of Y st z = [x, y] holds w = [(the Mult of X . [a1, x]), (the Mult of Y . [a1, y])]

          proof

            let x be VECTOR of X, y be VECTOR of Y;

            assume

             A5: z = [x, y];

            then x = x9 by A4, XTUPLE_0: 1;

            hence thesis by A4, A5, XTUPLE_0: 1;

          end;

          hence thesis;

        end;

        consider g be Function of [: REAL , [:the carrier of X, the carrier of Y:]:], [:the carrier of X, the carrier of Y:] such that

         A6: for a be Element of REAL , z be Element of [:the carrier of X, the carrier of Y:] holds P[a, z, (g . (a,z))] from BINOP_1:sch 3( A1);

        

         A7: for a be Real, z be Element of [:the carrier of X, the carrier of Y:] holds P[a, z, (g . (a,z))]

        proof

          let a be Real, z be Element of [:the carrier of X, the carrier of Y:];

          reconsider a as Element of REAL by XREAL_0:def 1;

           P[a, z, (g . (a,z))] by A6;

          hence thesis;

        end;

        take g;

        let a be Real, z be Element of [:the carrier of X, the carrier of Y:];

        thus thesis by A7;

      end;

      uniqueness

      proof

        let g1,g2 be Function of [: REAL , [:the carrier of X, the carrier of Y:]:], [:the carrier of X, the carrier of Y:];

        assume

         A8: for a be Real, z be Element of [:the carrier of X, the carrier of Y:], x be VECTOR of X, y be VECTOR of Y st z = [x, y] holds (g1 . (a,z)) = [(the Mult of X . [a, x]), (the Mult of Y . [a, y])];

        assume

         A9: for a be Real, z be Element of [:the carrier of X, the carrier of Y:], x be VECTOR of X, y be VECTOR of Y st z = [x, y] holds (g2 . (a,z)) = [(the Mult of X . [a, x]), (the Mult of Y . [a, y])];

        for a be Element of REAL , z be Element of [:the carrier of X, the carrier of Y:] holds (g1 . (a,z)) = (g2 . (a,z))

        proof

          let a be Element of REAL , z be Element of [:the carrier of X, the carrier of Y:];

          consider x,y be object such that

           A10: x in the carrier of X and

           A11: y in the carrier of Y and

           A12: z = [x, y] by ZFMISC_1:def 2;

          reconsider y as VECTOR of Y by A11;

          reconsider x as VECTOR of X by A10;

          (g1 . (a,z)) = [(the Mult of X . [a, x]), (the Mult of Y . [a, y])] by A8, A12;

          hence thesis by A9, A12;

        end;

        hence thesis;

      end;

    end

    definition

      let X,Y be non empty RLSStruct;

      :: CONVFUN1:def3

      func Prod_of_RLS (X,Y) -> RLSStruct equals RLSStruct (# [:the carrier of X, the carrier of Y:], [( 0. X), ( 0. Y)], ( Add_in_Prod_of_RLS (X,Y)), ( Mult_in_Prod_of_RLS (X,Y)) #);

      correctness ;

    end

    registration

      let X,Y be non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> non empty;

      coherence ;

    end

    theorem :: CONVFUN1:1

    for X,Y be non empty RLSStruct, x be VECTOR of X, y be VECTOR of Y, u be VECTOR of ( Prod_of_RLS (X,Y)), p be Real st u = [x, y] holds (p * u) = [(p * x), (p * y)] by Def2;

    theorem :: CONVFUN1:2

    

     Th2: for X,Y be non empty RLSStruct, x1,x2 be VECTOR of X, y1,y2 be VECTOR of Y, u1,u2 be VECTOR of ( Prod_of_RLS (X,Y)) st u1 = [x1, y1] & u2 = [x2, y2] holds (u1 + u2) = [(x1 + x2), (y1 + y2)] by Def1;

    registration

      let X,Y be Abelian non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> Abelian;

      coherence

      proof

        for u1,u2 be Element of ( Prod_of_RLS (X,Y)) holds (u1 + u2) = (u2 + u1)

        proof

          let u1,u2 be Element of ( Prod_of_RLS (X,Y));

          consider x1,y1 be object such that

           A1: x1 in the carrier of X and

           A2: y1 in the carrier of Y and

           A3: u1 = [x1, y1] by ZFMISC_1:def 2;

          reconsider y1 as VECTOR of Y by A2;

          reconsider x1 as VECTOR of X by A1;

          consider x2,y2 be object such that

           A4: x2 in the carrier of X and

           A5: y2 in the carrier of Y and

           A6: u2 = [x2, y2] by ZFMISC_1:def 2;

          reconsider y2 as VECTOR of Y by A5;

          reconsider x2 as VECTOR of X by A4;

          (u1 + u2) = [(x2 + x1), (y2 + y1)] by A3, A6, Th2;

          hence thesis by A3, A6, Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let X,Y be add-associative non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> add-associative;

      coherence

      proof

        for u1,u2,u3 be Element of ( Prod_of_RLS (X,Y)) holds ((u1 + u2) + u3) = (u1 + (u2 + u3))

        proof

          let u1,u2,u3 be Element of ( Prod_of_RLS (X,Y));

          consider x1,y1 be object such that

           A1: x1 in the carrier of X and

           A2: y1 in the carrier of Y and

           A3: u1 = [x1, y1] by ZFMISC_1:def 2;

          reconsider y1 as VECTOR of Y by A2;

          consider x3,y3 be object such that

           A4: x3 in the carrier of X and

           A5: y3 in the carrier of Y and

           A6: u3 = [x3, y3] by ZFMISC_1:def 2;

          reconsider y3 as VECTOR of Y by A5;

          reconsider x3 as VECTOR of X by A4;

          reconsider x1 as VECTOR of X by A1;

          consider x2,y2 be object such that

           A7: x2 in the carrier of X and

           A8: y2 in the carrier of Y and

           A9: u2 = [x2, y2] by ZFMISC_1:def 2;

          reconsider y2 as VECTOR of Y by A8;

          reconsider x2 as VECTOR of X by A7;

          (u1 + u2) = [(x1 + x2), (y1 + y2)] by A3, A9, Def1;

          then

           A10: ((u1 + u2) + u3) = [((x1 + x2) + x3), ((y1 + y2) + y3)] by A6, Def1;

          (u2 + u3) = [(x2 + x3), (y2 + y3)] by A9, A6, Def1;

          then

           A11: (u1 + (u2 + u3)) = [(x1 + (x2 + x3)), (y1 + (y2 + y3))] by A3, Def1;

          ((x1 + x2) + x3) = (x1 + (x2 + x3)) by RLVECT_1:def 3;

          hence thesis by A10, A11, RLVECT_1:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      let X,Y be right_zeroed non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> right_zeroed;

      coherence

      proof

        for u be Element of ( Prod_of_RLS (X,Y)) holds (u + ( 0. ( Prod_of_RLS (X,Y)))) = u

        proof

          let u be Element of ( Prod_of_RLS (X,Y));

          consider x,y be object such that

           A1: x in the carrier of X and

           A2: y in the carrier of Y and

           A3: u = [x, y] by ZFMISC_1:def 2;

          reconsider y as VECTOR of Y by A2;

          reconsider x as VECTOR of X by A1;

          

           A4: (y + ( 0. Y)) = y by RLVECT_1:def 4;

          (x + ( 0. X)) = x by RLVECT_1:def 4;

          hence thesis by A3, A4, Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let X,Y be right_complementable non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> right_complementable;

      coherence

      proof

        let u be Element of ( Prod_of_RLS (X,Y));

        consider x,y be object such that

         A1: x in the carrier of X and

         A2: y in the carrier of Y and

         A3: u = [x, y] by ZFMISC_1:def 2;

        reconsider x as VECTOR of X by A1;

        consider x1 be VECTOR of X such that

         A4: (x + x1) = ( 0. X) by ALGSTR_0:def 11;

        reconsider y as VECTOR of Y by A2;

        consider y1 be VECTOR of Y such that

         A5: (y + y1) = ( 0. Y) by ALGSTR_0:def 11;

        set u1 = [x1, y1];

        reconsider u1 as Element of ( Prod_of_RLS (X,Y));

        take u1;

        thus thesis by A3, A4, A5, Def1;

      end;

    end

    registration

      let X,Y be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      cluster ( Prod_of_RLS (X,Y)) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        

         A1: for a be Real holds for u1,u2 be VECTOR of ( Prod_of_RLS (X,Y)) holds (a * (u1 + u2)) = ((a * u1) + (a * u2))

        proof

          let a be Real;

          reconsider a as Real;

          let u1,u2 be VECTOR of ( Prod_of_RLS (X,Y));

          consider x1,y1 be object such that

           A2: x1 in the carrier of X and

           A3: y1 in the carrier of Y and

           A4: u1 = [x1, y1] by ZFMISC_1:def 2;

          reconsider x1 as VECTOR of X by A2;

          consider x2,y2 be object such that

           A5: x2 in the carrier of X and

           A6: y2 in the carrier of Y and

           A7: u2 = [x2, y2] by ZFMISC_1:def 2;

          reconsider y2 as VECTOR of Y by A6;

          reconsider x2 as VECTOR of X by A5;

          reconsider y1 as VECTOR of Y by A3;

          

           A8: (a * (x1 + x2)) = ((a * x1) + (a * x2)) by RLVECT_1:def 5;

          (u1 + u2) = [(x1 + x2), (y1 + y2)] by A4, A7, Def1;

          then

           A9: (a * (u1 + u2)) = [(a * (x1 + x2)), (a * (y1 + y2))] by Def2;

          

           A10: (a * (y1 + y2)) = ((a * y1) + (a * y2)) by RLVECT_1:def 5;

          

           A11: (a * u2) = [(a * x2), (a * y2)] by A7, Def2;

          (a * u1) = [(a * x1), (a * y1)] by A4, Def2;

          hence thesis by A9, A11, A8, A10, Def1;

        end;

        

         A12: for a,b be Real holds for u be VECTOR of ( Prod_of_RLS (X,Y)) holds ((a * b) * u) = (a * (b * u))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let u be VECTOR of ( Prod_of_RLS (X,Y));

          consider x,y be object such that

           A13: x in the carrier of X and

           A14: y in the carrier of Y and

           A15: u = [x, y] by ZFMISC_1:def 2;

          reconsider y as VECTOR of Y by A14;

          reconsider x as VECTOR of X by A13;

          (b * u) = [(b * x), (b * y)] by A15, Def2;

          then

           A16: (a * (b * u)) = [(a * (b * x)), (a * (b * y))] by Def2;

          

           A17: ((a * b) * y) = (a * (b * y)) by RLVECT_1:def 7;

          ((a * b) * x) = (a * (b * x)) by RLVECT_1:def 7;

          hence thesis by A15, A16, A17, Def2;

        end;

        

         A18: for a,b be Real holds for u be VECTOR of ( Prod_of_RLS (X,Y)) holds ((a + b) * u) = ((a * u) + (b * u))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let u be VECTOR of ( Prod_of_RLS (X,Y));

          consider x,y be object such that

           A19: x in the carrier of X and

           A20: y in the carrier of Y and

           A21: u = [x, y] by ZFMISC_1:def 2;

          reconsider y as VECTOR of Y by A20;

          reconsider x as VECTOR of X by A19;

          

           A22: (b * u) = [(b * x), (b * y)] by A21, Def2;

          (a * u) = [(a * x), (a * y)] by A21, Def2;

          then

           A23: ((a * u) + (b * u)) = [((a * x) + (b * x)), ((a * y) + (b * y))] by A22, Def1;

          

           A24: ((a + b) * y) = ((a * y) + (b * y)) by RLVECT_1:def 6;

          ((a + b) * x) = ((a * x) + (b * x)) by RLVECT_1:def 6;

          hence thesis by A21, A23, A24, Def2;

        end;

        for u be VECTOR of ( Prod_of_RLS (X,Y)) holds (1 * u) = u

        proof

          let u be VECTOR of ( Prod_of_RLS (X,Y));

          consider x,y be object such that

           A25: x in the carrier of X and

           A26: y in the carrier of Y and

           A27: u = [x, y] by ZFMISC_1:def 2;

          reconsider y as VECTOR of Y by A26;

          reconsider x as VECTOR of X by A25;

          

           A28: (1 * y) = y by RLVECT_1:def 8;

          (1 * x) = x by RLVECT_1:def 8;

          hence thesis by A27, A28, Def2;

        end;

        hence thesis by A1, A18, A12;

      end;

    end

    theorem :: CONVFUN1:3

    

     Th3: for X,Y be RealLinearSpace, n be Nat, x be FinSequence of the carrier of X, y be FinSequence of the carrier of Y, z be FinSequence of the carrier of ( Prod_of_RLS (X,Y)) st ( len x) = n & ( len y) = n & ( len z) = n & (for i be Nat st i in ( Seg n) holds (z . i) = [(x . i), (y . i)]) holds ( Sum z) = [( Sum x), ( Sum y)]

    proof

      let X,Y be RealLinearSpace;

      defpred P[ Nat] means for x be FinSequence of the carrier of X, y be FinSequence of the carrier of Y, z be FinSequence of the carrier of ( Prod_of_RLS (X,Y)) st ( len x) = $1 & ( len y) = $1 & ( len z) = $1 & for i be Nat st i in ( Seg $1) holds (z . i) = [(x . i), (y . i)] holds ( Sum z) = [( Sum x), ( Sum y)];

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let x be FinSequence of the carrier of X, y be FinSequence of the carrier of Y, z be FinSequence of the carrier of ( Prod_of_RLS (X,Y));

          assume that

           A3: ( len x) = (n + 1) and

           A4: ( len y) = (n + 1) and

           A5: ( len z) = (n + 1) and

           A6: for i be Nat st i in ( Seg (n + 1)) holds (z . i) = [(x . i), (y . i)];

          

           A7: ( 0 + n) <= (1 + n) by XREAL_1: 6;

          then

           A8: ( len (y | n)) = n by A4, FINSEQ_1: 59;

          

           A9: ( Seg n) c= ( Seg (n + 1)) by A7, FINSEQ_1: 5;

          

           A10: for i be Nat st i in ( Seg n) holds ((z | n) . i) = [((x | n) . i), ((y | n) . i)]

          proof

            let i be Nat;

            assume

             A11: i in ( Seg n);

            then

             A12: i <= n by FINSEQ_1: 1;

            then

             A13: ((y | n) . i) = (y . i) by FINSEQ_3: 112;

            

             A14: ((z | n) . i) = (z . i) by A12, FINSEQ_3: 112;

            ((x | n) . i) = (x . i) by A12, FINSEQ_3: 112;

            hence thesis by A6, A9, A11, A13, A14;

          end;

          

           A15: for i be Element of NAT st i in ( Seg (n + 1)) holds (x /. i) = (x . i) & (y /. i) = (y . i) & (z /. i) = (z . i)

          proof

            let i be Element of NAT ;

            assume

             A16: i in ( Seg (n + 1));

            then

             A17: i <= (n + 1) by FINSEQ_1: 1;

            1 <= i by A16, FINSEQ_1: 1;

            hence thesis by A3, A4, A5, A17, FINSEQ_4: 15;

          end;

          

           A18: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

          then

           A19: (y /. (n + 1)) = (y . (n + 1)) by A15;

          (z | n) = (z | ( Seg n)) by FINSEQ_1:def 15;

          then z = ((z | n) ^ <*(z . (n + 1))*>) by A5, FINSEQ_3: 55;

          then z = ((z | n) ^ <*(z /. (n + 1))*>) by A15, A18;

          

          then

           A20: ( Sum z) = (( Sum (z | n)) + ( Sum <*(z /. (n + 1))*>)) by RLVECT_1: 41

          .= (( Sum (z | n)) + (z /. (n + 1))) by RLVECT_1: 44;

          (y | n) = (y | ( Seg n)) by FINSEQ_1:def 15;

          then y = ((y | n) ^ <*(y . (n + 1))*>) by A4, FINSEQ_3: 55;

          then y = ((y | n) ^ <*(y /. (n + 1))*>) by A15, A18;

          

          then

           A21: ( Sum y) = (( Sum (y | n)) + ( Sum <*(y /. (n + 1))*>)) by RLVECT_1: 41

          .= (( Sum (y | n)) + (y /. (n + 1))) by RLVECT_1: 44;

          (x | n) = (x | ( Seg n)) by FINSEQ_1:def 15;

          then x = ((x | n) ^ <*(x . (n + 1))*>) by A3, FINSEQ_3: 55;

          then x = ((x | n) ^ <*(x /. (n + 1))*>) by A15, A18;

          

          then

           A22: ( Sum x) = (( Sum (x | n)) + ( Sum <*(x /. (n + 1))*>)) by RLVECT_1: 41

          .= (( Sum (x | n)) + (x /. (n + 1))) by RLVECT_1: 44;

          

           A23: (z /. (n + 1)) = (z . (n + 1)) by A15, A18;

          (x /. (n + 1)) = (x . (n + 1)) by A15, A18;

          then

           A24: (z /. (n + 1)) = [(x /. (n + 1)), (y /. (n + 1))] by A6, A19, A23, FINSEQ_1: 4;

          

           A25: ( len (z | n)) = n by A5, A7, FINSEQ_1: 59;

          ( len (x | n)) = n by A3, A7, FINSEQ_1: 59;

          then ( Sum (z | n)) = [( Sum (x | n)), ( Sum (y | n))] by A2, A8, A25, A10;

          hence thesis by A24, A22, A21, A20, Def1;

        end;

      end;

      

       A26: P[ 0 ]

      proof

        let x be FinSequence of the carrier of X, y be FinSequence of the carrier of Y, z be FinSequence of the carrier of ( Prod_of_RLS (X,Y));

        assume that

         A27: ( len x) = 0 and

         A28: ( len y) = 0 and

         A29: ( len z) = 0 and for i be Nat st i in ( Seg 0 ) holds (z . i) = [(x . i), (y . i)];

        x = ( <*> the carrier of X) by A27;

        then

         A30: ( Sum x) = ( 0. X) by RLVECT_1: 43;

        z = ( <*> the carrier of ( Prod_of_RLS (X,Y))) by A29;

        then

         A31: ( Sum z) = ( 0. ( Prod_of_RLS (X,Y))) by RLVECT_1: 43;

        y = ( <*> the carrier of Y) by A28;

        hence thesis by A30, A31, RLVECT_1: 43;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A26, A1);

    end;

    begin

    definition

      :: CONVFUN1:def4

      func RLS_Real -> non empty RLSStruct equals RLSStruct (# REAL , ( In ( 0 , REAL )), addreal , multreal #);

      correctness ;

    end

    registration

      cluster RLS_Real -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        thus RLS_Real is Abelian

        proof

          let v,w be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          reconsider wr = w as Real;

          

          thus (v + w) = (vr + wr) by BINOP_2:def 9

          .= (w + v) by BINOP_2:def 9;

        end;

        thus RLS_Real is add-associative

        proof

          let u,v,w be VECTOR of RLS_Real ;

          reconsider ur = u as Real;

          reconsider vr = v as Real;

          reconsider wr = w as Real;

          (v + w) = (vr + wr) by BINOP_2:def 9;

          then

           A1: (u + (v + w)) = (ur + (vr + wr)) by BINOP_2:def 9;

          (u + v) = (ur + vr) by BINOP_2:def 9;

          then ((u + v) + w) = ((ur + vr) + wr) by BINOP_2:def 9;

          hence thesis by A1;

        end;

        thus RLS_Real is right_zeroed

        proof

          let v be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          

          thus (v + ( 0. RLS_Real )) = (vr + 0 ) by BINOP_2:def 9

          .= v;

        end;

        thus RLS_Real is right_complementable

        proof

          let v be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          reconsider w = ( - vr) as VECTOR of RLS_Real by XREAL_0:def 1;

          take w;

          

          thus (v + w) = (vr + ( - vr)) by BINOP_2:def 9

          .= ( 0. RLS_Real );

        end;

        thus for a be Real holds for v,w be VECTOR of RLS_Real holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Real;

          reconsider a as Real;

          let v,w be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          reconsider wr = w as Real;

          

           A2: (a * v) = (a * vr) by BINOP_2:def 11;

          

           A3: (a * w) = (a * wr) by BINOP_2:def 11;

          (v + w) = (vr + wr) by BINOP_2:def 9;

          

          then (a * (v + w)) = (a * (vr + wr)) by BINOP_2:def 11

          .= ((a * vr) + (a * wr))

          .= ((a * v) + (a * w)) by A2, A3, BINOP_2:def 9;

          hence thesis;

        end;

        thus for a,b be Real holds for v be VECTOR of RLS_Real holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let v be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          

           A4: (b * v) = (b * vr) by BINOP_2:def 11;

          (a * v) = (a * vr) by BINOP_2:def 11;

          

          then ((a * v) + (b * v)) = ((a * vr) + (b * vr)) by A4, BINOP_2:def 9

          .= ((a + b) * vr)

          .= ((a + b) * v) by BINOP_2:def 11;

          hence thesis;

        end;

        thus for a,b be Real holds for v be VECTOR of RLS_Real holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Real;

          reconsider a, b as Real;

          let v be VECTOR of RLS_Real ;

          reconsider vr = v as Real;

          (b * v) = (b * vr) by BINOP_2:def 11;

          

          then (a * (b * v)) = (a * (b * vr)) by BINOP_2:def 11

          .= ((a * b) * vr)

          .= ((a * b) * v) by BINOP_2:def 11;

          hence thesis;

        end;

        let v be VECTOR of RLS_Real ;

        reconsider vr = v as Real;

        

        thus (1 * v) = (1 * vr) by BINOP_2:def 11

        .= v;

      end;

    end

    

     Lm1: for X be non empty RLSStruct, x be VECTOR of X, u be VECTOR of ( Prod_of_RLS (X, RLS_Real )), p,w be Real st u = [x, w] holds (p * u) = [(p * x), (p * w)]

    proof

      let X be non empty RLSStruct, x be VECTOR of X, u be VECTOR of ( Prod_of_RLS (X, RLS_Real )), p,w be Real;

      reconsider y = w as VECTOR of RLS_Real by XREAL_0:def 1;

      assume

       A1: u = [x, w];

      (p * y) = (p * w) by BINOP_2:def 11;

      hence thesis by A1, Def2;

    end;

    

     Lm2: for X be non empty RLSStruct, x1,x2 be VECTOR of X, w1,w2 be Real, u1,u2 be VECTOR of ( Prod_of_RLS (X, RLS_Real )) st u1 = [x1, w1] & u2 = [x2, w2] holds (u1 + u2) = [(x1 + x2), (w1 + w2)]

    proof

      let X be non empty RLSStruct, x1,x2 be VECTOR of X, w1,w2 be Real, u1,u2 be VECTOR of ( Prod_of_RLS (X, RLS_Real ));

      reconsider y1 = w1 as VECTOR of RLS_Real by XREAL_0:def 1;

      reconsider y2 = w2 as VECTOR of RLS_Real by XREAL_0:def 1;

      assume that

       A1: u1 = [x1, w1] and

       A2: u2 = [x2, w2];

      (y1 + y2) = (w1 + w2) by BINOP_2:def 9;

      hence thesis by A1, A2, Def1;

    end;

    

     Lm3: for a be FinSequence of the carrier of RLS_Real , b be FinSequence of REAL st ( len a) = ( len b) & (for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i)) holds ( Sum a) = ( Sum b)

    proof

      let a be FinSequence of the carrier of RLS_Real , b be FinSequence of REAL ;

      defpred P[ Nat] means for a be FinSequence of the carrier of RLS_Real , b be FinSequence of REAL st ( len a) = $1 & ( len b) = $1 & (for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i)) holds ( Sum a) = ( Sum b);

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let a be FinSequence of the carrier of RLS_Real , b be FinSequence of REAL ;

          assume that

           A3: ( len a) = (n + 1) and

           A4: ( len b) = (n + 1) and

           A5: for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i);

          

           A6: ( 0 + n) <= (1 + n) by XREAL_1: 6;

          then

           A7: ( len (a | n)) = n by A3, FINSEQ_1: 59;

          

           A8: ( dom a) = ( Seg (n + 1)) by A3, FINSEQ_1:def 3;

          

           A9: for i be Element of NAT st i in ( Seg (n + 1)) holds (a . i) = (a /. i) & (a /. i) = (b . i)

          proof

            let i be Element of NAT ;

            assume

             A10: i in ( Seg (n + 1));

            then

             A11: i <= (n + 1) by FINSEQ_1: 1;

            1 <= i by A10, FINSEQ_1: 1;

            then (a /. i) = (a . i) by A3, A11, FINSEQ_4: 15;

            hence thesis by A5, A8, A10;

          end;

          

           A12: ( Seg n) c= ( Seg (n + 1)) by A6, FINSEQ_1: 5;

          

           A13: for i be Element of NAT st i in ( dom (a | n)) holds ((a | n) . i) = ((b | n) . i)

          proof

            let i be Element of NAT ;

            assume i in ( dom (a | n));

            then

             A14: i in ( Seg n) by A7, FINSEQ_1:def 3;

            then

             A15: i <= n by FINSEQ_1: 1;

            then

             A16: ((b | n) . i) = (b . i) by FINSEQ_3: 112;

            ((a | n) . i) = (a . i) by A15, FINSEQ_3: 112;

            hence thesis by A5, A8, A12, A14, A16;

          end;

          ( len (b | n)) = n by A4, A6, FINSEQ_1: 59;

          then

           A17: ( Sum (a | n)) = ( Sum (b | n)) by A2, A7, A13;

          (b | n) = (b | ( Seg n)) by FINSEQ_1:def 15;

          then

           A18: b = ((b | n) ^ <*(b . (n + 1))*>) by A4, FINSEQ_3: 55;

          

           A19: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

          then

           A20: (a /. (n + 1)) = (b . (n + 1)) by A9;

          (a | n) = (a | ( Seg n)) by FINSEQ_1:def 15;

          then a = ((a | n) ^ <*(a . (n + 1))*>) by A3, FINSEQ_3: 55;

          then a = ((a | n) ^ <*(a /. (n + 1))*>) by A9, A19;

          

          then ( Sum a) = (( Sum (a | n)) + ( Sum <*(a /. (n + 1))*>)) by RLVECT_1: 41

          .= (( Sum (a | n)) + (a /. (n + 1))) by RLVECT_1: 44

          .= (( Sum (b | n)) + (b . (n + 1))) by A17, A20, BINOP_2:def 9;

          hence thesis by A18, RVSUM_1: 74;

        end;

      end;

      

       A21: P[ 0 ]

      proof

        let a be FinSequence of the carrier of RLS_Real , b be FinSequence of REAL ;

        assume that

         A22: ( len a) = 0 and

         A23: ( len b) = 0 and for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i);

        a = ( <*> the carrier of RLS_Real ) by A22;

        then

         A24: ( Sum a) = ( 0. RLS_Real ) by RLVECT_1: 43;

        b = ( <*> REAL ) by A23;

        hence thesis by A24, RVSUM_1: 72;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A21, A1);

      hence thesis;

    end;

    begin

    

     Lm4: for F be FinSequence of ExtREAL , x be Element of ExtREAL holds ( Sum (F ^ <*x*>)) = (( Sum F) + x)

    proof

      let F be FinSequence of ExtREAL , x be Element of ExtREAL ;

      consider f be sequence of ExtREAL such that

       A1: ( Sum (F ^ <*x*>)) = (f . ( len (F ^ <*x*>))) and

       A2: (f . 0 ) = 0. and

       A3: for i be Nat st i < ( len (F ^ <*x*>)) holds (f . (i + 1)) = ((f . i) + ((F ^ <*x*>) . (i + 1))) by EXTREAL1:def 2;

      

       A4: ( len (F ^ <*x*>)) = (( len F) + ( len <*x*>)) by FINSEQ_1: 22

      .= (( len F) + 1) by FINSEQ_1: 39;

      for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)))

      proof

        let i be Nat;

        

         A5: 1 <= (i + 1) by NAT_1: 11;

        assume

         A6: i < ( len F);

        then (i + 1) <= ( len F) by INT_1: 7;

        then (i + 1) in ( Seg ( len F)) by A5, FINSEQ_1: 1;

        then

         A7: (i + 1) in ( dom F) by FINSEQ_1:def 3;

        i < ( len (F ^ <*x*>)) by A4, A6, NAT_1: 13;

        then (f . (i + 1)) = ((f . i) + ((F ^ <*x*>) . (i + 1))) by A3;

        hence thesis by A7, FINSEQ_1:def 7;

      end;

      then

       A8: ( Sum F) = (f . ( len F)) by A2, EXTREAL1:def 2;

      ( len F) < ( len (F ^ <*x*>)) by A4, NAT_1: 13;

      then (f . (( len F) + 1)) = ((f . ( len F)) + ((F ^ <*x*>) . (( len F) + 1))) by A3;

      hence thesis by A1, A4, A8, FINSEQ_1: 42;

    end;

    

     Lm5: for F be FinSequence of ExtREAL st not -infty in ( rng F) holds ( Sum F) <> -infty

    proof

      defpred P[ FinSequence of ExtREAL ] means not -infty in ( rng $1) implies ( Sum $1) <> -infty ;

      

       A1: for F be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of ExtREAL ;

        let x be Element of ExtREAL ;

        assume

         A2: P[F];

        

         A3: ( Sum (F ^ <*x*>)) = (( Sum F) + x) by Lm4;

        assume not -infty in ( rng (F ^ <*x*>));

        then

         A4: not -infty in (( rng F) \/ ( rng <*x*>)) by FINSEQ_1: 31;

        then not -infty in ( rng <*x*>) by XBOOLE_0:def 3;

        then not -infty in {x} by FINSEQ_1: 38;

        then x <> -infty by TARSKI:def 1;

        hence thesis by A2, A4, A3, XBOOLE_0:def 3, XXREAL_3: 17;

      end;

      

       A5: P[( <*> ExtREAL )] by EXTREAL1: 7;

      thus for F be FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A5, A1);

    end;

    

     Lm6: for F be FinSequence of ExtREAL st +infty in ( rng F) & not -infty in ( rng F) holds ( Sum F) = +infty

    proof

      defpred P[ FinSequence of ExtREAL ] means +infty in ( rng $1) & not -infty in ( rng $1) implies ( Sum $1) = +infty ;

      

       A1: for F be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of ExtREAL ;

        let x be Element of ExtREAL ;

        assume

         A2: P[F];

        assume that

         A3: +infty in ( rng (F ^ <*x*>)) and

         A4: not -infty in ( rng (F ^ <*x*>));

        

         A5: ( Sum (F ^ <*x*>)) = (( Sum F) + x) by Lm4;

         +infty in (( rng F) \/ ( rng <*x*>)) by A3, FINSEQ_1: 31;

        then +infty in ( rng F) or +infty in ( rng <*x*>) by XBOOLE_0:def 3;

        then

         A6: +infty in ( rng F) or +infty in {x} by FINSEQ_1: 38;

        

         A7: not -infty in (( rng F) \/ ( rng <*x*>)) by A4, FINSEQ_1: 31;

        then not -infty in ( rng F) by XBOOLE_0:def 3;

        then

         A8: ( Sum F) <> -infty by Lm5;

         not -infty in ( rng <*x*>) by A7, XBOOLE_0:def 3;

        then not -infty in {x} by FINSEQ_1: 38;

        then

         A9: x <> -infty by TARSKI:def 1;

        per cases by A6, TARSKI:def 1;

          suppose +infty in ( rng F);

          hence thesis by A2, A7, A9, A5, XBOOLE_0:def 3, XXREAL_3:def 2;

        end;

          suppose +infty = x;

          hence thesis by A5, A8, XXREAL_3:def 2;

        end;

      end;

      

       A10: P[( <*> ExtREAL )];

      thus for F be FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A10, A1);

    end;

    

     Lm7: for a be FinSequence of ExtREAL , b be FinSequence of REAL st ( len a) = ( len b) & (for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i)) holds ( Sum a) = ( Sum b)

    proof

      let a be FinSequence of ExtREAL , b be FinSequence of REAL ;

      defpred P[ Nat] means for a be FinSequence of ExtREAL , b be FinSequence of REAL st ( len a) = $1 & ( len b) = $1 & (for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i)) holds ( Sum a) = ( Sum b);

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        thus P[(n + 1)]

        proof

          let a be FinSequence of ExtREAL , b be FinSequence of REAL ;

          assume that

           A3: ( len a) = (n + 1) and

           A4: ( len b) = (n + 1) and

           A5: for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i);

          

           A6: ( dom a) = ( Seg (n + 1)) by A3, FINSEQ_1:def 3;

          then

           A7: (a . (n + 1)) = (b . (n + 1)) by A5, FINSEQ_1: 4;

          

           A8: ( 0 + n) <= (1 + n) by XREAL_1: 6;

          then

           A9: ( len (a | n)) = n by A3, FINSEQ_1: 59;

          

           A10: ( Seg n) c= ( Seg (n + 1)) by A8, FINSEQ_1: 5;

          

           A11: for i be Element of NAT st i in ( dom (a | n)) holds ((a | n) . i) = ((b | n) . i)

          proof

            let i be Element of NAT ;

            assume i in ( dom (a | n));

            then

             A12: i in ( Seg n) by A9, FINSEQ_1:def 3;

            then

             A13: i <= n by FINSEQ_1: 1;

            then

             A14: ((b | n) . i) = (b . i) by FINSEQ_3: 112;

            ((a | n) . i) = (a . i) by A13, FINSEQ_3: 112;

            hence thesis by A5, A6, A10, A12, A14;

          end;

          ( len (b | n)) = n by A4, A8, FINSEQ_1: 59;

          then

           A15: ( Sum (a | n)) = ( Sum (b | n)) by A2, A9, A11;

          (b | n) = (b | ( Seg n)) by FINSEQ_1:def 15;

          then

           A16: b = ((b | n) ^ <*(b . (n + 1))*>) by A4, FINSEQ_3: 55;

          (a | n) = (a | ( Seg n)) by FINSEQ_1:def 15;

          then a = ((a | n) ^ <*(a . (n + 1))*>) by A3, FINSEQ_3: 55;

          

          then ( Sum a) = (( Sum (a | n)) + (a . (n + 1))) by Lm4

          .= (( Sum (b | n)) + (b . (n + 1))) by A15, A7, SUPINF_2: 1;

          hence thesis by A16, RVSUM_1: 74;

        end;

      end;

      

       A17: P[ 0 ]

      proof

        let a be FinSequence of ExtREAL , b be FinSequence of REAL ;

        assume that

         A18: ( len a) = 0 and

         A19: ( len b) = 0 and for i be Element of NAT st i in ( dom a) holds (a . i) = (b . i);

        a = ( <*> ExtREAL ) by A18;

        then

         A20: ( Sum a) = 0. by EXTREAL1: 7;

        b = ( <*> ExtREAL ) by A19;

        hence thesis by A20, RVSUM_1: 72;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A1);

      hence thesis;

    end;

    

     Lm8: for n be Element of NAT , a be FinSequence of ExtREAL , b be FinSequence of the carrier of RLS_Real st ( len a) = n & ( len b) = n & (for i be Element of NAT st i in ( Seg n) holds (a . i) = (b . i)) holds ( Sum a) = ( Sum b)

    proof

      let n be Element of NAT , a be FinSequence of ExtREAL , b be FinSequence of the carrier of RLS_Real ;

      assume that

       A1: ( len a) = n and

       A2: ( len b) = n and

       A3: for i be Element of NAT st i in ( Seg n) holds (a . i) = (b . i);

      set c = b;

      reconsider c as FinSequence of REAL ;

      ( dom a) = ( Seg n) by A1, FINSEQ_1:def 3;

      then

       A4: ( Sum a) = ( Sum c) by A1, A2, A3, Lm7;

      

       A5: for i be Element of NAT st i in ( dom b) holds (b . i) = (c . i);

      ( len b) = ( len c);

      hence thesis by A4, A5, Lm3;

    end;

    

     Lm9: for F be FinSequence of ExtREAL st ( rng F) c= { 0. } holds ( Sum F) = 0.

    proof

      let F be FinSequence of ExtREAL ;

      defpred P[ FinSequence of ExtREAL ] means ( rng $1) c= { 0. } implies ( Sum $1) = 0. ;

      assume

       A1: ( rng F) c= { 0. };

      

       A2: for F be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of ExtREAL ;

        let x be Element of ExtREAL ;

        assume

         A3: P[F];

        assume ( rng (F ^ <*x*>)) c= { 0. };

        then

         A4: (( rng F) \/ ( rng <*x*>)) c= { 0. } by FINSEQ_1: 31;

        then ( rng <*x*>) c= { 0. } by XBOOLE_1: 11;

        then {x} c= { 0. } by FINSEQ_1: 38;

        then x in { 0. } by ZFMISC_1: 31;

        then

         A5: x = 0. by TARSKI:def 1;

        

        thus ( Sum (F ^ <*x*>)) = (( Sum F) + x) by Lm4

        .= 0. by A3, A4, A5, XBOOLE_1: 11;

      end;

      

       A6: P[( <*> ExtREAL )] by EXTREAL1: 7;

      for F be FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A6, A2);

      hence thesis by A1;

    end;

    

     Lm10: for F be FinSequence of REAL st ( rng F) c= { 0 } holds ( Sum F) = 0

    proof

      let F be FinSequence of REAL ;

      defpred P[ FinSequence of REAL ] means ( rng $1) c= { 0 } implies ( Sum $1) = 0 ;

      

       A1: for F be FinSequence of REAL holds for x be Element of REAL st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of REAL ;

        let x be Element of REAL ;

        assume

         A2: P[F];

        assume ( rng (F ^ <*x*>)) c= { 0 };

        then

         A3: (( rng F) \/ ( rng <*x*>)) c= { 0 } by FINSEQ_1: 31;

        then ( rng <*x*>) c= { 0 } by XBOOLE_1: 11;

        then {x} c= { 0 } by FINSEQ_1: 38;

        then

         A4: x in { 0 } by ZFMISC_1: 31;

        

        thus ( Sum (F ^ <*x*>)) = (( Sum F) + x) by RVSUM_1: 74

        .= 0 by A2, A3, A4, TARSKI:def 1, XBOOLE_1: 11;

      end;

      assume

       A5: ( rng F) c= { 0 };

      

       A6: P[( <*> REAL )] by RVSUM_1: 72;

      for F be FinSequence of REAL holds P[F] from FINSEQ_2:sch 2( A6, A1);

      hence thesis by A5;

    end;

    

     Lm11: for X be RealLinearSpace, F be FinSequence of the carrier of X st ( rng F) c= {( 0. X)} holds ( Sum F) = ( 0. X)

    proof

      let X be RealLinearSpace;

      defpred P[ FinSequence of the carrier of X] means ( rng $1) c= {( 0. X)} implies ( Sum $1) = ( 0. X);

      

       A1: for F be FinSequence of the carrier of X holds for x be Element of X st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of the carrier of X;

        let x be Element of X;

        assume

         A2: P[F];

        assume ( rng (F ^ <*x*>)) c= {( 0. X)};

        then

         A3: (( rng F) \/ ( rng <*x*>)) c= {( 0. X)} by FINSEQ_1: 31;

        then ( rng <*x*>) c= {( 0. X)} by XBOOLE_1: 11;

        then {x} c= {( 0. X)} by FINSEQ_1: 38;

        then x in {( 0. X)} by ZFMISC_1: 31;

        then

         A4: x = ( 0. X) by TARSKI:def 1;

        

        thus ( Sum (F ^ <*x*>)) = (( Sum F) + ( Sum <*x*>)) by RLVECT_1: 41

        .= (( Sum F) + x) by RLVECT_1: 44

        .= ( 0. X) by A2, A3, A4, XBOOLE_1: 11;

      end;

      let F be FinSequence of the carrier of X;

      assume

       A5: ( rng F) c= {( 0. X)};

      

       A6: P[( <*> the carrier of X)] by RLVECT_1: 43;

      for F be FinSequence of the carrier of X holds P[F] from FINSEQ_2:sch 2( A6, A1);

      hence thesis by A5;

    end;

    begin

    definition

      let X be non empty RLSStruct, f be Function of the carrier of X, ExtREAL ;

      :: CONVFUN1:def5

      func epigraph f -> Subset of ( Prod_of_RLS (X, RLS_Real )) equals { [x, y] where x be Element of X, y be Element of REAL : (f . x) <= y };

      coherence

      proof

        deffunc f( Element of X, Element of REAL ) = [$1, $2];

        defpred P[ Element of X, Real] means (f . $1) <= $2;

        { f(x,y) where x be Element of X, y be Element of REAL : P[x, y] } is Subset of [:the carrier of X, REAL :] from DOMAIN_1:sch 9;

        hence thesis;

      end;

    end

    definition

      let X be non empty RLSStruct, f be Function of the carrier of X, ExtREAL ;

      :: CONVFUN1:def6

      attr f is convex means ( epigraph f) is convex;

    end

    

     Lm12: for w1,w2 be R_eal, wr1,wr2,p1,p2 be Real st w1 = wr1 & w2 = wr2 holds ((p1 * wr1) + (p2 * wr2)) = ((p1 * w1) + (p2 * w2))

    proof

      let w1,w2 be R_eal, wr1,wr2,p1,p2 be Real;

      assume that

       A1: w1 = wr1 and

       A2: w2 = wr2;

      

       A3: (p2 * wr2) = (p2 * w2) by A2, EXTREAL1: 1;

      (p1 * wr1) = (p1 * w1) by A1, EXTREAL1: 1;

      hence thesis by A3, SUPINF_2: 1;

    end;

    theorem :: CONVFUN1:4

    

     Th4: for X be non empty RLSStruct, f be Function of the carrier of X, ExtREAL st (for x be VECTOR of X holds (f . x) <> -infty ) holds f is convex iff for x1,x2 be VECTOR of X, p be Real st 0 < p & p < 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)))

    proof

      let X be non empty RLSStruct, f be Function of the carrier of X, ExtREAL ;

      assume

       A1: for x be VECTOR of X holds (f . x) <> -infty ;

      thus f is convex implies for x1,x2 be VECTOR of X, p be Real st 0 < p & p < 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)))

      proof

        assume f is convex;

        then

         A2: ( epigraph f) is convex;

        let x1,x2 be VECTOR of X, p be Real;

        assume that

         A3: 0 < p and

         A4: p < 1;

        set p2 = (1 - p);

        set p1 = p;

        

         A5: (1 - p) > 0 by A4, XREAL_1: 50;

        per cases by A1, XXREAL_0: 14;

          suppose

           A6: (f . x1) in REAL & (f . x2) in REAL ;

          then

          reconsider w2 = (f . x2) as Element of REAL ;

          reconsider w1 = (f . x1) as Element of REAL by A6;

          reconsider u1 = [x1, w1] as VECTOR of ( Prod_of_RLS (X, RLS_Real ));

          reconsider u2 = [x2, w2] as VECTOR of ( Prod_of_RLS (X, RLS_Real ));

          

           A7: [x2, w2] in ( epigraph f);

          

           A8: (p * u1) = [(p * x1), (p * w1)] by Lm1;

          

           A9: ((1 - p) * u2) = [((1 - p) * x2), ((1 - p) * w2)] by Lm1;

           [x1, w1] in ( epigraph f);

          then ((p * u1) + ((1 - p) * u2)) in ( epigraph f) by A2, A3, A4, A7, CONVEX1:def 2;

          then [((p * x1) + ((1 - p) * x2)), ((p * w1) + ((1 - p) * w2))] in ( epigraph f) by A8, A9, Lm2;

          then

          consider x0 be Element of X, y0 be Element of REAL such that

           A10: [((p * x1) + ((1 - p) * x2)), ((p * w1) + ((1 - p) * w2))] = [x0, y0] and

           A11: (f . x0) <= y0;

          

           A12: y0 = ((p * w1) + ((1 - p) * w2)) by A10, XTUPLE_0: 1;

          x0 = ((p * x1) + ((1 - p) * x2)) by A10, XTUPLE_0: 1;

          hence thesis by A11, A12, Lm12;

        end;

          suppose

           A13: (f . x1) = +infty & (f . x2) in REAL ;

          

           A14: (p2 * (f . x2)) in REAL by A13, XREAL_0:def 1;

          (p1 * (f . x1)) = +infty by A3, A13, XXREAL_3:def 5;

          then ((p1 * (f . x1)) + (p2 * (f . x2))) = +infty by A14, XXREAL_3:def 2;

          hence thesis by XXREAL_0: 4;

        end;

          suppose

           A15: (f . x1) in REAL & (f . x2) = +infty ;

          

           A16: (p1 * (f . x1)) in REAL by A15, XREAL_0:def 1;

          (p2 * (f . x2)) = +infty by A5, A15, XXREAL_3:def 5;

          then ((p1 * (f . x1)) + (p2 * (f . x2))) = +infty by A16, XXREAL_3:def 2;

          hence thesis by XXREAL_0: 4;

        end;

          suppose

           A17: (f . x1) = +infty & (f . x2) = +infty ;

          then (p2 * (f . x2)) = +infty by A5, XXREAL_3:def 5;

          then ((p1 * (f . x1)) + (p2 * (f . x2))) = +infty by A3, A17, XXREAL_3:def 2;

          hence thesis by XXREAL_0: 4;

        end;

      end;

      assume

       A18: for x1,x2 be VECTOR of X, p be Real st 0 < p & p < 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)));

      for u1,u2 be VECTOR of ( Prod_of_RLS (X, RLS_Real )), p be Real st 0 < p & p < 1 & u1 in ( epigraph f) & u2 in ( epigraph f) holds ((p * u1) + ((1 - p) * u2)) in ( epigraph f)

      proof

        let u1,u2 be VECTOR of ( Prod_of_RLS (X, RLS_Real )), p be Real;

        assume that

         A19: 0 < p and

         A20: p < 1 and

         A21: u1 in ( epigraph f) and

         A22: u2 in ( epigraph f);

        reconsider pp = p as Real;

        thus ((p * u1) + ((1 - p) * u2)) in ( epigraph f)

        proof

          consider x2 be Element of X, y2 be Element of REAL such that

           A23: u2 = [x2, y2] and

           A24: (f . x2) <= y2 by A22;

          

           A25: ((1 - p) * u2) = [((1 - p) * x2), ((1 - p) * y2)] by A23, Lm1;

          (f . x2) <> +infty by A24, XXREAL_0: 9;

          then

          reconsider w2 = (f . x2) as Element of REAL by A1, XXREAL_0: 14;

          consider x1 be Element of X, y1 be Element of REAL such that

           A26: u1 = [x1, y1] and

           A27: (f . x1) <= y1 by A21;

          (f . x1) <> +infty by A27, XXREAL_0: 9;

          then

          reconsider w1 = (f . x1) as Element of REAL by A1, XXREAL_0: 14;

          (1 - p) > 0 by A20, XREAL_1: 50;

          then ((1 - p) * w2) <= ((1 - p) * y2) by A24, XREAL_1: 64;

          then

           A28: ((p * w1) + ((1 - p) * w2)) <= ((p * w1) + ((1 - p) * y2)) by XREAL_1: 6;

          (p * w1) <= (p * y1) by A19, A27, XREAL_1: 64;

          then ((p * w1) + ((1 - p) * y2)) <= ((p * y1) + ((1 - p) * y2)) by XREAL_1: 6;

          then

           A29: ((p * w1) + ((1 - p) * w2)) <= ((p * y1) + ((1 - p) * y2)) by A28, XXREAL_0: 2;

          

           A30: ((p * w1) + ((1 - p) * w2)) in REAL by XREAL_0:def 1;

          

           A31: ((p * w1) + ((1 - p) * w2)) = ((p * (f . x1)) + ((1 - p) * (f . x2))) by Lm12;

          then (f . ((pp * x1) + ((1 - pp) * x2))) <> +infty by A18, A19, A20, XXREAL_0: 9, A30;

          then

          reconsider w = (f . ((p * x1) + ((1 - p) * x2))) as Element of REAL by A1, XXREAL_0: 14;

          

           A32: ((p * y1) + ((1 - p) * y2)) in REAL by XREAL_0:def 1;

          w <= ((pp * w1) + ((1 - pp) * w2)) by A18, A19, A20, A31;

          then (f . ((pp * x1) + ((1 - pp) * x2))) <= ((p * y1) + ((1 - p) * y2)) by A29, XXREAL_0: 2;

          then

           A33: [((p * x1) + ((1 - p) * x2)), ((p * y1) + ((1 - p) * y2))] in { [x, y] where x be Element of X, y be Element of REAL : (f . x) <= y } by A32;

          (p * u1) = [(p * x1), (p * y1)] by A26, Lm1;

          then ((p * u1) + ((1 - p) * u2)) = [((p * x1) + ((1 - p) * x2)), ((p * y1) + ((1 - p) * y2))] by A25, Lm2;

          hence thesis by A33;

        end;

      end;

      then ( epigraph f) is convex by CONVEX1:def 2;

      hence thesis;

    end;

    theorem :: CONVFUN1:5

    for X be RealLinearSpace, f be Function of the carrier of X, ExtREAL st (for x be VECTOR of X holds (f . x) <> -infty ) holds f is convex iff for x1,x2 be VECTOR of X, p be Real st 0 <= p & p <= 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)))

    proof

      let X be RealLinearSpace, f be Function of the carrier of X, ExtREAL ;

      assume

       A1: for x be VECTOR of X holds (f . x) <> -infty ;

      thus f is convex implies for x1,x2 be VECTOR of X, p be Real st 0 <= p & p <= 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)))

      proof

        assume

         A2: f is convex;

        let x1,x2 be VECTOR of X, p be Real;

        assume that

         A3: 0 <= p and

         A4: p <= 1;

        per cases ;

          suppose

           A5: p = 0 ;

          then

           A6: ((1 - p) * x2) = x2 by RLVECT_1:def 8;

          (p * x1) = ( 0. X) by A5, RLVECT_1: 10;

          then

           A7: ((p * x1) + ((1 - p) * x2)) = x2 by A6;

          

           A8: ((1 - p) * (f . x2)) = (f . x2) by A5, XXREAL_3: 81;

          (p * (f . x1)) = 0. by A5;

          hence thesis by A7, A8, XXREAL_3: 4;

        end;

          suppose

           A9: p = 1;

          then

           A10: ((1 - p) * x2) = ( 0. X) by RLVECT_1: 10;

          (p * x1) = x1 by A9, RLVECT_1:def 8;

          then

           A11: ((p * x1) + ((1 - p) * x2)) = x1 by A10;

          

           A12: (p * (f . x1)) = (f . x1) by A9, XXREAL_3: 81;

          ((1 - p) * (f . x2)) = 0. by A9;

          hence thesis by A11, A12, XXREAL_3: 4;

        end;

          suppose

           A13: p <> 0 & p <> 1;

          then p < 1 by A4, XXREAL_0: 1;

          hence thesis by A1, A2, A3, A13, Th4;

        end;

      end;

      assume for x1,x2 be VECTOR of X, p be Real st 0 <= p & p <= 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)));

      then for x1,x2 be VECTOR of X, p be Real st 0 < p & p < 1 holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)));

      hence thesis by A1, Th4;

    end;

    begin

    theorem :: CONVFUN1:6

    for f be PartFunc of REAL , REAL , g be Function of the carrier of RLS_Real , ExtREAL , X be Subset of RLS_Real st X c= ( dom f) & for x be Real holds (x in X implies (g . x) = (f . x)) & ( not x in X implies (g . x) = +infty ) holds g is convex iff f is_convex_on X & X is convex

    proof

      let f be PartFunc of REAL , REAL , g be Function of the carrier of RLS_Real , ExtREAL , X be Subset of RLS_Real ;

      assume that

       A1: X c= ( dom f) and

       A2: for x be Real holds (x in X implies (g . x) = (f . x)) & ( not x in X implies (g . x) = +infty );

      

       A3: for v be VECTOR of RLS_Real holds (g . v) <> -infty

      proof

        let v be VECTOR of RLS_Real ;

        reconsider x = v as Real;

        (f . x) in REAL by XREAL_0:def 1;

        hence thesis by A2;

      end;

      

       A4: for v be VECTOR of RLS_Real st v in X holds (g . v) in REAL

      proof

        let v be VECTOR of RLS_Real ;

        reconsider x = v as Real;

        assume v in X;

        then (g . x) = (f . x) by A2;

        hence thesis by XREAL_0:def 1;

      end;

      thus g is convex implies f is_convex_on X & X is convex

      proof

        assume

         A5: g is convex;

        for p be Real st 0 <= p & p <= 1 holds for x1,x2 be Real st x1 in X & x2 in X & ((p * x1) + ((1 - p) * x2)) in X holds (f . ((p * x1) + ((1 - p) * x2))) <= ((p * (f . x1)) + ((1 - p) * (f . x2)))

        proof

          let p be Real;

          assume that

           A6: 0 <= p and

           A7: p <= 1;

          let x1,x2 be Real;

          assume that

           A8: x1 in X and

           A9: x2 in X and

           A10: ((p * x1) + ((1 - p) * x2)) in X;

          

           A11: (f . x1) = (g . x1) by A2, A8;

          

           A12: (f . ((p * x1) + ((1 - p) * x2))) = (g . ((p * x1) + ((1 - p) * x2))) by A2, A10;

          

           A13: (f . x2) = (g . x2) by A2, A9;

          per cases ;

            suppose p = 0 ;

            hence thesis;

          end;

            suppose p = 1;

            hence thesis;

          end;

            suppose

             A14: p <> 0 & p <> 1;

            reconsider v2 = x2 as VECTOR of RLS_Real by XREAL_0:def 1;

            reconsider v1 = x1 as VECTOR of RLS_Real by XREAL_0:def 1;

            

             A15: ((1 - p) * v2) = ((1 - p) * x2) by BINOP_2:def 11;

            (p * v1) = (p * x1) by BINOP_2:def 11;

            then

             A16: (g . ((p * v1) + ((1 - p) * v2))) = (f . ((p * x1) + ((1 - p) * x2))) by A12, A15, BINOP_2:def 9;

            

             A17: p < 1 by A7, A14, XXREAL_0: 1;

            ((p * (f . v1)) + ((1 - p) * (f . v2))) = ((p * (g . v1)) + ((1 - p) * (g . v2))) by A11, A13, Lm12;

            hence thesis by A3, A5, A6, A14, A17, A16, Th4;

          end;

        end;

        hence f is_convex_on X by A1, RFUNCT_3:def 12;

        for v1,v2 be VECTOR of RLS_Real , p be Real st 0 < p & p < 1 & v1 in X & v2 in X holds ((p * v1) + ((1 - p) * v2)) in X

        proof

          let v1,v2 be VECTOR of RLS_Real , p be Real;

          assume that

           A18: 0 < p and

           A19: p < 1 and

           A20: v1 in X and

           A21: v2 in X;

          reconsider w1 = (g . v1), w2 = (g . v2) as Element of REAL by A4, A20, A21;

          

           A22: ((p * w1) + ((1 - p) * w2)) in REAL by XREAL_0:def 1;

          

           A23: ((p * w1) + ((1 - p) * w2)) = ((p * (g . v1)) + ((1 - p) * (g . v2))) by Lm12;

          (g . ((p * v1) + ((1 - p) * v2))) <= ((p * (g . v1)) + ((1 - p) * (g . v2))) by A3, A5, A18, A19, Th4;

          then (g . ((p * v1) + ((1 - p) * v2))) <> +infty by A23, XXREAL_0: 9, A22;

          hence thesis by A2;

        end;

        hence X is convex by CONVEX1:def 2;

      end;

      thus f is_convex_on X & X is convex implies g is convex

      proof

        assume that

         A24: f is_convex_on X and

         A25: X is convex;

        for v1,v2 be VECTOR of RLS_Real , p be Real st 0 < p & p < 1 holds (g . ((p * v1) + ((1 - p) * v2))) <= ((p * (g . v1)) + ((1 - p) * (g . v2)))

        proof

          let v1,v2 be VECTOR of RLS_Real , p be Real;

          assume that

           A26: 0 < p and

           A27: p < 1;

          reconsider x2 = v2 as Real;

          reconsider x1 = v1 as Real;

          reconsider p as Real;

          

           A28: (1 - p) > 0 by A27, XREAL_1: 50;

          per cases ;

            suppose

             A29: v1 in X & v2 in X;

            then

             A30: (f . x2) = (g . v2) by A2;

            (f . x1) = (g . v1) by A2, A29;

            then

             A31: ((p * (f . x1)) + ((1 - p) * (f . x2))) = ((p * (g . v1)) + ((1 - p) * (g . v2))) by A30, Lm12;

            

             A32: ((1 - p) * v2) = ((1 - p) * x2) by BINOP_2:def 11;

            (p * v1) = (p * x1) by BINOP_2:def 11;

            then

             A33: ((p * v1) + ((1 - p) * v2)) = ((p * x1) + ((1 - p) * x2)) by A32, BINOP_2:def 9;

            reconsider pc = ((p * x1) + ((1 - p) * x2)) as Real;

            

             A34: ((p * v1) + ((1 - p) * v2)) in X by A25, A26, A27, A29, CONVEX1:def 2;

            then (f . pc) = (g . ((p * v1) + ((1 - p) * v2))) by A2, A33;

            hence thesis by A24, A26, A27, A29, A34, A33, A31, RFUNCT_3:def 12;

          end;

            suppose

             A35: v1 in X & not v2 in X;

            then (g . x2) = +infty by A2;

            then

             A36: ((1 - p) * (g . v2)) = +infty by A28, XXREAL_3:def 5;

            reconsider w1 = (g . x1) as Element of REAL by A4, A35;

            (p * w1) = (p * (g . v1)) by EXTREAL1: 1;

            then ((p * (g . v1)) + ((1 - p) * (g . v2))) = +infty by A36, XXREAL_3:def 2;

            hence thesis by XXREAL_0: 4;

          end;

            suppose

             A37: not v1 in X & v2 in X;

            then (g . x1) = +infty by A2;

            then

             A38: (p * (g . v1)) = +infty by A26, XXREAL_3:def 5;

            reconsider w2 = (g . x2) as Element of REAL by A4, A37;

            ((1 - p) * w2) = ((1 - p) * (g . v2)) by EXTREAL1: 1;

            then ((p * (g . v1)) + ((1 - p) * (g . v2))) = +infty by A38, XXREAL_3:def 2;

            hence thesis by XXREAL_0: 4;

          end;

            suppose

             A39: not v1 in X & not v2 in X;

            then (g . x2) = +infty by A2;

            then

             A40: ((1 - p) * (g . v2)) = +infty by A28, XXREAL_3:def 5;

            (g . x1) = +infty by A2, A39;

            then ((p * (g . v1)) + ((1 - p) * (g . v2))) = +infty by A26, A40, XXREAL_3:def 2;

            hence thesis by XXREAL_0: 4;

          end;

        end;

        hence thesis by A3, Th4;

      end;

    end;

    begin

    theorem :: CONVFUN1:7

    

     Th7: for X be RealLinearSpace, M be Subset of X holds M is convex iff for n be non zero Nat, p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Nat st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M

    proof

      let X be RealLinearSpace, M be Subset of X;

      thus M is convex implies for n be non zero Nat, p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Nat st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M

      proof

        defpred P[ Nat] means for p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = $1 & ( len y) = $1 & ( len z) = $1 & ( Sum p) = 1 & (for i be Nat st i in ( Seg $1) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M;

        assume

         A1: M is convex;

        

         A2: for n be non zero Nat st P[n] holds P[(n + 1)]

        proof

          let n be non zero Nat;

          assume

           A3: P[n];

          thus for p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = (n + 1) & ( len y) = (n + 1) & ( len z) = (n + 1) & ( Sum p) = 1 & (for i be Nat st i in ( Seg (n + 1)) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M

          proof

            let p be FinSequence of REAL , y,z be FinSequence of the carrier of X;

            assume that

             A4: ( len p) = (n + 1) and

             A5: ( len y) = (n + 1) and

             A6: ( len z) = (n + 1) and

             A7: ( Sum p) = 1 and

             A8: for i be Nat st i in ( Seg (n + 1)) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M;

            set q = (1 - (p . (n + 1)));

            

             A9: ( dom (p | n)) = ( Seg ( len (p | n))) by FINSEQ_1:def 3;

            1 <= (n + 1) by NAT_1: 14;

            then 1 in ( Seg (n + 1)) by FINSEQ_1: 1;

            then (p . 1) > 0 by A8;

            then

             A10: ((p | n) . 1) > 0 by FINSEQ_3: 112, NAT_1: 14;

            (p | n) = (p | ( Seg n)) by FINSEQ_1:def 15;

            then p = ((p | n) ^ <*(p . (n + 1))*>) by A4, FINSEQ_3: 55;

            then

             A11: 1 = (( Sum (p | n)) + (p . (n + 1))) by A7, RVSUM_1: 74;

            

             A12: ( 0 + n) <= (1 + n) by XREAL_1: 6;

            then

             A13: ( len (p | n)) = n by A4, FINSEQ_1: 59;

            then

             A14: ( dom (p | n)) = ( Seg n) by FINSEQ_1:def 3;

            

             A15: ( Seg n) c= ( Seg (n + 1)) by A12, FINSEQ_1: 5;

            

             A16: for i be Nat st i in ( dom (p | n)) holds 0 <= ((p | n) . i)

            proof

              let i be Nat;

              assume

               A17: i in ( dom (p | n));

              then

               A18: i <= n by A14, FINSEQ_1: 1;

              (p . i) > 0 by A8, A14, A15, A17;

              hence thesis by A18, FINSEQ_3: 112;

            end;

            set y9 = (y | n);

            set p9 = ((1 / q) * (p | n));

            deffunc f( Nat) = ((p9 . $1) * (y9 /. $1));

            consider z9 be FinSequence of the carrier of X such that

             A19: ( len z9) = n and

             A20: for i be Nat st i in ( dom z9) holds (z9 . i) = f(i) from FINSEQ_2:sch 1;

            

             A21: ( len y9) = n by A5, A12, FINSEQ_1: 59;

            then

             A22: ( dom y9) = ( Seg n) by FINSEQ_1:def 3;

            

             A23: for i be Nat, v be VECTOR of X st i in ( dom z9) & v = ((z | n) . i) holds (z9 . i) = ((1 / q) * v)

            proof

              let i be Nat, v be VECTOR of X;

              assume that

               A24: i in ( dom z9) and

               A25: v = ((z | n) . i);

              

               A26: i in ( Seg n) by A19, A24, FINSEQ_1:def 3;

              then

               A27: (y9 /. i) = (y /. i) by A22, FINSEQ_4: 70;

              

               A28: i <= n by A26, FINSEQ_1: 1;

              then

               A29: ((z | n) . i) = (z . i) by FINSEQ_3: 112;

              (z9 . i) = ((p9 . i) * (y9 /. i)) by A20, A24

              .= (((1 / q) * ((p | n) . i)) * (y9 /. i)) by RVSUM_1: 44

              .= (((1 / q) * (p . i)) * (y9 /. i)) by A28, FINSEQ_3: 112

              .= ((1 / q) * ((p . i) * (y9 /. i))) by RLVECT_1:def 7

              .= ((1 / q) * v) by A8, A15, A25, A26, A29, A27;

              hence thesis;

            end;

            1 <= n by NAT_1: 14;

            then 1 in ( Seg n) by FINSEQ_1: 1;

            then

             A30: q > 0 by A11, A14, A16, A10, RVSUM_1: 85;

            ( dom p9) = ( Seg ( len p9)) by FINSEQ_1:def 3;

            then ( Seg ( len p9)) = ( Seg ( len (p | n))) by A9, VALUED_1:def 5;

            then

             A31: ( len p9) = n by A13, FINSEQ_1: 6;

            

             A32: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

            then

             A33: (y /. (n + 1)) in M by A8;

            

             A34: q < 1 by A8, A32, XREAL_1: 44;

            (z | n) = (z | ( Seg n)) by FINSEQ_1:def 15;

            then

             A35: z = ((z | n) ^ <*(z . (n + 1))*>) by A6, FINSEQ_3: 55;

            (z . (n + 1)) = ((p . (n + 1)) * (y /. (n + 1))) by A8, A32;

            

            then

             A36: ( Sum z) = (( Sum (z | n)) + ( Sum <*((p . (n + 1)) * (y /. (n + 1)))*>)) by A35, RLVECT_1: 41

            .= (( Sum (z | n)) + ((1 - q) * (y /. (n + 1)))) by RLVECT_1: 44;

            

             A37: ( dom z9) = ( Seg n) by A19, FINSEQ_1:def 3;

            

             A38: for i be Nat st i in ( Seg n) holds (p9 . i) > 0 & (z9 . i) = ((p9 . i) * (y9 /. i)) & (y9 /. i) in M

            proof

              (q " ) > 0 by A30;

              then

               A39: (1 / q) > 0 by XCMPLX_1: 215;

              let i be Nat;

              assume

               A40: i in ( Seg n);

              then

               A41: i <= n by FINSEQ_1: 1;

              

               A42: (p9 . i) = ((1 / q) * ((p | n) . i)) by RVSUM_1: 44

              .= ((1 / q) * (p . i)) by A41, FINSEQ_3: 112;

              

               A43: ( Seg n) c= ( Seg (n + 1)) by A12, FINSEQ_1: 5;

              then (p . i) > 0 by A8, A40;

              hence (p9 . i) > 0 by A39, A42;

              thus (z9 . i) = ((p9 . i) * (y9 /. i)) by A20, A37, A40;

              (y /. i) in M by A8, A40, A43;

              hence thesis by A22, A40, FINSEQ_4: 70;

            end;

            ( len (z | n)) = n by A6, A12, FINSEQ_1: 59;

            

            then

             A44: (q * ( Sum z9)) = (q * ((1 / q) * ( Sum (z | n)))) by A19, A23, RLVECT_1: 39

            .= ((q * (1 / q)) * ( Sum (z | n))) by RLVECT_1:def 7

            .= (1 * ( Sum (z | n))) by A30, XCMPLX_1: 106

            .= ( Sum (z | n)) by RLVECT_1:def 8;

            ( Sum p9) = ((1 / q) * q) by A11, RVSUM_1: 87

            .= 1 by A30, XCMPLX_1: 106;

            then ( Sum z9) in M by A3, A19, A31, A21, A38;

            hence thesis by A1, A33, A34, A30, A36, A44, CONVEX1:def 2;

          end;

        end;

        

         A45: P[1]

        proof

          let p be FinSequence of REAL , y,z be FinSequence of the carrier of X;

          assume that

           A46: ( len p) = 1 and ( len y) = 1 and

           A47: ( len z) = 1 and

           A48: ( Sum p) = 1 and

           A49: for i be Nat st i in ( Seg 1) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M;

          reconsider p1 = (p . 1) as Element of REAL by XREAL_0:def 1;

          p = <*p1*> by A46, FINSEQ_1: 40;

          then

           A50: (p . 1) = 1 by A48, FINSOP_1: 11;

          

           A51: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

          then (z . 1) = ((p . 1) * (y /. 1)) by A49;

          then

           A52: (z . 1) = (y /. 1) by A50, RLVECT_1:def 8;

          

           A53: z = <*(z . 1)*> by A47, FINSEQ_1: 40;

          (y /. 1) in M by A49, A51;

          hence thesis by A53, A52, RLVECT_1: 44;

        end;

        thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A45, A2);

      end;

      thus (for n be non zero Nat, p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Nat st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M) implies M is convex

      proof

        assume

         A54: for n be non zero Nat, p be FinSequence of REAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Nat st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M) holds ( Sum z) in M;

        for x1,x2 be VECTOR of X, r be Real st 0 < r & r < 1 & x1 in M & x2 in M holds ((r * x1) + ((1 - r) * x2)) in M

        proof

          let x1,x2 be VECTOR of X, r be Real;

          assume that

           A55: 0 < r and

           A56: r < 1 and

           A57: x1 in M and

           A58: x2 in M;

          set z = <*(r * x1), ((1 - r) * x2)*>;

          set y = <*x1, x2*>;

          reconsider r as Element of REAL by XREAL_0:def 1;

          reconsider r1 = (1 - r) as Element of REAL by XREAL_0:def 1;

          set p = <*r, r1*>;

          

           A59: for i be Nat st i in ( Seg 2) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (y /. i) in M

          proof

            let i be Nat;

            assume

             A60: i in ( Seg 2);

            per cases by A60, FINSEQ_1: 2, TARSKI:def 2;

              suppose

               A61: i = 1;

              then

               A62: (y /. i) = x1 by FINSEQ_4: 17;

              (p . i) = r by A61, FINSEQ_1: 44;

              hence thesis by A55, A57, A61, A62, FINSEQ_1: 44;

            end;

              suppose

               A63: i = 2;

              then

               A64: (y /. i) = x2 by FINSEQ_4: 17;

              (p . i) = (1 - r) by A63, FINSEQ_1: 44;

              hence thesis by A56, A58, A63, A64, FINSEQ_1: 44, XREAL_1: 50;

            end;

          end;

          

           A65: ( len y) = 2 by FINSEQ_1: 44;

          

           A66: ( Sum p) = (r + (1 - r)) by RVSUM_1: 77

          .= 1;

          

           A67: ( len z) = 2 by FINSEQ_1: 44;

          ( len p) = 2 by FINSEQ_1: 44;

          then ( Sum z) in M by A54, A65, A67, A66, A59;

          hence thesis by RLVECT_1: 45;

        end;

        hence thesis by CONVEX1:def 2;

      end;

    end;

    begin

    

     Lm13: for X be RealLinearSpace, f be Function of the carrier of X, ExtREAL , n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y be FinSequence of the carrier of X st ( len F) = n & (for x be VECTOR of X holds (f . x) <> -infty ) & (for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (F . i) = ((p . i) * (f . (y /. i)))) holds not -infty in ( rng F)

    proof

      let X be RealLinearSpace, f be Function of the carrier of X, ExtREAL , n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y be FinSequence of the carrier of X;

      assume that

       A1: ( len F) = n and

       A2: for x be VECTOR of X holds (f . x) <> -infty and

       A3: for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (F . i) = ((p . i) * (f . (y /. i)));

      for i be object st i in ( dom F) holds (F . i) <> -infty

      proof

        let i be object;

        assume

         A4: i in ( dom F);

        then

        reconsider i as Element of NAT ;

        

         A5: i in ( Seg n) by A1, A4, FINSEQ_1:def 3;

        then

         A6: (p . i) >= 0 by A3;

        

         A7: (F . i) = ((p . i) * (f . (y /. i))) by A3, A5;

        per cases ;

          suppose (p . i) = 0. ;

          hence thesis by A7;

        end;

          suppose (f . (y /. i)) <> +infty ;

          then

          reconsider w = (f . (y /. i)) as Element of REAL by A2, XXREAL_0: 14;

          (F . i) = ((p . i) * w) by A7, EXTREAL1: 1;

          hence thesis;

        end;

          suppose (p . i) <> 0. & (f . (y /. i)) = +infty ;

          hence thesis by A6, A7;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: CONVFUN1:8

    

     Th8: for X be RealLinearSpace, f be Function of the carrier of X, ExtREAL st (for x be VECTOR of X holds (f . x) <> -infty ) holds f is convex iff for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)

    proof

      let X be RealLinearSpace, f be Function of the carrier of X, ExtREAL ;

      assume

       A1: for x be VECTOR of X holds (f . x) <> -infty ;

      thus f is convex implies for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)

      proof

        assume

         A2: f is convex;

        let n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X;

        assume that

         A3: ( len p) = n and

         A4: ( len F) = n and ( len y) = n and

         A5: ( len z) = n and

         A6: ( Sum p) = 1 and

         A7: for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)));

        for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (F . i) = ((p . i) * (f . (y /. i))) by A7;

        then

         A8: not -infty in ( rng F) by A1, A4, Lm13;

        per cases ;

          suppose

           A9: for i be Element of NAT st i in ( Seg n) holds (f . (y /. i)) <> +infty ;

          defpred P[ set, set] means $2 = [(y /. $1), (f . (y /. $1))];

          reconsider V = ( Prod_of_RLS (X, RLS_Real )) as RealLinearSpace;

          

           A10: for i be Element of NAT st i in ( Seg n) holds (f . (y /. i)) in REAL

          proof

            let i be Element of NAT ;

            assume i in ( Seg n);

            then (f . (y /. i)) <> +infty by A9;

            hence thesis by A1, XXREAL_0: 14;

          end;

          

           A11: for i be Nat st i in ( Seg n) holds ex v be Element of V st P[i, v]

          proof

            let i be Nat;

            assume i in ( Seg n);

            then

            reconsider w = (f . (y /. i)) as Element of REAL by A10;

            set v = [(y /. i), w];

            reconsider v as Element of V;

            take v;

            thus thesis;

          end;

          consider g be FinSequence of the carrier of V such that

           A12: ( dom g) = ( Seg n) and

           A13: for i be Nat st i in ( Seg n) holds P[i, (g /. i)] from RECDEF_1:sch 17( A11);

          

           A14: ( len g) = n by A12, FINSEQ_1:def 3;

          defpred P[ set, set] means $2 = (F . $1);

          

           A15: for i be Nat st i in ( Seg n) holds ex w be Element of RLS_Real st P[i, w]

          proof

            let i be Nat;

            assume

             A16: i in ( Seg n);

            then

            reconsider a = (f . (y /. i)) as Element of REAL by A10;

            (F . i) = ((p . i) * (f . (y /. i))) by A7, A16;

            then (F . i) = ((p . i) * a) by EXTREAL1: 1;

            then

            reconsider w = (F . i) as Element of RLS_Real by XREAL_0:def 1;

            take w;

            thus thesis;

          end;

          consider F1 be FinSequence of the carrier of RLS_Real such that

           A17: ( dom F1) = ( Seg n) and

           A18: for i be Nat st i in ( Seg n) holds P[i, (F1 /. i)] from RECDEF_1:sch 17( A15);

          

           A19: ( len F1) = n by A17, FINSEQ_1:def 3;

          reconsider M = ( epigraph f) as Subset of V;

          deffunc f( Nat) = ((p . $1) * (g /. $1));

          consider G be FinSequence of the carrier of V such that

           A20: ( len G) = n and

           A21: for i be Nat st i in ( dom G) holds (G . i) = f(i) from FINSEQ_2:sch 1;

          

           A22: ( dom G) = ( Seg n) by A20, FINSEQ_1:def 3;

          

           A23: for i be Nat st i in ( Seg n) holds (p . i) > 0 & (G . i) = ((p . i) * (g /. i)) & (g /. i) in M

          proof

            let i be Nat;

            assume

             A24: i in ( Seg n);

            hence (p . i) > 0 by A7;

            thus (G . i) = ((p . i) * (g /. i)) by A21, A22, A24;

            reconsider w = (f . (y /. i)) as Element of REAL by A10, A24;

             [(y /. i), w] in { [x, a] where x be Element of X, a be Element of REAL : (f . x) <= a };

            hence thesis by A13, A24;

          end;

          M is convex by A2;

          then

           A25: ( Sum G) in M by A3, A6, A14, A20, A23, Th7;

          

           A26: for i be Element of NAT st i in ( Seg n) holds (F1 . i) = (F . i)

          proof

            let i be Element of NAT ;

            assume

             A27: i in ( Seg n);

            then (F1 /. i) = (F1 . i) by A17, PARTFUN1:def 6;

            hence thesis by A18, A27;

          end;

          for i be Nat st i in ( Seg n) holds (G . i) = [(z . i), (F1 . i)]

          proof

            let i be Nat;

            assume

             A28: i in ( Seg n);

            then

            reconsider a = (f . (y /. i)) as Element of REAL by A10;

            (g /. i) = [(y /. i), a] by A13, A28;

            then ((p . i) * (g /. i)) = [((p . i) * (y /. i)), ((p . i) * a)] by Lm1;

            then (G . i) = [((p . i) * (y /. i)), ((p . i) * a)] by A21, A22, A28;

            then

             A29: (G . i) = [(z . i), ((p . i) * a)] by A7, A28;

            (F . i) = ((p . i) * (f . (y /. i))) by A7, A28;

            then (F . i) = ((p . i) * a) by EXTREAL1: 1;

            hence thesis by A26, A28, A29;

          end;

          then ( Sum G) = [( Sum z), ( Sum F1)] by A5, A20, A19, Th3;

          then [( Sum z), ( Sum F)] in M by A4, A25, A26, A19, Lm8;

          then

          consider x be Element of X, w be Element of REAL such that

           A30: [( Sum z), ( Sum F)] = [x, w] and

           A31: (f . x) <= w;

          x = ( Sum z) by A30, XTUPLE_0: 1;

          hence thesis by A30, A31, XTUPLE_0: 1;

        end;

          suppose ex i be Element of NAT st i in ( Seg n) & (f . (y /. i)) = +infty ;

          then

          consider i be Element of NAT such that

           A32: i in ( Seg n) and

           A33: (f . (y /. i)) = +infty ;

          

           A34: (F . i) = ((p . i) * (f . (y /. i))) by A7, A32;

          

           A35: i in ( dom F) by A4, A32, FINSEQ_1:def 3;

          (p . i) > 0 by A7, A32;

          then (F . i) = +infty by A33, A34, XXREAL_3:def 5;

          then ( Sum F) = +infty by A8, A35, Lm6, FUNCT_1: 3;

          hence thesis by XXREAL_0: 4;

        end;

      end;

      thus (for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)) implies f is convex

      proof

        assume

         A36: for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F);

        for x1,x2 be VECTOR of X, q be Real st 0 < q & q < 1 holds (f . ((q * x1) + ((1 - q) * x2))) <= ((q * (f . x1)) + ((1 - q) * (f . x2)))

        proof

          set n = 2;

          let x1,x2 be VECTOR of X, q be Real;

          assume that

           A37: 0 < q and

           A38: q < 1;

          reconsider q1 = (q * (f . x1)), q2 = ((1 - q) * (f . x2)) as R_eal by XXREAL_0:def 1;

          reconsider F = <*q1, q2*> as FinSequence of ExtREAL ;

          reconsider z = <*(q * x1), ((1 - q) * x2)*> as FinSequence of the carrier of X;

          reconsider y = <*x1, x2*> as FinSequence of the carrier of X;

          reconsider q as Element of REAL by XREAL_0:def 1;

          reconsider q1 = (1 - q) as Element of REAL by XREAL_0:def 1;

          reconsider p = <*q, q1*> as FinSequence of REAL ;

          

           A39: for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))

          proof

            let i be Element of NAT ;

            assume

             A40: i in ( Seg n);

            per cases by A40, FINSEQ_1: 2, TARSKI:def 2;

              suppose

               A41: i = 1;

              then

               A42: (y /. i) = x1 by FINSEQ_4: 17;

              (p . i) = q by A41, FINSEQ_1: 44;

              hence thesis by A37, A41, A42, FINSEQ_1: 44;

            end;

              suppose

               A43: i = 2;

              then

               A44: (y /. i) = x2 by FINSEQ_4: 17;

              (p . i) = (1 - q) by A43, FINSEQ_1: 44;

              hence thesis by A38, A43, A44, FINSEQ_1: 44, XREAL_1: 50;

            end;

          end;

          

           A45: ( len p) = n by FINSEQ_1: 44;

          

           A46: ( Sum p) = (q + (1 - q)) by RVSUM_1: 77

          .= 1;

          

           A47: ( len z) = n by FINSEQ_1: 44;

          

           A48: ( Sum z) = ((q * x1) + ((1 - q) * x2)) by RLVECT_1: 45;

          

           A49: ( len y) = n by FINSEQ_1: 44;

          

           A50: ( len F) = n by FINSEQ_1: 44;

          ( Sum F) = ((q * (f . x1)) + ((1 - q) * (f . x2))) by EXTREAL1: 9;

          hence thesis by A36, A45, A50, A49, A47, A46, A39, A48;

        end;

        hence thesis by A1, Th4;

      end;

    end;

    

     Lm14: for F be FinSequence of REAL holds ex s be Permutation of ( dom F), n be Element of NAT st for i be Element of NAT st i in ( dom F) holds i in ( Seg n) iff (F . (s . i)) <> 0

    proof

      deffunc f( Nat) = $1;

      let F be FinSequence of REAL ;

      defpred P[ Nat] means (F . $1) <> 0 ;

      defpred R[ Nat] means (F . $1) = 0 ;

      set A = { f(i) where i be Element of NAT : f(i) in ( dom F) & P[i] };

      set B = { f(i) where i be Element of NAT : f(i) in ( dom F) & R[i] };

      set N = ( len F);

      

       A1: A c= ( dom F) from FRAENKEL:sch 17;

      then

       A2: A c= ( Seg N) by FINSEQ_1:def 3;

      reconsider A as finite set by A1;

      

       A3: ( rng ( Sgm A)) = A by A2, FINSEQ_1:def 13;

      

       A4: B c= ( dom F) from FRAENKEL:sch 17;

      then

       A5: B c= ( Seg N) by FINSEQ_1:def 3;

      reconsider B as finite set by A4;

      

       A6: ( rng ( Sgm B)) = B by A5, FINSEQ_1:def 13;

      for x be object holds not x in (A /\ B)

      proof

        let x be object;

        assume

         A7: x in (A /\ B);

        then x in B by XBOOLE_0:def 4;

        then

         A8: ex i2 be Element of NAT st x = i2 & i2 in ( dom F) & (F . i2) = 0 ;

        x in A by A7, XBOOLE_0:def 4;

        then ex i1 be Element of NAT st x = i1 & i1 in ( dom F) & (F . i1) <> 0 ;

        hence contradiction by A8;

      end;

      then (A /\ B) = {} by XBOOLE_0:def 1;

      then

       A9: A misses B by XBOOLE_0:def 7;

      set s = (( Sgm A) ^ ( Sgm B));

      

       A10: ( Sgm B) is one-to-one by A5, FINSEQ_3: 92;

      ( Sgm A) is one-to-one by A2, FINSEQ_3: 92;

      then

       A11: s is one-to-one by A3, A6, A9, A10, FINSEQ_3: 91;

      set n = ( len ( Sgm A));

      

       A12: ( len ( Sgm A)) = ( card A) by A2, FINSEQ_3: 39;

      for x be object holds x in ( dom F) iff (x in A or x in B)

      proof

        let x be object;

        thus x in ( dom F) implies (x in A or x in B)

        proof

          assume

           A13: x in ( dom F);

          then

          reconsider x as Element of NAT ;

          per cases ;

            suppose (F . x) <> 0 ;

            hence thesis by A13;

          end;

            suppose (F . x) = 0 ;

            hence thesis by A13;

          end;

        end;

        thus thesis by A1, A4;

      end;

      then

       A14: (A \/ B) = ( dom F) by XBOOLE_0:def 3;

      then

       A15: ( rng s) = ( dom F) by A3, A6, FINSEQ_1: 31;

      ( len ( Sgm B)) = ( card B) by A5, FINSEQ_3: 39;

      

      then ( len s) = (( card A) + ( card B)) by A12, FINSEQ_1: 22

      .= ( card (A \/ B)) by A9, CARD_2: 40

      .= ( card ( Seg N)) by A14, FINSEQ_1:def 3;

      then

       A16: ( len s) = N by FINSEQ_1: 57;

      then

       A17: ( dom s) = ( Seg N) by FINSEQ_1:def 3;

      

       A18: for x be Element of NAT st x in ( dom F) & not x in ( Seg n) holds ex k be Element of NAT st x = (k + n) & k in ( dom ( Sgm B)) & (s . x) = (( Sgm B) . k)

      proof

        let x be Element of NAT ;

        assume that

         A19: x in ( dom F) and

         A20: not x in ( Seg n);

        

         A21: x in ( Seg N) by A19, FINSEQ_1:def 3;

         not (1 <= x & x <= n) by A20, FINSEQ_1: 1;

        then (n + 1) <= x by A21, FINSEQ_1: 1, INT_1: 7;

        then

         A22: ((n + 1) - n) <= (x - n) by XREAL_1: 9;

        reconsider k = (x - n) as Element of NAT by A22, INT_1: 3;

        take k;

        ( len s) = (n + ( len ( Sgm B))) by FINSEQ_1: 22;

        then

         A23: (N - n) = ( len ( Sgm B)) by A16;

        x <= N by A21, FINSEQ_1: 1;

        then k <= ( len ( Sgm B)) by A23, XREAL_1: 9;

        then k in ( Seg ( len ( Sgm B))) by A22, FINSEQ_1: 1;

        then k in ( Seg ( card B)) by A5, FINSEQ_3: 39;

        then

         A24: k in ( dom ( Sgm B)) by A5, FINSEQ_3: 40;

        x = (k + n);

        hence thesis by A24, FINSEQ_1:def 7;

      end;

      ( dom F) = ( Seg N) by FINSEQ_1:def 3;

      then

      reconsider s as Function of ( dom F), ( dom F) by A15, A17, FUNCT_2: 1;

      s is onto by A15, FUNCT_2:def 3;

      then

      reconsider s as Permutation of ( dom F) by A11;

      take s, n;

      let i be Element of NAT ;

      assume

       A25: i in ( dom F);

      thus i in ( Seg n) implies (F . (s . i)) <> 0

      proof

        assume i in ( Seg n);

        then

         A26: i in ( dom ( Sgm A)) by FINSEQ_1:def 3;

        then (s . i) = (( Sgm A) . i) by FINSEQ_1:def 7;

        then (s . i) in A by A3, A26, FUNCT_1: 3;

        then ex j be Element of NAT st (s . i) = j & j in ( dom F) & (F . j) <> 0 ;

        hence thesis;

      end;

      thus (F . (s . i)) <> 0 implies i in ( Seg n)

      proof

        assume

         A27: (F . (s . i)) <> 0 ;

        assume not i in ( Seg n);

        then ex k be Element of NAT st i = (k + n) & k in ( dom ( Sgm B)) & (s . i) = (( Sgm B) . k) by A18, A25;

        then (s . i) in ( rng ( Sgm B)) by FUNCT_1: 3;

        then ex j be Element of NAT st (s . i) = j & j in ( dom F) & (F . j) = 0 by A6;

        hence thesis by A27;

      end;

    end;

    theorem :: CONVFUN1:9

    for X be RealLinearSpace, f be Function of the carrier of X, ExtREAL st (for x be VECTOR of X holds (f . x) <> -infty ) holds f is convex iff for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)

    proof

      let X be RealLinearSpace, f be Function of the carrier of X, ExtREAL ;

      assume

       A1: for x be VECTOR of X holds (f . x) <> -infty ;

      thus f is convex implies for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)

      proof

        assume

         A2: f is convex;

        let n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X;

        assume that

         A3: ( len p) = n and

         A4: ( len F) = n and

         A5: ( len y) = n and

         A6: ( len z) = n and

         A7: ( Sum p) = 1 and

         A8: for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)));

        consider s be Permutation of ( dom p), k be Element of NAT such that

         A9: for i be Element of NAT st i in ( dom p) holds i in ( Seg k) iff (p . (s . i)) <> 0 by Lm14;

        

         A10: ( dom p) = ( Seg n) by A3, FINSEQ_1:def 3;

        then

        reconsider s1 = s as FinSequence of ( Seg n) by FINSEQ_2: 25;

        

         A11: ( dom F) = ( Seg n) by A4, FINSEQ_1:def 3;

        then

         A12: F is Function of ( Seg n), ExtREAL by FINSEQ_2: 26;

        then

        reconsider F9 = (F * s1) as FinSequence of ExtREAL by FINSEQ_2: 32;

        

         A13: F9 = ((F9 | k) ^ (F9 /^ k)) by RFINSEQ: 8;

        

         A14: for i be Element of NAT st 1 <= i & i <= (n - k) holds (i + k) in ( Seg n) & (p . (s . (i + k))) = 0

        proof

          let i be Element of NAT ;

          assume that

           A15: 1 <= i and

           A16: i <= (n - k);

          i <= (i + k) by INT_1: 6;

          then

           A17: 1 <= (i + k) by A15, XXREAL_0: 2;

          ( 0 + k) < (i + k) by A15, XREAL_1: 6;

          then

           A18: not (i + k) in ( Seg k) by FINSEQ_1: 1;

          

           A19: (i + k) <= ((n - k) + k) by A16, XREAL_1: 6;

          then (i + k) in ( dom p) by A10, A17, FINSEQ_1: 1;

          hence thesis by A9, A19, A17, A18, FINSEQ_1: 1;

        end;

        

         A20: ( dom z) = ( Seg n) by A6, FINSEQ_1:def 3;

        then

         A21: z is Function of ( Seg n), the carrier of X by FINSEQ_2: 26;

        then

        reconsider z9 = (z * s1) as FinSequence of the carrier of X by FINSEQ_2: 32;

        ( dom s) = ( Seg n) by A10, FUNCT_2:def 1;

        then

         A22: ( len s1) = n by FINSEQ_1:def 3;

        then

         A23: ( len z9) = n by A21, FINSEQ_2: 33;

        

         A24: ( Sum (z9 /^ k)) = ( 0. X)

        proof

          per cases ;

            suppose k >= n;

            then (z9 /^ k) = ( <*> the carrier of X) by A23, FINSEQ_5: 32;

            hence thesis by RLVECT_1: 43;

          end;

            suppose

             A25: k < n;

            for w be object st w in ( rng (z9 /^ k)) holds w in {( 0. X)}

            proof

              reconsider k1 = (n - k) as Element of NAT by A25, INT_1: 5;

              let w be object;

              assume w in ( rng (z9 /^ k));

              then

              consider i be object such that

               A26: i in ( dom (z9 /^ k)) and

               A27: ((z9 /^ k) . i) = w by FUNCT_1:def 3;

              reconsider i as Element of NAT by A26;

              ( len (z9 /^ k)) = k1 by A23, A25, RFINSEQ:def 1;

              then

               A28: i in ( Seg k1) by A26, FINSEQ_1:def 3;

              then

               A29: 1 <= i by FINSEQ_1: 1;

              

               A30: i <= (n - k) by A28, FINSEQ_1: 1;

              then (s . (i + k)) in ( Seg n) by A10, A14, A29, FUNCT_2: 5;

              then (z . (s . (i + k))) = ((p . (s . (i + k))) * (y /. (s . (i + k)))) by A8;

              then

               A31: (z . (s . (i + k))) = ( 0. X) by A14, A29, A30, RLVECT_1: 10;

              (i + k) in ( Seg n) by A14, A29, A30;

              then (i + k) in ( dom z9) by A23, FINSEQ_1:def 3;

              then (z9 . (i + k)) = ( 0. X) by A31, FUNCT_1: 12;

              then w = ( 0. X) by A23, A25, A26, A27, RFINSEQ:def 1;

              hence thesis by TARSKI:def 1;

            end;

            then ( rng (z9 /^ k)) c= {( 0. X)} by TARSKI:def 3;

            hence thesis by Lm11;

          end;

        end;

        

         A32: p is Function of ( Seg n), REAL by A10, FINSEQ_2: 26;

        then

        reconsider p9 = (p * s1) as FinSequence of REAL by FINSEQ_2: 32;

        set k9 = ( min (k,n));

        reconsider k9 as Element of NAT ;

        p9 = ((p9 | k) ^ (p9 /^ k)) by RFINSEQ: 8;

        then

         A33: ( Sum p9) = (( Sum (p9 | k)) + ( Sum (p9 /^ k))) by RVSUM_1: 75;

        

         A34: ( len F9) = n by A22, A12, FINSEQ_2: 33;

        

         A35: ( Sum (F9 /^ k)) = 0.

        proof

          per cases ;

            suppose k >= n;

            hence thesis by A34, EXTREAL1: 7, FINSEQ_5: 32;

          end;

            suppose

             A36: k < n;

            for w be object st w in ( rng (F9 /^ k)) holds w in { 0. }

            proof

              reconsider k1 = (n - k) as Element of NAT by A36, INT_1: 5;

              let w be object;

              assume w in ( rng (F9 /^ k));

              then

              consider i be object such that

               A37: i in ( dom (F9 /^ k)) and

               A38: ((F9 /^ k) . i) = w by FUNCT_1:def 3;

              reconsider i as Element of NAT by A37;

              ( len (F9 /^ k)) = k1 by A34, A36, RFINSEQ:def 1;

              then

               A39: i in ( Seg k1) by A37, FINSEQ_1:def 3;

              then

               A40: 1 <= i by FINSEQ_1: 1;

              

               A41: i <= (n - k) by A39, FINSEQ_1: 1;

              then

               A42: (p . (s . (i + k))) = 0 by A14, A40;

              (i + k) in ( Seg n) by A14, A40, A41;

              then

               A43: (i + k) in ( dom F9) by A34, FINSEQ_1:def 3;

              (s . (i + k)) in ( Seg n) by A10, A14, A40, A41, FUNCT_2: 5;

              then (F . (s . (i + k))) = ( 0 * (f . (y /. (s . (i + k))))) by A8, A42;

              then (F9 . (i + k)) = 0. by A43, FUNCT_1: 12;

              then w = 0. by A34, A36, A37, A38, RFINSEQ:def 1;

              hence thesis by TARSKI:def 1;

            end;

            then ( rng (F9 /^ k)) c= { 0. } by TARSKI:def 3;

            hence thesis by Lm9;

          end;

        end;

        

         A44: (F9 | k) = (F9 | ( Seg k)) by FINSEQ_1:def 15;

        then

         A45: ( len (F9 | k)) = k9 by A34, FINSEQ_2: 21;

        for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (F . i) = ((p . i) * (f . (y /. i))) by A8;

        then

         A46: not -infty in ( rng F) by A1, A4, Lm13;

        then not -infty in ( rng F9) by FUNCT_1: 14;

        then

         A47: not -infty in (( rng (F9 | k)) \/ ( rng (F9 /^ k))) by A13, FINSEQ_1: 31;

        then

         A48: not -infty in ( rng (F9 /^ k)) by XBOOLE_0:def 3;

        

         A49: (z9 | k) = (z9 | ( Seg k)) by FINSEQ_1:def 15;

        then

         A50: ( len (z9 | k)) = k9 by A23, FINSEQ_2: 21;

        

         A51: ( len p9) = n by A22, A32, FINSEQ_2: 33;

        

         A52: ( Sum (p9 /^ k)) = 0

        proof

          per cases ;

            suppose k >= n;

            hence thesis by A51, FINSEQ_5: 32, RVSUM_1: 72;

          end;

            suppose

             A53: k < n;

            for w be object st w in ( rng (p9 /^ k)) holds w in { 0 }

            proof

              reconsider k1 = (n - k) as Element of NAT by A53, INT_1: 5;

              let w be object;

              assume w in ( rng (p9 /^ k));

              then

              consider i be object such that

               A54: i in ( dom (p9 /^ k)) and

               A55: ((p9 /^ k) . i) = w by FUNCT_1:def 3;

              reconsider i as Element of NAT by A54;

              ( len (p9 /^ k)) = k1 by A51, A53, RFINSEQ:def 1;

              then

               A56: i in ( Seg k1) by A54, FINSEQ_1:def 3;

              then

               A57: 1 <= i by FINSEQ_1: 1;

              

               A58: i <= (n - k) by A56, FINSEQ_1: 1;

              then (i + k) in ( Seg n) by A14, A57;

              then

               A59: (i + k) in ( dom p9) by A51, FINSEQ_1:def 3;

              (p . (s . (i + k))) = 0 by A14, A57, A58;

              then (p9 . (i + k)) = 0 by A59, FUNCT_1: 12;

              then w = 0 by A51, A53, A54, A55, RFINSEQ:def 1;

              hence thesis by TARSKI:def 1;

            end;

            then ( rng (p9 /^ k)) c= { 0 } by TARSKI:def 3;

            hence thesis by Lm10;

          end;

        end;

        

         A60: (p9 | k) = (p9 | ( Seg k)) by FINSEQ_1:def 15;

        then

         A61: ( len (p9 | k)) = k9 by A51, FINSEQ_2: 21;

         not -infty in ( rng (F9 | k)) by A47, XBOOLE_0:def 3;

        then

         A62: ( Sum F9) = (( Sum (F9 | k)) + ( Sum (F9 /^ k))) by A13, A48, EXTREAL1: 10;

        ( Sum F9) = ( Sum F) by A10, A11, A46, EXTREAL1: 11;

        then

         A63: ( Sum (F9 | k)) = ( Sum F) by A62, A35, XXREAL_3: 4;

        z9 = ((z9 | k) ^ (z9 /^ k)) by RFINSEQ: 8;

        then

         A64: ( Sum z9) = (( Sum (z9 | k)) + ( Sum (z9 /^ k))) by RLVECT_1: 41;

        ( Sum z9) = ( Sum z) by A10, A20, RLVECT_2: 7;

        then

         A65: ( Sum (z9 | k)) = ( Sum z) by A64, A24;

        

         A66: ( dom y) = ( Seg n) by A5, FINSEQ_1:def 3;

        then

         A67: y is Function of ( Seg n), the carrier of X by FINSEQ_2: 26;

        then

        reconsider y9 = (y * s1) as FinSequence of the carrier of X by FINSEQ_2: 32;

        

         A68: (y9 | k) = (y9 | ( Seg k)) by FINSEQ_1:def 15;

        ( len y9) = n by A22, A67, FINSEQ_2: 33;

        then

         A69: ( len (y9 | k)) = k9 by A68, FINSEQ_2: 21;

        

         A70: (p9,p) are_fiberwise_equipotent by RFINSEQ: 4;

        then (p9 | k) <> {} by A7, A33, A52, RFINSEQ: 9, RVSUM_1: 72;

        then

        reconsider k9 as non zero Element of NAT by A61;

        

         A71: for i be Element of NAT st i in ( Seg k9) holds ((p9 | k) . i) > 0 & ((z9 | k) . i) = (((p9 | k) . i) * ((y9 | k) /. i)) & ((F9 | k) . i) = (((p9 | k) . i) * (f . ((y9 | k) /. i)))

        proof

          let i be Element of NAT ;

          assume

           A72: i in ( Seg k9);

          then

           A73: i in ( dom (p9 | k)) by A61, FINSEQ_1:def 3;

          then

           A74: ((p9 | k) /. i) = (p9 /. i) by FINSEQ_4: 70;

          ( dom (p9 | k)) = (( dom p9) /\ ( Seg k)) by A60, RELAT_1: 61;

          then

           A75: i in ( dom p9) by A73, XBOOLE_0:def 4;

          then

           A76: (p9 . i) = (p . (s . i)) by FUNCT_1: 12;

          (p9 /. i) = (p9 . i) by A75, PARTFUN1:def 6;

          then

           A77: ((p9 | k) . i) = (p . (s . i)) by A73, A74, A76, PARTFUN1:def 6;

          

           A78: i in ( dom (y9 | k)) by A69, A72, FINSEQ_1:def 3;

          then

           A79: ((y9 | k) /. i) = (y9 /. i) by FINSEQ_4: 70;

          ( dom (y9 | k)) = (( dom y9) /\ ( Seg k)) by A68, RELAT_1: 61;

          then

           A80: i in ( dom y9) by A78, XBOOLE_0:def 4;

          then

           A81: (y9 . i) = (y . (s . i)) by FUNCT_1: 12;

          

           A82: i in ( dom (F9 | k)) by A45, A72, FINSEQ_1:def 3;

          then

           A83: ((F9 | k) /. i) = (F9 /. i) by FINSEQ_4: 70;

          ( dom (F9 | k)) = (( dom F9) /\ ( Seg k)) by A44, RELAT_1: 61;

          then

           A84: i in ( dom F9) by A82, XBOOLE_0:def 4;

          then

           A85: (F9 . i) = (F . (s . i)) by FUNCT_1: 12;

          (F9 /. i) = (F9 . i) by A84, PARTFUN1:def 6;

          then

           A86: ((F9 | k) . i) = (F . (s . i)) by A82, A83, A85, PARTFUN1:def 6;

          

           A87: i in ( dom (z9 | k)) by A50, A72, FINSEQ_1:def 3;

          then

           A88: ((z9 | k) /. i) = (z9 /. i) by FINSEQ_4: 70;

          ( dom (z9 | k)) = (( dom z9) /\ ( Seg k)) by A49, RELAT_1: 61;

          then

           A89: i in ( dom z9) by A87, XBOOLE_0:def 4;

          then

           A90: (z9 . i) = (z . (s . i)) by FUNCT_1: 12;

          (z9 /. i) = (z9 . i) by A89, PARTFUN1:def 6;

          then

           A91: ((z9 | k) . i) = (z . (s . i)) by A87, A88, A90, PARTFUN1:def 6;

          

           A92: i in ( Seg n) by A51, A75, FINSEQ_1:def 3;

          k9 <= k by XXREAL_0: 17;

          then ( Seg k9) c= ( Seg k) by FINSEQ_1: 5;

          then

           A93: (p . (s . i)) <> 0 by A9, A10, A72, A92;

          (y9 /. i) = (y9 . i) by A80, PARTFUN1:def 6;

          then

           A94: ((y9 | k) /. i) = (y /. (s . i)) by A10, A66, A79, A81, A92, FUNCT_2: 5, PARTFUN1:def 6;

          (s . i) in ( Seg n) by A10, A92, FUNCT_2: 5;

          hence thesis by A8, A77, A94, A91, A86, A93;

        end;

        ( Sum (p9 | k)) = 1 by A7, A33, A52, A70, RFINSEQ: 9;

        hence thesis by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8;

      end;

      thus (for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)) implies f is convex

      proof

        assume

         A95: for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F);

        for n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X st ( len p) = n & ( len F) = n & ( len y) = n & ( len z) = n & ( Sum p) = 1 & (for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)))) holds (f . ( Sum z)) <= ( Sum F)

        proof

          let n be non zero Element of NAT , p be FinSequence of REAL , F be FinSequence of ExtREAL , y,z be FinSequence of the carrier of X;

          assume that

           A96: ( len p) = n and

           A97: ( len F) = n and

           A98: ( len y) = n and

           A99: ( len z) = n and

           A100: ( Sum p) = 1 and

           A101: for i be Element of NAT st i in ( Seg n) holds (p . i) > 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i)));

          for i be Element of NAT st i in ( Seg n) holds (p . i) >= 0 & (z . i) = ((p . i) * (y /. i)) & (F . i) = ((p . i) * (f . (y /. i))) by A101;

          hence thesis by A95, A96, A97, A98, A99, A100;

        end;

        hence thesis by A1, Th8;

      end;

    end;