:: CONVFUN1 semantic presentation begin definition let X, Y be non empty RLSStruct ; func Add_in_Prod_of_RLS (X,Y) -> BinOp of [: the carrier of X, the carrier of Y:] means :Def1: :: CONVFUN1:def 1 for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being 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 ex b1 being BinOp of [: the carrier of X, the carrier of Y:] st for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] proof defpred S1[ set , set , set ] means for x1, x2 being VECTOR of X for y1, y2 being 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 being Element of [: the carrier of X, the carrier of Y:] ex z3 being Element of [: the carrier of X, the carrier of Y:] st S1[z1,z2,z3] proof let z1, z2 be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ex z3 being Element of [: the carrier of X, the carrier of Y:] st S1[z1,z2,z3] consider x19, y19 being set 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 being set 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 = y19, y29 = y29 as VECTOR of Y by A3, A6; reconsider x19 = x19, x29 = 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 [: the carrier of X, the carrier of Y:] ; take z3 ; ::_thesis: S1[z1,z2,z3] let x1, x2 be VECTOR of X; ::_thesis: for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] let y1, y2 be VECTOR of Y; ::_thesis: ( z1 = [x1,y1] & z2 = [x2,y2] implies z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) assume that A8: z1 = [x1,y1] and A9: z2 = [x2,y2] ; ::_thesis: z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,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 z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A7, A9, A10, A11, XTUPLE_0:1; ::_thesis: verum end; thus ex o being BinOp of [: the carrier of X, the carrier of Y:] st for a, b being Element of [: the carrier of X, the carrier of Y:] holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being BinOp of [: the carrier of X, the carrier of Y:] st ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds b1 = b2 proof let A1, A2 be BinOp of [: the carrier of X, the carrier of Y:]; ::_thesis: ( ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being 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])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being 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])] ) implies A1 = A2 ) assume A12: for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being 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])] ; ::_thesis: ( ex z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex x1, x2 being VECTOR of X ex y1, y2 being VECTOR of Y st ( z1 = [x1,y1] & z2 = [x2,y2] & not A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) or A1 = A2 ) assume A13: for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being 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])] ; ::_thesis: A1 = A2 for z1, z2 being 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:]; ::_thesis: A1 . (z1,z2) = A2 . (z1,z2) consider x1, y1 being set 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 being set 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 = y1, y2 = y2 as VECTOR of Y by A15, A18; reconsider x1 = x1, x2 = 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 A1 . (z1,z2) = A2 . (z1,z2) by A13, A16, A19; ::_thesis: verum end; hence A1 = A2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def_1_:_ for X, Y being non empty RLSStruct for b3 being BinOp of [: the carrier of X, the carrier of Y:] holds ( b3 = Add_in_Prod_of_RLS (X,Y) iff for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b3 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ); definition let X, Y be non empty RLSStruct ; 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: :: CONVFUN1:def 2 for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds it . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]; existence ex b1 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] proof defpred S1[ set , set , set ] means for x being VECTOR of X for y being VECTOR of Y st $2 = [x,y] holds $3 = [( the Mult of X . [$1,x]),( the Mult of Y . [$1,y])]; A1: for a1 being Element of REAL for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w] proof let a1 be Element of REAL ; ::_thesis: for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w] let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w] consider x9, y9 being set 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 = y9 as VECTOR of Y by A3; reconsider x9 = 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 ; ::_thesis: S1[a1,z,w] for x being VECTOR of X for y being 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; ::_thesis: for y being VECTOR of Y st z = [x,y] holds w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] let y be VECTOR of Y; ::_thesis: ( z = [x,y] implies w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] ) assume A5: z = [x,y] ; ::_thesis: w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] then x = x9 by A4, XTUPLE_0:1; hence w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] by A4, A5, XTUPLE_0:1; ::_thesis: verum end; hence S1[a1,z,w] ; ::_thesis: verum end; consider g being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] such that A6: for a being Element of REAL for z being Element of [: the carrier of X, the carrier of Y:] holds S1[a,z,g . (a,z)] from BINOP_1:sch_3(A1); take g ; ::_thesis: for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] let a be Real; ::_thesis: for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] thus for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A6; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds b1 = b2 proof let g1, g2 be Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]; ::_thesis: ( ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) implies g1 = g2 ) assume A7: for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; ::_thesis: ( ex a being Real ex z being Element of [: the carrier of X, the carrier of Y:] ex x being VECTOR of X ex y being VECTOR of Y st ( z = [x,y] & not g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) or g1 = g2 ) assume A8: for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; ::_thesis: g1 = g2 for a being Real for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z) proof let a be Real; ::_thesis: for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z) let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: g1 . (a,z) = g2 . (a,z) consider x, y being set such that A9: x in the carrier of X and A10: y in the carrier of Y and A11: z = [x,y] by ZFMISC_1:def_2; reconsider y = y as VECTOR of Y by A10; reconsider x = x as VECTOR of X by A9; g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A7, A11; hence g1 . (a,z) = g2 . (a,z) by A8, A11; ::_thesis: verum end; hence g1 = g2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def_2_:_ for X, Y being non empty RLSStruct for b3 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds ( b3 = Mult_in_Prod_of_RLS (X,Y) iff for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b3 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ); definition let X, Y be non empty RLSStruct ; func Prod_of_RLS (X,Y) -> RLSStruct equals :: CONVFUN1:def 3 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 coherence 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)) #) is RLSStruct ; ; end; :: deftheorem defines Prod_of_RLS CONVFUN1:def_3_:_ for X, Y being non empty RLSStruct holds Prod_of_RLS (X,Y) = 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)) #); registration let X, Y be non empty RLSStruct ; cluster Prod_of_RLS (X,Y) -> non empty ; coherence not Prod_of_RLS (X,Y) is empty ; end; theorem :: CONVFUN1:1 for X, Y being non empty RLSStruct for x being VECTOR of X for y being VECTOR of Y for u being VECTOR of (Prod_of_RLS (X,Y)) for p being Real st u = [x,y] holds p * u = [(p * x),(p * y)] by Def2; theorem Th2: :: CONVFUN1:2 for X, Y being non empty RLSStruct for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y for u1, u2 being 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 non empty Abelian RLSStruct ; cluster Prod_of_RLS (X,Y) -> Abelian ; coherence Prod_of_RLS (X,Y) is Abelian proof for u1, u2 being Element of (Prod_of_RLS (X,Y)) holds u1 + u2 = u2 + u1 proof let u1, u2 be Element of (Prod_of_RLS (X,Y)); ::_thesis: u1 + u2 = u2 + u1 consider x1, y1 being set 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 = y1 as VECTOR of Y by A2; reconsider x1 = x1 as VECTOR of X by A1; consider x2, y2 being set 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 = y2 as VECTOR of Y by A5; reconsider x2 = x2 as VECTOR of X by A4; u1 + u2 = [(x2 + x1),(y2 + y1)] by A3, A6, Th2; hence u1 + u2 = u2 + u1 by A3, A6, Def1; ::_thesis: verum end; hence Prod_of_RLS (X,Y) is Abelian by RLVECT_1:def_2; ::_thesis: verum end; end; registration let X, Y be non empty add-associative RLSStruct ; cluster Prod_of_RLS (X,Y) -> add-associative ; coherence Prod_of_RLS (X,Y) is add-associative proof for u1, u2, u3 being 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)); ::_thesis: (u1 + u2) + u3 = u1 + (u2 + u3) consider x1, y1 being set 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 = y1 as VECTOR of Y by A2; consider x3, y3 being set 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 = y3 as VECTOR of Y by A5; reconsider x3 = x3 as VECTOR of X by A4; reconsider x1 = x1 as VECTOR of X by A1; consider x2, y2 being set 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 = y2 as VECTOR of Y by A8; reconsider x2 = 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 (u1 + u2) + u3 = u1 + (u2 + u3) by A10, A11, RLVECT_1:def_3; ::_thesis: verum end; hence Prod_of_RLS (X,Y) is add-associative by RLVECT_1:def_3; ::_thesis: verum end; end; registration let X, Y be non empty right_zeroed RLSStruct ; cluster Prod_of_RLS (X,Y) -> right_zeroed ; coherence Prod_of_RLS (X,Y) is right_zeroed proof for u being 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)); ::_thesis: u + (0. (Prod_of_RLS (X,Y))) = u consider x, y being set 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 = y as VECTOR of Y by A2; reconsider x = 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 u + (0. (Prod_of_RLS (X,Y))) = u by A3, A4, Def1; ::_thesis: verum end; hence Prod_of_RLS (X,Y) is right_zeroed by RLVECT_1:def_4; ::_thesis: verum end; end; registration let X, Y be non empty right_complementable RLSStruct ; cluster Prod_of_RLS (X,Y) -> right_complementable ; coherence Prod_of_RLS (X,Y) is right_complementable proof let u be Element of (Prod_of_RLS (X,Y)); :: according to ALGSTR_0:def_16 ::_thesis: u is right_complementable consider x, y being set 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 = x as VECTOR of X by A1; consider x1 being VECTOR of X such that A4: x + x1 = 0. X by ALGSTR_0:def_11; reconsider y = y as VECTOR of Y by A2; consider y1 being VECTOR of Y such that A5: y + y1 = 0. Y by ALGSTR_0:def_11; set u1 = [x1,y1]; reconsider u1 = [x1,y1] as Element of (Prod_of_RLS (X,Y)) ; take u1 ; :: according to ALGSTR_0:def_11 ::_thesis: u + u1 = 0. (Prod_of_RLS (X,Y)) thus u + u1 = 0. (Prod_of_RLS (X,Y)) by A3, A4, A5, Def1; ::_thesis: verum end; end; registration let X, Y be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; cluster Prod_of_RLS (X,Y) -> vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital ) proof A1: for a being real number for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2) proof let a be real number ; ::_thesis: for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2) reconsider a = a as Real by XREAL_0:def_1; let u1, u2 be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: a * (u1 + u2) = (a * u1) + (a * u2) consider x1, y1 being set 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 = x1 as VECTOR of X by A2; consider x2, y2 being set 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 = y2 as VECTOR of Y by A6; reconsider x2 = x2 as VECTOR of X by A5; reconsider y1 = 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 a * (u1 + u2) = (a * u1) + (a * u2) by A9, A11, A8, A10, Def1; ::_thesis: verum end; A12: for a, b being real number for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u) proof let a, b be real number ; ::_thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u) reconsider a = a, b = b as Real by XREAL_0:def_1; let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: (a * b) * u = a * (b * u) consider x, y being set 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 = y as VECTOR of Y by A14; reconsider x = 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 (a * b) * u = a * (b * u) by A15, A16, A17, Def2; ::_thesis: verum end; A18: for a, b being real number for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u) proof let a, b be real number ; ::_thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u) reconsider a = a, b = b as Real by XREAL_0:def_1; let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: (a + b) * u = (a * u) + (b * u) consider x, y being set 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 = y as VECTOR of Y by A20; reconsider x = 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 (a + b) * u = (a * u) + (b * u) by A21, A23, A24, Def2; ::_thesis: verum end; for u being VECTOR of (Prod_of_RLS (X,Y)) holds 1 * u = u proof let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: 1 * u = u consider x, y being set 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 = y as VECTOR of Y by A26; reconsider x = 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 1 * u = u by A27, A28, Def2; ::_thesis: verum end; hence ( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital ) by A1, A18, A12, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum end; end; theorem Th3: :: CONVFUN1:3 for X, Y being RealLinearSpace for n being Element of NAT for x being FinSequence of the carrier of X for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n & len y = n & len z = n & ( for i being Element of 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; ::_thesis: for n being Element of NAT for x being FinSequence of the carrier of X for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n & len y = n & len z = n & ( for i being Element of NAT st i in Seg n holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] defpred S1[ Element of NAT ] means for x being FinSequence of the carrier of X for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = $1 & len y = $1 & len z = $1 & ( for i being Element of NAT st i in Seg $1 holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)]; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let x be FinSequence of the carrier of X; ::_thesis: for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] let y be FinSequence of the carrier of Y; ::_thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); ::_thesis: ( len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] ) assume that A3: len x = n + 1 and A4: len y = n + 1 and A5: len z = n + 1 and A6: for i being Element of NAT st i in Seg (n + 1) holds z . i = [(x . i),(y . i)] ; ::_thesis: Sum z = [(Sum x),(Sum y)] 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 being Element of NAT st i in Seg n holds (z | n) . i = [((x | n) . i),((y | n) . i)] proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (z | n) . i = [((x | n) . i),((y | n) . i)] ) assume A11: i in Seg n ; ::_thesis: (z | n) . i = [((x | n) . i),((y | n) . i)] 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 (z | n) . i = [((x | n) . i),((y | n) . i)] by A6, A9, A11, A13, A14; ::_thesis: verum end; A15: for i being 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 ; ::_thesis: ( i in Seg (n + 1) implies ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) ) assume A16: i in Seg (n + 1) ; ::_thesis: ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) then A17: i <= n + 1 by FINSEQ_1:1; 1 <= i by A16, FINSEQ_1:1; hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by A3, A4, A5, A17, FINSEQ_4:15; ::_thesis: verum 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 Sum z = [(Sum x),(Sum y)] by A24, A22, A21, A20, Def1; ::_thesis: verum end; end; A26: S1[ 0 ] proof let x be FinSequence of the carrier of X; ::_thesis: for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] let y be FinSequence of the carrier of Y; ::_thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); ::_thesis: ( len x = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] ) assume that A27: len x = 0 and A28: len y = 0 and A29: len z = 0 and for i being Element of NAT st i in Seg 0 holds z . i = [(x . i),(y . i)] ; ::_thesis: Sum z = [(Sum x),(Sum y)] 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 Sum z = [(Sum x),(Sum y)] by A30, A31, RLVECT_1:43; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A26, A1); ::_thesis: verum end; begin definition func RLS_Real -> non empty RLSStruct equals :: CONVFUN1:def 4 RLSStruct(# REAL,0,addreal,multreal #); correctness coherence RLSStruct(# REAL,0,addreal,multreal #) is non empty RLSStruct ; ; end; :: deftheorem defines RLS_Real CONVFUN1:def_4_:_ RLS_Real = RLSStruct(# REAL,0,addreal,multreal #); registration cluster RLS_Real -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLS_Real is Abelian & RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof thus RLS_Real is Abelian ::_thesis: ( RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v 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 ; ::_thesis: verum end; thus RLS_Real is add-associative ::_thesis: ( RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let u, v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w) 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 (u + v) + w = u + (v + w) by A1; ::_thesis: verum end; thus RLS_Real is right_zeroed ::_thesis: ( RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let v be VECTOR of RLS_Real; :: according to RLVECT_1:def_4 ::_thesis: v + (0. RLS_Real) = v reconsider vr = v as Real ; thus v + (0. RLS_Real) = vr + 0 by BINOP_2:def_9 .= v ; ::_thesis: verum end; thus RLS_Real is right_complementable ::_thesis: ( RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let v be VECTOR of RLS_Real; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider vr = v as Real ; reconsider w = - vr as VECTOR of RLS_Real ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. RLS_Real thus v + w = vr + (- vr) by BINOP_2:def_9 .= 0. RLS_Real ; ::_thesis: verum end; thus for a being real number for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let a be real number ; ::_thesis: for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w) reconsider a = a as Real by XREAL_0:def_1; let v, w be VECTOR of RLS_Real; ::_thesis: a * (v + w) = (a * v) + (a * w) 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 a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum end; thus for a, b being real number for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proof let a, b be real number ; ::_thesis: for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v) reconsider a = a, b = b as Real by XREAL_0:def_1; let v be VECTOR of RLS_Real; ::_thesis: (a + b) * v = (a * v) + (b * v) 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 (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum end; thus for a, b being real number for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RLS_Real is scalar-unital proof let a, b be real number ; ::_thesis: for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v) reconsider a = a, b = b as Real by XREAL_0:def_1; let v be VECTOR of RLS_Real; ::_thesis: (a * b) * v = a * (b * v) 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 (a * b) * v = a * (b * v) ; ::_thesis: verum end; let v be VECTOR of RLS_Real; :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v reconsider vr = v as Real ; thus 1 * v = 1 * vr by BINOP_2:def_11 .= v ; ::_thesis: verum end; end; Lm1: for X being non empty RLSStruct for x being VECTOR of X for u being VECTOR of (Prod_of_RLS (X,RLS_Real)) for p, w being Real st u = [x,w] holds p * u = [(p * x),(p * w)] proof let X be non empty RLSStruct ; ::_thesis: for x being VECTOR of X for u being VECTOR of (Prod_of_RLS (X,RLS_Real)) for p, w being Real st u = [x,w] holds p * u = [(p * x),(p * w)] let x be VECTOR of X; ::_thesis: for u being VECTOR of (Prod_of_RLS (X,RLS_Real)) for p, w being Real st u = [x,w] holds p * u = [(p * x),(p * w)] let u be VECTOR of (Prod_of_RLS (X,RLS_Real)); ::_thesis: for p, w being Real st u = [x,w] holds p * u = [(p * x),(p * w)] let p, w be Real; ::_thesis: ( u = [x,w] implies p * u = [(p * x),(p * w)] ) reconsider y = w as VECTOR of RLS_Real ; assume A1: u = [x,w] ; ::_thesis: p * u = [(p * x),(p * w)] p * y = p * w by BINOP_2:def_11; hence p * u = [(p * x),(p * w)] by A1, Def2; ::_thesis: verum end; Lm2: for X being non empty RLSStruct for x1, x2 being VECTOR of X for w1, w2 being Real for u1, u2 being 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 ; ::_thesis: for x1, x2 being VECTOR of X for w1, w2 being Real for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) st u1 = [x1,w1] & u2 = [x2,w2] holds u1 + u2 = [(x1 + x2),(w1 + w2)] let x1, x2 be VECTOR of X; ::_thesis: for w1, w2 being Real for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) st u1 = [x1,w1] & u2 = [x2,w2] holds u1 + u2 = [(x1 + x2),(w1 + w2)] let w1, w2 be Real; ::_thesis: for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) st u1 = [x1,w1] & u2 = [x2,w2] holds u1 + u2 = [(x1 + x2),(w1 + w2)] let u1, u2 be VECTOR of (Prod_of_RLS (X,RLS_Real)); ::_thesis: ( u1 = [x1,w1] & u2 = [x2,w2] implies u1 + u2 = [(x1 + x2),(w1 + w2)] ) reconsider y1 = w1 as VECTOR of RLS_Real ; reconsider y2 = w2 as VECTOR of RLS_Real ; assume that A1: u1 = [x1,w1] and A2: u2 = [x2,w2] ; ::_thesis: u1 + u2 = [(x1 + x2),(w1 + w2)] y1 + y2 = w1 + w2 by BINOP_2:def_9; hence u1 + u2 = [(x1 + x2),(w1 + w2)] by A1, A2, Def1; ::_thesis: verum end; Lm3: for a being FinSequence of the carrier of RLS_Real for b being FinSequence of REAL st len a = len b & ( for i being 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; ::_thesis: for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) defpred S1[ Element of NAT ] means for a being FinSequence of the carrier of RLS_Real for b being FinSequence of REAL st len a = $1 & len b = $1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let a be FinSequence of the carrier of RLS_Real; ::_thesis: for b being FinSequence of REAL st len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) assume that A3: len a = n + 1 and A4: len b = n + 1 and A5: for i being Element of NAT st i in dom a holds a . i = b . i ; ::_thesis: Sum a = Sum b 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 being 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 ; ::_thesis: ( i in Seg (n + 1) implies ( a . i = a /. i & a /. i = b . i ) ) assume A10: i in Seg (n + 1) ; ::_thesis: ( a . i = a /. i & a /. i = b . i ) 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 ( a . i = a /. i & a /. i = b . i ) by A5, A8, A10; ::_thesis: verum end; A12: Seg n c= Seg (n + 1) by A6, FINSEQ_1:5; A13: for i being Element of NAT st i in dom (a | n) holds (a | n) . i = (b | n) . i proof let i be Element of NAT ; ::_thesis: ( i in dom (a | n) implies (a | n) . i = (b | n) . i ) assume i in dom (a | n) ; ::_thesis: (a | n) . i = (b | n) . i 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 (a | n) . i = (b | n) . i by A5, A8, A12, A14, A16; ::_thesis: verum 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 Sum a = Sum b by A18, RVSUM_1:74; ::_thesis: verum end; end; A21: S1[ 0 ] proof let a be FinSequence of the carrier of RLS_Real; ::_thesis: for b being FinSequence of REAL st len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) assume that A22: len a = 0 and A23: len b = 0 and for i being Element of NAT st i in dom a holds a . i = b . i ; ::_thesis: Sum a = Sum b a = <*> the carrier of RLS_Real by A22; then A24: Sum a = 0. RLS_Real by RLVECT_1:43; b = <*> REAL by A23; hence Sum a = Sum b by A24, RVSUM_1:72; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A1); hence ( len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) ; ::_thesis: verum end; begin Lm4: for F being FinSequence of ExtREAL for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x proof let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x let x be Element of ExtREAL ; ::_thesis: Sum (F ^ <*x*>) = (Sum F) + x consider f being Function of NAT,ExtREAL such that A1: Sum (F ^ <*x*>) = f . (len (F ^ <*x*>)) and A2: f . 0 = 0. and A3: for i being Element of 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 being Element of NAT st i < len F holds f . (i + 1) = (f . i) + (F . (i + 1)) proof let i be Element of NAT ; ::_thesis: ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) ) A5: 1 <= i + 1 by NAT_1:11; assume A6: i < len F ; ::_thesis: f . (i + 1) = (f . i) + (F . (i + 1)) 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 f . (i + 1) = (f . i) + (F . (i + 1)) by A7, FINSEQ_1:def_7; ::_thesis: verum 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 Sum (F ^ <*x*>) = (Sum F) + x by A1, A4, A8, FINSEQ_1:42; ::_thesis: verum end; Lm5: for F being FinSequence of ExtREAL st not -infty in rng F holds Sum F <> -infty proof defpred S1[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum $1 <> -infty ); A1: for F being FinSequence of ExtREAL for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] proof let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>] A3: Sum (F ^ <*x*>) = (Sum F) + x by Lm4; assume not -infty in rng (F ^ <*x*>) ; ::_thesis: Sum (F ^ <*x*>) <> -infty 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 Sum (F ^ <*x*>) <> -infty by A2, A4, A3, XBOOLE_0:def_3, XXREAL_3:17; ::_thesis: verum end; A5: S1[ <*> ExtREAL] by EXTREAL1:7; thus for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A5, A1); ::_thesis: verum end; Lm6: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds Sum F = +infty proof defpred S1[ FinSequence of ExtREAL ] means ( +infty in rng $1 & not -infty in rng $1 implies Sum $1 = +infty ); A1: for F being FinSequence of ExtREAL for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] proof let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>] assume that A3: +infty in rng (F ^ <*x*>) and A4: not -infty in rng (F ^ <*x*>) ; ::_thesis: Sum (F ^ <*x*>) = +infty 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; percases ( +infty in rng F or +infty = x ) by A6, TARSKI:def_1; suppose +infty in rng F ; ::_thesis: Sum (F ^ <*x*>) = +infty hence Sum (F ^ <*x*>) = +infty by A2, A7, A9, A5, XBOOLE_0:def_3, XXREAL_3:def_2; ::_thesis: verum end; suppose +infty = x ; ::_thesis: Sum (F ^ <*x*>) = +infty hence Sum (F ^ <*x*>) = +infty by A5, A8, XXREAL_3:def_2; ::_thesis: verum end; end; end; A10: S1[ <*> ExtREAL] ; thus for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A10, A1); ::_thesis: verum end; Lm7: for a being FinSequence of ExtREAL for b being FinSequence of REAL st len a = len b & ( for i being 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 ; ::_thesis: for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) defpred S1[ Element of NAT ] means for a being FinSequence of ExtREAL for b being FinSequence of REAL st len a = $1 & len b = $1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let a be FinSequence of ExtREAL ; ::_thesis: for b being FinSequence of REAL st len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) assume that A3: len a = n + 1 and A4: len b = n + 1 and A5: for i being Element of NAT st i in dom a holds a . i = b . i ; ::_thesis: Sum a = Sum b 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 being Element of NAT st i in dom (a | n) holds (a | n) . i = (b | n) . i proof let i be Element of NAT ; ::_thesis: ( i in dom (a | n) implies (a | n) . i = (b | n) . i ) assume i in dom (a | n) ; ::_thesis: (a | n) . i = (b | n) . i 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 (a | n) . i = (b | n) . i by A5, A6, A10, A12, A14; ::_thesis: verum 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 Sum a = Sum b by A16, RVSUM_1:74; ::_thesis: verum end; end; A17: S1[ 0 ] proof let a be FinSequence of ExtREAL ; ::_thesis: for b being FinSequence of REAL st len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of REAL ; ::_thesis: ( len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) assume that A18: len a = 0 and A19: len b = 0 and for i being Element of NAT st i in dom a holds a . i = b . i ; ::_thesis: Sum a = Sum b a = <*> ExtREAL by A18; then A20: Sum a = 0. by EXTREAL1:7; b = <*> ExtREAL by A19; hence Sum a = Sum b by A20, RVSUM_1:72; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A1); hence ( len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) implies Sum a = Sum b ) ; ::_thesis: verum end; Lm8: for n being Element of NAT for a being FinSequence of ExtREAL for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being 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 ; ::_thesis: for a being FinSequence of ExtREAL for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds a . i = b . i ) holds Sum a = Sum b let a be FinSequence of ExtREAL ; ::_thesis: for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds a . i = b . i ) holds Sum a = Sum b let b be FinSequence of the carrier of RLS_Real; ::_thesis: ( len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds a . i = b . i ) implies Sum a = Sum b ) assume that A1: len a = n and A2: len b = n and A3: for i being Element of NAT st i in Seg n holds a . i = b . i ; ::_thesis: Sum a = Sum b set c = b; reconsider c = b 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 being Element of NAT st i in dom b holds b . i = c . i ; len b = len c ; hence Sum a = Sum b by A4, A5, Lm3; ::_thesis: verum end; Lm9: for F being FinSequence of ExtREAL st rng F c= {0.} holds Sum F = 0. proof let F be FinSequence of ExtREAL ; ::_thesis: ( rng F c= {0.} implies Sum F = 0. ) defpred S1[ FinSequence of ExtREAL ] means ( rng $1 c= {0.} implies Sum $1 = 0. ); assume A1: rng F c= {0.} ; ::_thesis: Sum F = 0. A2: for F being FinSequence of ExtREAL for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] proof let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds S1[F ^ <*x*>] let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] ) assume A3: S1[F] ; ::_thesis: S1[F ^ <*x*>] assume rng (F ^ <*x*>) c= {0.} ; ::_thesis: Sum (F ^ <*x*>) = 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 ; ::_thesis: verum end; A6: S1[ <*> ExtREAL] by EXTREAL1:7; for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A6, A2); hence Sum F = 0. by A1; ::_thesis: verum end; Lm10: for F being FinSequence of REAL st rng F c= {0} holds Sum F = 0 proof let F be FinSequence of REAL ; ::_thesis: ( rng F c= {0} implies Sum F = 0 ) defpred S1[ FinSequence of REAL ] means ( rng $1 c= {0} implies Sum $1 = 0 ); A1: for F being FinSequence of REAL for x being Element of REAL st S1[F] holds S1[F ^ <*x*>] proof let F be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[F] holds S1[F ^ <*x*>] let x be Element of REAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>] assume rng (F ^ <*x*>) c= {0} ; ::_thesis: Sum (F ^ <*x*>) = 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 ; ::_thesis: verum end; assume A5: rng F c= {0} ; ::_thesis: Sum F = 0 A6: S1[ <*> REAL] by RVSUM_1:72; for F being FinSequence of REAL holds S1[F] from FINSEQ_2:sch_2(A6, A1); hence Sum F = 0 by A5; ::_thesis: verum end; Lm11: for X being RealLinearSpace for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds Sum F = 0. X proof let X be RealLinearSpace; ::_thesis: for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds Sum F = 0. X defpred S1[ FinSequence of the carrier of X] means ( rng $1 c= {(0. X)} implies Sum $1 = 0. X ); A1: for F being FinSequence of the carrier of X for x being Element of X st S1[F] holds S1[F ^ <*x*>] proof let F be FinSequence of the carrier of X; ::_thesis: for x being Element of X st S1[F] holds S1[F ^ <*x*>] let x be Element of X; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] ) assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>] assume rng (F ^ <*x*>) c= {(0. X)} ; ::_thesis: Sum (F ^ <*x*>) = 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, RLVECT_1:def_4, XBOOLE_1:11 ; ::_thesis: verum end; let F be FinSequence of the carrier of X; ::_thesis: ( rng F c= {(0. X)} implies Sum F = 0. X ) assume A5: rng F c= {(0. X)} ; ::_thesis: Sum F = 0. X A6: S1[ <*> the carrier of X] by RLVECT_1:43; for F being FinSequence of the carrier of X holds S1[F] from FINSEQ_2:sch_2(A6, A1); hence Sum F = 0. X by A5; ::_thesis: verum end; begin definition let X be non empty RLSStruct ; let f be Function of the carrier of X,ExtREAL; func epigraph f -> Subset of (Prod_of_RLS (X,RLS_Real)) equals :: CONVFUN1:def 5 { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ; coherence { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } is Subset of (Prod_of_RLS (X,RLS_Real)) proof deffunc H1( Element of X, Element of REAL ) -> Element of [: the carrier of X,REAL:] = [$1,$2]; defpred S1[ Element of X, Element of REAL ] means f . $1 <= R_EAL $2; { H1(x,y) where x is Element of X, y is Element of REAL : S1[x,y] } is Subset of [: the carrier of X,REAL:] from DOMAIN_1:sch_9(); hence { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } is Subset of (Prod_of_RLS (X,RLS_Real)) ; ::_thesis: verum end; end; :: deftheorem defines epigraph CONVFUN1:def_5_:_ for X being non empty RLSStruct for f being Function of the carrier of X,ExtREAL holds epigraph f = { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ; definition let X be non empty RLSStruct ; let f be Function of the carrier of X,ExtREAL; attrf is convex means :Def6: :: CONVFUN1:def 6 epigraph f is convex ; end; :: deftheorem Def6 defines convex CONVFUN1:def_6_:_ for X being non empty RLSStruct for f being Function of the carrier of X,ExtREAL holds ( f is convex iff epigraph f is convex ); Lm12: for w1, w2 being R_eal for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) proof let w1, w2 be R_eal; ::_thesis: for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) let wr1, wr2, p1, p2 be Real; ::_thesis: ( w1 = wr1 & w2 = wr2 implies (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) ) assume that A1: w1 = wr1 and A2: w2 = wr2 ; ::_thesis: (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) A3: p2 * wr2 = (R_EAL p2) * w2 by A2, EXTREAL1:1; p1 * wr1 = (R_EAL p1) * w1 by A1, EXTREAL1:1; hence (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) by A3, SUPINF_2:1; ::_thesis: verum end; theorem Th4: :: CONVFUN1:4 for X being non empty RLSStruct for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) proof let X be non empty RLSStruct ; ::_thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) ) assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) thus ( f is convex implies for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) ::_thesis: ( ( for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) implies f is convex ) proof assume f is convex ; ::_thesis: for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) then A2: epigraph f is convex by Def6; let x1, x2 be VECTOR of X; ::_thesis: for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) let p be Real; ::_thesis: ( 0 < p & p < 1 implies f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) assume that A3: 0 < p and A4: p < 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) set p2 = R_EAL (1 - p); set p1 = R_EAL p; A5: 1 - p > 0 by A4, XREAL_1:50; percases ( ( f . x1 in REAL & f . x2 in REAL ) or ( f . x1 = +infty & f . x2 in REAL ) or ( f . x1 in REAL & f . x2 = +infty ) or ( f . x1 = +infty & f . x2 = +infty ) ) by A1, XXREAL_0:14; supposeA6: ( f . x1 in REAL & f . x2 in REAL ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) then reconsider w2 = f . x2 as Real ; reconsider w1 = f . x1 as 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)) ; f . x2 <= R_EAL w2 ; then 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; f . x1 <= R_EAL w1 ; then [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 being Element of X, y0 being Element of REAL such that A10: [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] and A11: f . x0 <= R_EAL 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 f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, Lm12; ::_thesis: verum end; supposeA13: ( f . x1 = +infty & f . x2 in REAL ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) A14: (R_EAL (1 - p)) * (f . x2) in REAL proof reconsider w2 = f . x2 as Real by A13; (R_EAL (1 - p)) * (f . x2) = (1 - p) * w2 by EXTREAL1:1; hence (R_EAL (1 - p)) * (f . x2) in REAL ; ::_thesis: verum end; (R_EAL p) * (f . x1) = +infty by A3, A13, XXREAL_3:def_5; then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A14, XXREAL_3:def_2; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum end; supposeA15: ( f . x1 in REAL & f . x2 = +infty ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) A16: (R_EAL p) * (f . x1) in REAL proof reconsider w1 = f . x1 as Real by A15; (R_EAL p) * (f . x1) = p * w1 by EXTREAL1:1; hence (R_EAL p) * (f . x1) in REAL ; ::_thesis: verum end; (R_EAL (1 - p)) * (f . x2) = +infty by A5, A15, XXREAL_3:def_5; then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A16, XXREAL_3:def_2; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum end; supposeA17: ( f . x1 = +infty & f . x2 = +infty ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) then (R_EAL (1 - p)) * (f . x2) = +infty by A5, XXREAL_3:def_5; then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A3, A17, XXREAL_3:def_2; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum end; end; end; assume A18: for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ; ::_thesis: f is convex for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) for p being 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)); ::_thesis: for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds (p * u1) + ((1 - p) * u2) in epigraph f let p be Real; ::_thesis: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f implies (p * u1) + ((1 - p) * u2) in epigraph f ) assume that A19: 0 < p and A20: p < 1 and A21: u1 in epigraph f and A22: u2 in epigraph f ; ::_thesis: (p * u1) + ((1 - p) * u2) in epigraph f thus (p * u1) + ((1 - p) * u2) in epigraph f ::_thesis: verum proof consider x2 being Element of X, y2 being Element of REAL such that A23: u2 = [x2,y2] and A24: f . x2 <= R_EAL 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 Real by A1, XXREAL_0:14; consider x1 being Element of X, y1 being Element of REAL such that A26: u1 = [x1,y1] and A27: f . x1 <= R_EAL y1 by A21; f . x1 <> +infty by A27, XXREAL_0:9; then reconsider w1 = f . x1 as 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: R_EAL ((p * w1) + ((1 - p) * w2)) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by Lm12; then f . ((p * x1) + ((1 - p) * x2)) <> +infty by A18, A19, A20, XXREAL_0:9; then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Real by A1, XXREAL_0:14; w <= (p * w1) + ((1 - p) * w2) by A18, A19, A20, A30; then f . ((p * x1) + ((1 - p) * x2)) <= R_EAL ((p * y1) + ((1 - p) * y2)) by A29, XXREAL_0:2; then A31: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ; p * u1 = [(p * x1),(p * y1)] by A26, Lm1; hence (p * u1) + ((1 - p) * u2) in epigraph f by A31, A25, Lm2; ::_thesis: verum end; end; then epigraph f is convex by CONVEX1:def_2; hence f is convex by Def6; ::_thesis: verum end; theorem :: CONVFUN1:5 for X being RealLinearSpace for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) proof let X be RealLinearSpace; ::_thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) ) assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) thus ( f is convex implies for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) ::_thesis: ( ( for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) implies f is convex ) proof assume A2: f is convex ; ::_thesis: for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) let x1, x2 be VECTOR of X; ::_thesis: for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) assume that A3: 0 <= p and A4: p <= 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) percases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ; supposeA5: p = 0 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) 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, RLVECT_1:4; A8: (R_EAL (1 - p)) * (f . x2) = f . x2 by A5, XXREAL_3:81; (R_EAL p) * (f . x1) = 0. by A5; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A7, A8, XXREAL_3:4; ::_thesis: verum end; supposeA9: p = 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) 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, RLVECT_1:4; A12: (R_EAL p) * (f . x1) = f . x1 by A9, XXREAL_3:81; (R_EAL (1 - p)) * (f . x2) = 0. by A9; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, XXREAL_3:4; ::_thesis: verum end; supposeA13: ( p <> 0 & p <> 1 ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) then p < 1 by A4, XXREAL_0:1; hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A1, A2, A3, A13, Th4; ::_thesis: verum end; end; end; assume for x1, x2 being VECTOR of X for p being Real st 0 <= p & p <= 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ; ::_thesis: f is convex then for x1, x2 being VECTOR of X for p being Real st 0 < p & p < 1 holds f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ; hence f is convex by A1, Th4; ::_thesis: verum end; begin theorem :: CONVFUN1:6 for f being PartFunc of REAL,REAL for g being Function of the carrier of RLS_Real,ExtREAL for X being Subset of RLS_Real st X c= dom f & ( for x being 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; ::_thesis: for g being Function of the carrier of RLS_Real,ExtREAL for X being Subset of RLS_Real st X c= dom f & ( for x being 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 ) ) let g be Function of the carrier of RLS_Real,ExtREAL; ::_thesis: for X being Subset of RLS_Real st X c= dom f & ( for x being 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 ) ) let X be Subset of RLS_Real; ::_thesis: ( X c= dom f & ( for x being Real holds ( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ) implies ( g is convex iff ( f is_convex_on X & X is convex ) ) ) assume that A1: X c= dom f and A2: for x being Real holds ( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ; ::_thesis: ( g is convex iff ( f is_convex_on X & X is convex ) ) A3: for v being VECTOR of RLS_Real holds g . v <> -infty proof let v be VECTOR of RLS_Real; ::_thesis: g . v <> -infty reconsider x = v as Real ; f . x in REAL ; hence g . v <> -infty by A2; ::_thesis: verum end; A4: for v being VECTOR of RLS_Real st v in X holds g . v in REAL proof let v be VECTOR of RLS_Real; ::_thesis: ( v in X implies g . v in REAL ) reconsider x = v as Real ; assume v in X ; ::_thesis: g . v in REAL then g . x = f . x by A2; hence g . v in REAL ; ::_thesis: verum end; thus ( g is convex implies ( f is_convex_on X & X is convex ) ) ::_thesis: ( f is_convex_on X & X is convex implies g is convex ) proof assume A5: g is convex ; ::_thesis: ( f is_convex_on X & X is convex ) for p being Real st 0 <= p & p <= 1 holds for x1, x2 being 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; ::_thesis: ( 0 <= p & p <= 1 implies for x1, x2 being 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)) ) assume that A6: 0 <= p and A7: p <= 1 ; ::_thesis: for x1, x2 being 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)) let x1, x2 be Real; ::_thesis: ( x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) assume that A8: x1 in X and A9: x2 in X and A10: (p * x1) + ((1 - p) * x2) in X ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) 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; percases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ; suppose p = 0 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ; ::_thesis: verum end; suppose p = 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ; ::_thesis: verum end; supposeA14: ( p <> 0 & p <> 1 ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) reconsider v2 = x2 as VECTOR of RLS_Real ; reconsider v1 = x1 as VECTOR of RLS_Real ; 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)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A11, A13, Lm12; hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A3, A5, A6, A14, A17, A16, Th4; ::_thesis: verum end; end; end; hence f is_convex_on X by A1, RFUNCT_3:def_12; ::_thesis: X is convex for v1, v2 being VECTOR of RLS_Real for p being 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; ::_thesis: for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds (p * v1) + ((1 - p) * v2) in X let p be Real; ::_thesis: ( 0 < p & p < 1 & v1 in X & v2 in X implies (p * v1) + ((1 - p) * v2) in X ) assume that A18: 0 < p and A19: p < 1 and A20: v1 in X and A21: v2 in X ; ::_thesis: (p * v1) + ((1 - p) * v2) in X reconsider w1 = g . v1, w2 = g . v2 as Real by A4, A20, A21; A22: (p * w1) + ((1 - p) * w2) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by Lm12; g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A3, A5, A18, A19, Th4; then g . ((p * v1) + ((1 - p) * v2)) <> +infty by A22, XXREAL_0:9; hence (p * v1) + ((1 - p) * v2) in X by A2; ::_thesis: verum end; hence X is convex by CONVEX1:def_2; ::_thesis: verum end; thus ( f is_convex_on X & X is convex implies g is convex ) ::_thesis: verum proof assume that A23: f is_convex_on X and A24: X is convex ; ::_thesis: g is convex for v1, v2 being VECTOR of RLS_Real for p being Real st 0 < p & p < 1 holds g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) proof let v1, v2 be VECTOR of RLS_Real; ::_thesis: for p being Real st 0 < p & p < 1 holds g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) let p be Real; ::_thesis: ( 0 < p & p < 1 implies g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) ) assume that A25: 0 < p and A26: p < 1 ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) reconsider x2 = v2 as Real ; reconsider x1 = v1 as Real ; A27: 1 - p > 0 by A26, XREAL_1:50; percases ( ( v1 in X & v2 in X ) or ( v1 in X & not v2 in X ) or ( not v1 in X & v2 in X ) or ( not v1 in X & not v2 in X ) ) ; supposeA28: ( v1 in X & v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) then A29: f . x2 = g . v2 by A2; f . x1 = g . v1 by A2, A28; then A30: (p * (f . x1)) + ((1 - p) * (f . x2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A29, Lm12; A31: (1 - p) * v2 = (1 - p) * x2 by BINOP_2:def_11; p * v1 = p * x1 by BINOP_2:def_11; then A32: (p * v1) + ((1 - p) * v2) = (p * x1) + ((1 - p) * x2) by A31, BINOP_2:def_9; A33: (p * v1) + ((1 - p) * v2) in X by A24, A25, A26, A28, CONVEX1:def_2; then f . ((p * x1) + ((1 - p) * x2)) = g . ((p * v1) + ((1 - p) * v2)) by A2, A32; hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A23, A25, A26, A28, A33, A32, A30, RFUNCT_3:def_12; ::_thesis: verum end; supposeA34: ( v1 in X & not v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) then g . x2 = +infty by A2; then A35: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def_5; reconsider w1 = g . x1 as Real by A4, A34; p * w1 = (R_EAL p) * (g . v1) by EXTREAL1:1; then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A35, XXREAL_3:def_2; hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum end; supposeA36: ( not v1 in X & v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) then g . x1 = +infty by A2; then A37: (R_EAL p) * (g . v1) = +infty by A25, XXREAL_3:def_5; reconsider w2 = g . x2 as Real by A4, A36; (1 - p) * w2 = (R_EAL (1 - p)) * (g . v2) by EXTREAL1:1; then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A37, XXREAL_3:def_2; hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum end; supposeA38: ( not v1 in X & not v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) then g . x2 = +infty by A2; then A39: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def_5; g . x1 = +infty by A2, A38; then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A25, A39, XXREAL_3:def_2; hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum end; end; end; hence g is convex by A3, Th4; ::_thesis: verum end; end; begin theorem Th7: :: CONVFUN1:7 for X being RealLinearSpace for M being Subset of X holds ( M is convex iff for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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; ::_thesis: for M being Subset of X holds ( M is convex iff for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 ) let M be Subset of X; ::_thesis: ( M is convex iff for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 ) thus ( M is convex implies for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 ) ::_thesis: ( ( for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 defpred S1[ Nat] means for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = $1 & len y = $1 & len z = $1 & Sum p = 1 & ( for i being 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 ; ::_thesis: for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 A2: for n being non empty Nat st S1[n] holds S1[n + 1] proof let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] thus for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being 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 ::_thesis: verum proof let p be FinSequence of REAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being 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 let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M ) 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 being Nat st i in Seg (n + 1) holds ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; ::_thesis: Sum z 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 being Nat st i in dom (p | n) holds 0 <= (p | n) . i proof let i be Nat; ::_thesis: ( i in dom (p | n) implies 0 <= (p | n) . i ) assume A17: i in dom (p | n) ; ::_thesis: 0 <= (p | n) . i then A18: i <= n by A14, FINSEQ_1:1; p . i > 0 by A8, A14, A15, A17; hence 0 <= (p | n) . i by A18, FINSEQ_3:112; ::_thesis: verum end; set y9 = y | n; set p9 = (1 / (1 - (p . (n + 1)))) * (p | n); deffunc H1( Nat) -> Element of the carrier of X = (((1 / (1 - (p . (n + 1)))) * (p | n)) . $1) * ((y | n) /. $1); consider z9 being FinSequence of the carrier of X such that A19: len z9 = n and A20: for i being Nat st i in dom z9 holds z9 . i = H1(i) from FINSEQ_2:sch_1(); A21: len (y | n) = n by A5, A12, FINSEQ_1:59; then A22: dom (y | n) = Seg n by FINSEQ_1:def_3; A23: for i being Element of NAT for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds z9 . i = (1 / (1 - (p . (n + 1)))) * v proof let i be Element of NAT ; ::_thesis: for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds z9 . i = (1 / (1 - (p . (n + 1)))) * v let v be VECTOR of X; ::_thesis: ( i in dom z9 & v = (z | n) . i implies z9 . i = (1 / (1 - (p . (n + 1)))) * v ) assume that A24: i in dom z9 and A25: v = (z | n) . i ; ::_thesis: z9 . i = (1 / (1 - (p . (n + 1)))) * v A26: i in Seg n by A19, A24, FINSEQ_1:def_3; then A27: (y | n) /. 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 = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A24 .= ((1 / (1 - (p . (n + 1)))) * ((p | n) . i)) * ((y | n) /. i) by RVSUM_1:44 .= ((1 / (1 - (p . (n + 1)))) * (p . i)) * ((y | n) /. i) by A28, FINSEQ_3:112 .= (1 / (1 - (p . (n + 1)))) * ((p . i) * ((y | n) /. i)) by RLVECT_1:def_7 .= (1 / (1 - (p . (n + 1)))) * v by A8, A15, A25, A26, A29, A27 ; hence z9 . i = (1 / (1 - (p . (n + 1)))) * v ; ::_thesis: verum end; 1 <= n by NAT_1:14; then 1 in Seg n by FINSEQ_1:1; then A30: 1 - (p . (n + 1)) > 0 by A11, A14, A16, A10, RVSUM_1:85; dom ((1 / (1 - (p . (n + 1)))) * (p | n)) = Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) by FINSEQ_1:def_3; then Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) = Seg (len (p | n)) by A9, VALUED_1:def_5; then A31: len ((1 / (1 - (p . (n + 1)))) * (p | n)) = 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: 1 - (p . (n + 1)) < 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 - (1 - (p . (n + 1)))) * (y /. (n + 1))) by RLVECT_1:44 ; A37: dom z9 = Seg n by A19, FINSEQ_1:def_3; A38: for i being Nat st i in Seg n holds ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) proof (1 - (p . (n + 1))) " > 0 by A30; then A39: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:215; let i be Nat; ::_thesis: ( i in Seg n implies ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) ) assume A40: i in Seg n ; ::_thesis: ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) then A41: i <= n by FINSEQ_1:1; A42: ((1 / (1 - (p . (n + 1)))) * (p | n)) . i = (1 / (1 - (p . (n + 1)))) * ((p | n) . i) by RVSUM_1:44 .= (1 / (1 - (p . (n + 1)))) * (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 ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 by A39, A42, XREAL_1:129; ::_thesis: ( z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A37, A40; ::_thesis: (y | n) /. i in M y /. i in M by A8, A40, A43; hence (y | n) /. i in M by A22, A40, FINSEQ_4:70; ::_thesis: verum end; len (z | n) = n by A6, A12, FINSEQ_1:59; then A44: (1 - (p . (n + 1))) * (Sum z9) = (1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n))) by A19, A23, RLVECT_1:39 .= ((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (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 ((1 / (1 - (p . (n + 1)))) * (p | n)) = (1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) by A11, RVSUM_1:87 .= 1 by A30, XCMPLX_1:106 ; then Sum z9 in M by A3, A19, A31, A21, A38; hence Sum z in M by A1, A33, A34, A30, A36, A44, CONVEX1:def_2; ::_thesis: verum end; end; A45: S1[1] proof let p be FinSequence of REAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being 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 let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being Nat st i in Seg 1 holds ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M ) assume that A46: len p = 1 and len y = 1 and A47: len z = 1 and A48: Sum p = 1 and A49: for i being Nat st i in Seg 1 holds ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; ::_thesis: Sum z in M p = <*(p . 1)*> 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 Sum z in M by A53, A52, RLVECT_1:44; ::_thesis: verum end; thus for n being non empty Nat holds S1[n] from NAT_1:sch_10(A45, A2); ::_thesis: verum end; thus ( ( for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 ) ::_thesis: verum proof assume A54: for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being 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 ; ::_thesis: M is convex for x1, x2 being VECTOR of X for r being 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; ::_thesis: for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds (r * x1) + ((1 - r) * x2) in M let r be Real; ::_thesis: ( 0 < r & r < 1 & x1 in M & x2 in M implies (r * x1) + ((1 - r) * x2) in M ) assume that A55: 0 < r and A56: r < 1 and A57: x1 in M and A58: x2 in M ; ::_thesis: (r * x1) + ((1 - r) * x2) in M set z = <*(r * x1),((1 - r) * x2)*>; set y = <*x1,x2*>; set p = <*r,(1 - r)*>; A59: for i being Nat st i in Seg 2 holds ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) proof let i be Nat; ::_thesis: ( i in Seg 2 implies ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) ) assume A60: i in Seg 2 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) percases ( i = 1 or i = 2 ) by A60, FINSEQ_1:2, TARSKI:def_2; supposeA61: i = 1 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) then A62: <*x1,x2*> /. i = x1 by FINSEQ_4:17; <*r,(1 - r)*> . i = r by A61, FINSEQ_1:44; hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A55, A57, A61, A62, FINSEQ_1:44; ::_thesis: verum end; supposeA63: i = 2 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) then A64: <*x1,x2*> /. i = x2 by FINSEQ_4:17; <*r,(1 - r)*> . i = 1 - r by A63, FINSEQ_1:44; hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A56, A58, A63, A64, FINSEQ_1:44, XREAL_1:50; ::_thesis: verum end; end; end; A65: len <*x1,x2*> = 2 by FINSEQ_1:44; A66: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77 .= 1 ; A67: len <*(r * x1),((1 - r) * x2)*> = 2 by FINSEQ_1:44; len <*r,(1 - r)*> = 2 by FINSEQ_1:44; then Sum <*(r * x1),((1 - r) * x2)*> in M by A54, A65, A67, A66, A59; hence (r * x1) + ((1 - r) * x2) in M by RLVECT_1:45; ::_thesis: verum end; hence M is convex by CONVEX1:def_2; ::_thesis: verum end; end; begin Lm13: for X being RealLinearSpace for f being Function of the carrier of X,ExtREAL for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F proof let X be RealLinearSpace; ::_thesis: for f being Function of the carrier of X,ExtREAL for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F let f be Function of the carrier of X,ExtREAL; ::_thesis: for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F let n be non empty Element of NAT ; ::_thesis: for p being FinSequence of REAL for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F let p be FinSequence of REAL ; ::_thesis: for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F let F be FinSequence of ExtREAL ; ::_thesis: for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F let y be FinSequence of the carrier of X; ::_thesis: ( len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies not -infty in rng F ) assume that A1: len F = n and A2: for x being VECTOR of X holds f . x <> -infty and A3: for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; ::_thesis: not -infty in rng F for i being set st i in dom F holds F . i <> -infty proof let i be set ; ::_thesis: ( i in dom F implies F . i <> -infty ) assume A4: i in dom F ; ::_thesis: F . i <> -infty then reconsider i = 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 = (R_EAL (p . i)) * (f . (y /. i)) by A3, A5; percases ( R_EAL (p . i) = 0. or f . (y /. i) <> +infty or ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ) ; suppose R_EAL (p . i) = 0. ; ::_thesis: F . i <> -infty hence F . i <> -infty by A7; ::_thesis: verum end; suppose f . (y /. i) <> +infty ; ::_thesis: F . i <> -infty then reconsider w = f . (y /. i) as Real by A2, XXREAL_0:14; F . i = (p . i) * w by A7, EXTREAL1:1; hence F . i <> -infty ; ::_thesis: verum end; suppose ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ; ::_thesis: F . i <> -infty hence F . i <> -infty by A6, A7; ::_thesis: verum end; end; end; hence not -infty in rng F by FUNCT_1:def_3; ::_thesis: verum end; theorem Th8: :: CONVFUN1:8 for X being RealLinearSpace for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) proof let X be RealLinearSpace; ::_thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) ) assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) thus ( f is convex implies for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) ::_thesis: ( ( for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) implies f is convex ) proof assume A2: f is convex ; ::_thesis: for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let n be non empty Element of NAT ; ::_thesis: for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let p be FinSequence of REAL ; ::_thesis: for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let F be FinSequence of ExtREAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F ) 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 being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; ::_thesis: f . (Sum z) <= Sum F for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A7; then A8: not -infty in rng F by A1, A4, Lm13; percases ( for i being Element of NAT st i in Seg n holds f . (y /. i) <> +infty or ex i being Element of NAT st ( i in Seg n & f . (y /. i) = +infty ) ) ; supposeA9: for i being Element of NAT st i in Seg n holds f . (y /. i) <> +infty ; ::_thesis: f . (Sum z) <= Sum F defpred S1[ set , set ] means $2 = [(y /. $1),(f . (y /. $1))]; reconsider V = Prod_of_RLS (X,RLS_Real) as RealLinearSpace ; A10: for i being Element of NAT st i in Seg n holds f . (y /. i) in REAL proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies f . (y /. i) in REAL ) assume i in Seg n ; ::_thesis: f . (y /. i) in REAL then f . (y /. i) <> +infty by A9; hence f . (y /. i) in REAL by A1, XXREAL_0:14; ::_thesis: verum end; A11: for i being Element of NAT st i in Seg n holds ex v being Element of V st S1[i,v] proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex v being Element of V st S1[i,v] ) assume i in Seg n ; ::_thesis: ex v being Element of V st S1[i,v] then reconsider w = f . (y /. i) as Real by A10; set v = [(y /. i),w]; reconsider v = [(y /. i),w] as Element of V ; take v ; ::_thesis: S1[i,v] thus S1[i,v] ; ::_thesis: verum end; consider g being FinSequence of the carrier of V such that A12: dom g = Seg n and A13: for i being Element of NAT st i in Seg n holds S1[i,g /. i] from RECDEF_1:sch_17(A11); A14: len g = n by A12, FINSEQ_1:def_3; defpred S2[ set , set ] means $2 = F . $1; A15: for i being Element of NAT st i in Seg n holds ex w being Element of RLS_Real st S2[i,w] proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex w being Element of RLS_Real st S2[i,w] ) assume A16: i in Seg n ; ::_thesis: ex w being Element of RLS_Real st S2[i,w] then reconsider a = f . (y /. i) as Real by A10; F . i = (R_EAL (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 ; take w ; ::_thesis: S2[i,w] thus S2[i,w] ; ::_thesis: verum end; consider F1 being FinSequence of the carrier of RLS_Real such that A17: dom F1 = Seg n and A18: for i being Element of NAT st i in Seg n holds S2[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 H1( Nat) -> Element of the carrier of V = (p . $1) * (g /. $1); consider G being FinSequence of the carrier of V such that A20: len G = n and A21: for i being Nat st i in dom G holds G . i = H1(i) from FINSEQ_2:sch_1(); A22: dom G = Seg n by A20, FINSEQ_1:def_3; A23: for i being 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; ::_thesis: ( i in Seg n implies ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M ) ) assume A24: i in Seg n ; ::_thesis: ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M ) hence p . i > 0 by A7; ::_thesis: ( G . i = (p . i) * (g /. i) & g /. i in M ) thus G . i = (p . i) * (g /. i) by A21, A22, A24; ::_thesis: g /. i in M reconsider w = f . (y /. i) as Real by A10, A24; f . (y /. i) = R_EAL w ; then [(y /. i),w] in { [x,a] where x is Element of X, a is Element of REAL : f . x <= R_EAL a } ; hence g /. i in M by A13, A24; ::_thesis: verum end; M is convex by A2, Def6; then A25: Sum G in M by A3, A6, A14, A20, A23, Th7; A26: for i being Element of NAT st i in Seg n holds F1 . i = F . i proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies F1 . i = F . i ) assume A27: i in Seg n ; ::_thesis: F1 . i = F . i then F1 /. i = F1 . i by A17, PARTFUN1:def_6; hence F1 . i = F . i by A18, A27; ::_thesis: verum end; for i being Element of NAT st i in Seg n holds G . i = [(z . i),(F1 . i)] proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies G . i = [(z . i),(F1 . i)] ) assume A28: i in Seg n ; ::_thesis: G . i = [(z . i),(F1 . i)] then reconsider a = f . (y /. i) as 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 = (R_EAL (p . i)) * (f . (y /. i)) by A7, A28; then F . i = (p . i) * a by EXTREAL1:1; hence G . i = [(z . i),(F1 . i)] by A26, A28, A29; ::_thesis: verum 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 being Element of X, w being Element of REAL such that A30: [(Sum z),(Sum F)] = [x,w] and A31: f . x <= R_EAL w ; x = Sum z by A30, XTUPLE_0:1; hence f . (Sum z) <= Sum F by A30, A31, XTUPLE_0:1; ::_thesis: verum end; suppose ex i being Element of NAT st ( i in Seg n & f . (y /. i) = +infty ) ; ::_thesis: f . (Sum z) <= Sum F then consider i being Element of NAT such that A32: i in Seg n and A33: f . (y /. i) = +infty ; A34: F . i = (R_EAL (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 f . (Sum z) <= Sum F by XXREAL_0:4; ::_thesis: verum end; end; end; thus ( ( for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) implies f is convex ) ::_thesis: verum proof assume A36: for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ; ::_thesis: f is convex for x1, x2 being VECTOR of X for q being Real st 0 < q & q < 1 holds f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) proof set n = 2; let x1, x2 be VECTOR of X; ::_thesis: for q being Real st 0 < q & q < 1 holds f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) let q be Real; ::_thesis: ( 0 < q & q < 1 implies f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) ) assume that A37: 0 < q and A38: q < 1 ; ::_thesis: f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) reconsider F = <*((R_EAL q) * (f . x1)),((R_EAL (1 - q)) * (f . x2))*> 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 p = <*q,(1 - q)*> as FinSequence of REAL ; A39: for i being Element of NAT st i in Seg 2 holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg 2 implies ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) assume A40: i in Seg 2 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) percases ( i = 1 or i = 2 ) by A40, FINSEQ_1:2, TARSKI:def_2; supposeA41: i = 1 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) then A42: y /. i = x1 by FINSEQ_4:17; p . i = q by A41, FINSEQ_1:44; hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A37, A41, A42, FINSEQ_1:44; ::_thesis: verum end; supposeA43: i = 2 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) then A44: y /. i = x2 by FINSEQ_4:17; p . i = 1 - q by A43, FINSEQ_1:44; hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A38, A43, A44, FINSEQ_1:44, XREAL_1:50; ::_thesis: verum end; end; end; A45: len p = 2 by FINSEQ_1:44; A46: Sum p = q + (1 - q) by RVSUM_1:77 .= 1 ; A47: len z = 2 by FINSEQ_1:44; A48: Sum z = (q * x1) + ((1 - q) * x2) by RLVECT_1:45; A49: len y = 2 by FINSEQ_1:44; A50: len F = 2 by FINSEQ_1:44; Sum F = ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) by EXTREAL1:9; hence f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) by A36, A45, A50, A49, A47, A46, A39, A48; ::_thesis: verum end; hence f is convex by A1, Th4; ::_thesis: verum end; end; Lm14: for F being FinSequence of REAL ex s being Permutation of (dom F) ex n being Element of NAT st for i being Element of NAT st i in dom F holds ( i in Seg n iff F . (s . i) <> 0 ) proof deffunc H1( Nat) -> Nat = $1; let F be FinSequence of REAL ; ::_thesis: ex s being Permutation of (dom F) ex n being Element of NAT st for i being Element of NAT st i in dom F holds ( i in Seg n iff F . (s . i) <> 0 ) defpred S1[ Nat] means F . $1 <> 0 ; defpred S2[ Nat] means F . $1 = 0 ; set A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } ; set B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } ; set N = len F; A1: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= dom F from FRAENKEL:sch_17(); then A2: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= Seg (len F) by FINSEQ_1:def_3; reconsider A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } as finite set by A1; A3: rng (Sgm A) = A by A2, FINSEQ_1:def_13; A4: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= dom F from FRAENKEL:sch_17(); then A5: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= Seg (len F) by FINSEQ_1:def_3; reconsider B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } as finite set by A4; A6: rng (Sgm B) = B by A5, FINSEQ_1:def_13; for x being set holds not x in A /\ B proof let x be set ; ::_thesis: not x in A /\ B assume A7: x in A /\ B ; ::_thesis: contradiction then x in B by XBOOLE_0:def_4; then A8: ex i2 being 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 being Element of NAT st ( x = i1 & i1 in dom F & F . i1 <> 0 ) ; hence contradiction by A8; ::_thesis: verum 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: (Sgm A) ^ (Sgm B) 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 being set holds ( x in dom F iff ( x in A or x in B ) ) proof let x be set ; ::_thesis: ( x in dom F iff ( x in A or x in B ) ) thus ( not x in dom F or x in A or x in B ) ::_thesis: ( ( x in A or x in B ) implies x in dom F ) proof assume A13: x in dom F ; ::_thesis: ( x in A or x in B ) then reconsider x = x as Element of NAT ; percases ( F . x <> 0 or F . x = 0 ) ; suppose F . x <> 0 ; ::_thesis: ( x in A or x in B ) hence ( x in A or x in B ) by A13; ::_thesis: verum end; suppose F . x = 0 ; ::_thesis: ( x in A or x in B ) hence ( x in A or x in B ) by A13; ::_thesis: verum end; end; end; thus ( ( x in A or x in B ) implies x in dom F ) by A1, A4; ::_thesis: verum end; then A14: A \/ B = dom F by XBOOLE_0:def_3; then A15: rng ((Sgm A) ^ (Sgm B)) = dom F by A3, A6, FINSEQ_1:31; len (Sgm B) = card B by A5, FINSEQ_3:39; then len ((Sgm A) ^ (Sgm B)) = (card A) + (card B) by A12, FINSEQ_1:22 .= card (A \/ B) by A9, CARD_2:40 .= card (Seg (len F)) by A14, FINSEQ_1:def_3 ; then A16: len ((Sgm A) ^ (Sgm B)) = len F by FINSEQ_1:57; then A17: dom ((Sgm A) ^ (Sgm B)) = Seg (len F) by FINSEQ_1:def_3; A18: for x being Element of NAT st x in dom F & not x in Seg (len (Sgm A)) holds ex k being Element of NAT st ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) proof let x be Element of NAT ; ::_thesis: ( x in dom F & not x in Seg (len (Sgm A)) implies ex k being Element of NAT st ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) ) assume that A19: x in dom F and A20: not x in Seg (len (Sgm A)) ; ::_thesis: ex k being Element of NAT st ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) A21: x in Seg (len F) by A19, FINSEQ_1:def_3; ( not 1 <= x or not x <= len (Sgm A) ) by A20, FINSEQ_1:1; then (len (Sgm A)) + 1 <= x by A21, FINSEQ_1:1, INT_1:7; then A22: ((len (Sgm A)) + 1) - (len (Sgm A)) <= x - (len (Sgm A)) by XREAL_1:9; then reconsider k = x - (len (Sgm A)) as Element of NAT by INT_1:3; take k ; ::_thesis: ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) len ((Sgm A) ^ (Sgm B)) = (len (Sgm A)) + (len (Sgm B)) by FINSEQ_1:22; then A23: (len F) - (len (Sgm A)) = len (Sgm B) by A16; x <= len F 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 + (len (Sgm A)) ; hence ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) by A24, FINSEQ_1:def_7; ::_thesis: verum end; dom F = Seg (len F) by FINSEQ_1:def_3; then reconsider s = (Sgm A) ^ (Sgm B) 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 = s as Permutation of (dom F) by A11; take s ; ::_thesis: ex n being Element of NAT st for i being Element of NAT st i in dom F holds ( i in Seg n iff F . (s . i) <> 0 ) take len (Sgm A) ; ::_thesis: for i being Element of NAT st i in dom F holds ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) let i be Element of NAT ; ::_thesis: ( i in dom F implies ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) ) assume A25: i in dom F ; ::_thesis: ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) thus ( i in Seg (len (Sgm A)) implies F . (s . i) <> 0 ) ::_thesis: ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) ) proof assume i in Seg (len (Sgm A)) ; ::_thesis: F . (s . i) <> 0 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 being Element of NAT st ( s . i = j & j in dom F & F . j <> 0 ) ; hence F . (s . i) <> 0 ; ::_thesis: verum end; thus ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) ) ::_thesis: verum proof assume A27: F . (s . i) <> 0 ; ::_thesis: i in Seg (len (Sgm A)) assume not i in Seg (len (Sgm A)) ; ::_thesis: contradiction then ex k being Element of NAT st ( i = k + (len (Sgm A)) & 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 being Element of NAT st ( s . i = j & j in dom F & F . j = 0 ) by A6; hence contradiction by A27; ::_thesis: verum end; end; theorem :: CONVFUN1:9 for X being RealLinearSpace for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) proof let X be RealLinearSpace; ::_thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) ) assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) thus ( f is convex implies for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) ::_thesis: ( ( for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) implies f is convex ) proof assume A2: f is convex ; ::_thesis: for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let n be non empty Element of NAT ; ::_thesis: for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let p be FinSequence of REAL ; ::_thesis: for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let F be FinSequence of ExtREAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F ) 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 being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; ::_thesis: f . (Sum z) <= Sum F consider s being Permutation of (dom p), k being Element of NAT such that A9: for i being 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 being 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 ; ::_thesis: ( 1 <= i & i <= n - k implies ( i + k in Seg n & p . (s . (i + k)) = 0 ) ) assume that A15: 1 <= i and A16: i <= n - k ; ::_thesis: ( i + k in Seg n & p . (s . (i + k)) = 0 ) 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 ( i + k in Seg n & p . (s . (i + k)) = 0 ) by A9, A19, A17, A18, FINSEQ_1:1; ::_thesis: verum 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 percases ( k >= n or k < n ) ; suppose k >= n ; ::_thesis: Sum (z9 /^ k) = 0. X then z9 /^ k = <*> the carrier of X by A23, FINSEQ_5:32; hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; ::_thesis: verum end; supposeA25: k < n ; ::_thesis: Sum (z9 /^ k) = 0. X for w being set 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 set ; ::_thesis: ( w in rng (z9 /^ k) implies w in {(0. X)} ) assume w in rng (z9 /^ k) ; ::_thesis: w in {(0. X)} then consider i being set such that A26: i in dom (z9 /^ k) and A27: (z9 /^ k) . i = w by FUNCT_1:def_3; reconsider i = 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 w in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; then rng (z9 /^ k) c= {(0. X)} by TARSKI:def_3; hence Sum (z9 /^ k) = 0. X by Lm11; ::_thesis: verum end; 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 = min (k,n) 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 percases ( k >= n or k < n ) ; suppose k >= n ; ::_thesis: Sum (F9 /^ k) = 0. hence Sum (F9 /^ k) = 0. by A34, EXTREAL1:7, FINSEQ_5:32; ::_thesis: verum end; supposeA36: k < n ; ::_thesis: Sum (F9 /^ k) = 0. for w being set 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 set ; ::_thesis: ( w in rng (F9 /^ k) implies w in {0.} ) assume w in rng (F9 /^ k) ; ::_thesis: w in {0.} then consider i being set such that A37: i in dom (F9 /^ k) and A38: (F9 /^ k) . i = w by FUNCT_1:def_3; reconsider i = 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)) = (R_EAL 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 w in {0.} by TARSKI:def_1; ::_thesis: verum end; then rng (F9 /^ k) c= {0.} by TARSKI:def_3; hence Sum (F9 /^ k) = 0. by Lm9; ::_thesis: verum end; 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 being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (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 percases ( k >= n or k < n ) ; suppose k >= n ; ::_thesis: Sum (p9 /^ k) = 0 hence Sum (p9 /^ k) = 0 by A51, FINSEQ_5:32, RVSUM_1:72; ::_thesis: verum end; supposeA53: k < n ; ::_thesis: Sum (p9 /^ k) = 0 for w being set 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 set ; ::_thesis: ( w in rng (p9 /^ k) implies w in {0} ) assume w in rng (p9 /^ k) ; ::_thesis: w in {0} then consider i being set such that A54: i in dom (p9 /^ k) and A55: (p9 /^ k) . i = w by FUNCT_1:def_3; reconsider i = 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 w in {0} by TARSKI:def_1; ::_thesis: verum end; then rng (p9 /^ k) c= {0} by TARSKI:def_3; hence Sum (p9 /^ k) = 0 by Lm10; ::_thesis: verum end; 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, RLVECT_1:def_4; 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 = k9 as non empty Element of NAT by A61; A71: for i being 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 = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg k9 implies ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) ) assume A72: i in Seg k9 ; ::_thesis: ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) 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 ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) by A8, A77, A94, A91, A86, A93; ::_thesis: verum end; Sum (p9 | k) = 1 by A7, A33, A52, A70, RFINSEQ:9; hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; ::_thesis: verum end; thus ( ( for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) implies f is convex ) ::_thesis: verum proof assume A95: for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ; ::_thesis: f is convex for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F proof let n be non empty Element of NAT ; ::_thesis: for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let p be FinSequence of REAL ; ::_thesis: for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let F be FinSequence of ExtREAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F ) 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 being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; ::_thesis: f . (Sum z) <= Sum F for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A101; hence f . (Sum z) <= Sum F by A95, A96, A97, A98, A99, A100; ::_thesis: verum end; hence f is convex by A1, Th8; ::_thesis: verum end; end;