rfunct_3.miz



    begin

    reserve n,m for Nat,

r,r1,r2,s,t for Real,

x,y for set;

    definition

      let r be Real;

      :: RFUNCT_3:def1

      func max+ (r) -> Real equals ( max (r, 0 ));

      correctness ;

      :: RFUNCT_3:def2

      func max- (r) -> Real equals ( max (( - r), 0 ));

      correctness ;

    end

    theorem :: RFUNCT_3:1

    

     Th1: for r be Real holds r = (( max+ r) - ( max- r))

    proof

      let r be Real;

      now

        per cases ;

          case

           A1: 0 <= r;

          then ( max- r) = 0 by XXREAL_0:def 10;

          hence thesis by A1, XXREAL_0:def 10;

        end;

          case r < 0 ;

          then ( max+ r) = 0 & ( max- r) = ( - r) by XXREAL_0:def 10;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:2

    

     Th2: for r be Real holds |.r.| = (( max+ r) + ( max- r))

    proof

      let r be Real;

      now

        per cases ;

          case

           A1: 0 <= r;

          then ( max+ r) = r & ( max- r) = 0 by XXREAL_0:def 10;

          hence thesis by A1, ABSVALUE:def 1;

        end;

          case

           A2: r < 0 ;

          then ( max+ r) = 0 & ( max- r) = ( - r) by XXREAL_0:def 10;

          hence thesis by A2, ABSVALUE:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:3

    

     Th3: for r be Real holds (2 * ( max+ r)) = (r + |.r.|)

    proof

      let r be Real;

      

      thus (r + |.r.|) = ((( max+ r) - ( max- r)) + |.r.|) by Th1

      .= ((( max+ r) - ( max- r)) + (( max+ r) + ( max- r))) by Th2

      .= (2 * ( max+ r));

    end;

    theorem :: RFUNCT_3:4

    

     Th4: for r,s be Real st 0 <= r holds ( max+ (r * s)) = (r * ( max+ s))

    proof

      let r,s be Real;

      assume

       A1: 0 <= r;

      now

        per cases ;

          case

           A2: 0 <= s;

          then ( max+ (r * s)) = (r * s) by A1, XXREAL_0:def 10;

          hence thesis by A2, XXREAL_0:def 10;

        end;

          case

           A3: s < 0 ;

          then ( max+ s) = 0 by XXREAL_0:def 10;

          hence thesis by A1, A3, XXREAL_0:def 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:5

    

     Th5: for r,s be Real holds ( max+ (r + s)) <= (( max+ r) + ( max+ s))

    proof

      let r,s be Real;

      

       A1: 0 <= ( max (r, 0 )) & 0 <= ( max (s, 0 )) by XXREAL_0: 25;

      

       A2: r <= ( max (r, 0 )) & s <= ( max (s, 0 )) by XXREAL_0: 25;

      now

        per cases ;

          case 0 <= (r + s);

          then ( max+ (r + s)) = (r + s) by XXREAL_0:def 10;

          hence thesis by A2, XREAL_1: 7;

        end;

          case (r + s) < 0 ;

          then ( max+ (r + s)) = ( 0 + 0 ) by XXREAL_0:def 10;

          hence thesis by A1;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: for D be non empty set, f be FinSequence of D st ( len f) <= n holds (f | n) = f

    proof

      let D be non empty set, f be FinSequence of D;

      

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

      assume ( len f) <= n;

      then (f | n) = (f | ( Seg n)) & ( dom f) c= ( Seg n) by A1, FINSEQ_1: 5, FINSEQ_1:def 15;

      hence thesis by RELAT_1: 68;

    end;

    

     Lm2: for f be Function, x be set st not x in ( rng f) holds (f " {x}) = {}

    proof

      let f be Function, x be set;

      assume

       A1: not x in ( rng f);

      ( rng f) misses {x}

      proof

        set y = the Element of (( rng f) /\ {x});

        assume (( rng f) /\ {x}) <> {} ;

        then y in ( rng f) & y in {x} by XBOOLE_0:def 4;

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis by RELAT_1: 138;

    end;

    begin

    theorem :: RFUNCT_3:6

    

     Th6: for D be non empty set, F be PartFunc of D, REAL , r,s be Real st r <> 0 holds (F " {(s / r)}) = ((r (#) F) " {s})

    proof

      let D be non empty set, F be PartFunc of D, REAL , r,s be Real;

      assume

       A1: r <> 0 ;

      thus (F " {(s / r)}) c= ((r (#) F) " {s})

      proof

        let x be object;

        assume

         A2: x in (F " {(s / r)});

        then

        reconsider d = x as Element of D;

        d in ( dom F) by A2, FUNCT_1:def 7;

        then

         A3: d in ( dom (r (#) F)) by VALUED_1:def 5;

        (F . d) in {(s / r)} by A2, FUNCT_1:def 7;

        then (F . d) = (s / r) by TARSKI:def 1;

        then (r * (F . d)) = s by A1, XCMPLX_1: 87;

        then ((r (#) F) . d) = s by A3, VALUED_1:def 5;

        then ((r (#) F) . d) in {s} by TARSKI:def 1;

        hence thesis by A3, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A4: x in ((r (#) F) " {s});

      then

      reconsider d = x as Element of D;

      

       A5: d in ( dom (r (#) F)) by A4, FUNCT_1:def 7;

      ((r (#) F) . d) in {s} by A4, FUNCT_1:def 7;

      then ((r (#) F) . d) = s by TARSKI:def 1;

      then (r * (F . d)) = s by A5, VALUED_1:def 5;

      then (F . d) = (s / r) by A1, XCMPLX_1: 89;

      then

       A6: (F . d) in {(s / r)} by TARSKI:def 1;

      d in ( dom F) by A5, VALUED_1:def 5;

      hence thesis by A6, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:7

    

     Th7: for D be non empty set, F be PartFunc of D, REAL holds (( 0 (#) F) " { 0 }) = ( dom F)

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      thus (( 0 (#) F) " { 0 }) c= ( dom F)

      proof

        let x be object;

        assume

         A1: x in (( 0 (#) F) " { 0 });

        then

        reconsider d = x as Element of D;

        d in ( dom ( 0 (#) F)) by A1, FUNCT_1:def 7;

        hence thesis by VALUED_1:def 5;

      end;

      let x be object;

      assume

       A2: x in ( dom F);

      then

      reconsider d = x as Element of D;

      

       A3: d in ( dom ( 0 (#) F)) by A2, VALUED_1:def 5;

      

      then (( 0 (#) F) . d) = ( 0 * (F . d)) by VALUED_1:def 5

      .= 0 ;

      then (( 0 (#) F) . d) in { 0 } by TARSKI:def 1;

      hence thesis by A3, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:8

    

     Th8: for D be non empty set, F be PartFunc of D, REAL , r st 0 < r holds (( abs F) " {r}) = (F " {( - r), r})

    proof

      let D be non empty set, F be PartFunc of D, REAL , r;

      assume

       A1: 0 < r;

      

       A2: ( dom ( abs F)) = ( dom F) by VALUED_1:def 11;

      thus (( abs F) " {r}) c= (F " {( - r), r})

      proof

        let x be object;

        assume

         A3: x in (( abs F) " {r});

        then

        reconsider rr = x as Element of D;

        (( abs F) . rr) in {r} by A3, FUNCT_1:def 7;

        then |.(F . rr).| in {r} by VALUED_1: 18;

        then

         A4: |.(F . rr).| = r by TARSKI:def 1;

        

         A5: rr in ( dom ( abs F)) by A3, FUNCT_1:def 7;

        now

          per cases ;

            case 0 <= (F . rr);

            then (F . rr) = r by A4, ABSVALUE:def 1;

            then (F . rr) in {( - r), r} by TARSKI:def 2;

            hence thesis by A2, A5, FUNCT_1:def 7;

          end;

            case (F . rr) < 0 ;

            then ( - (F . rr)) = r by A4, ABSVALUE:def 1;

            then (F . rr) in {( - r), r} by TARSKI:def 2;

            hence thesis by A2, A5, FUNCT_1:def 7;

          end;

        end;

        hence thesis;

      end;

      let x be object;

      assume

       A6: x in (F " {( - r), r});

      then

      reconsider rr = x as Element of D;

      

       A7: rr in ( dom F) by A6, FUNCT_1:def 7;

      

       A8: (F . rr) in {( - r), r} by A6, FUNCT_1:def 7;

      now

        per cases by A8, TARSKI:def 2;

          case (F . rr) = ( - r);

          

          then r = |.( - (F . rr)).| by A1, ABSVALUE:def 1

          .= |.(F . rr).| by COMPLEX1: 52

          .= (( abs F) . rr) by VALUED_1: 18;

          then (( abs F) . rr) in {r} by TARSKI:def 1;

          hence thesis by A2, A7, FUNCT_1:def 7;

        end;

          case (F . rr) = r;

          

          then r = |.(F . rr).| by A1, ABSVALUE:def 1

          .= (( abs F) . rr) by VALUED_1: 18;

          then (( abs F) . rr) in {r} by TARSKI:def 1;

          hence thesis by A2, A7, FUNCT_1:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:9

    

     Th9: for D be non empty set, F be PartFunc of D, REAL holds (( abs F) " { 0 }) = (F " { 0 })

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom ( abs F)) = ( dom F) by VALUED_1:def 11;

      thus (( abs F) " { 0 }) c= (F " { 0 })

      proof

        let x be object;

        assume

         A2: x in (( abs F) " { 0 });

        then

        reconsider r = x as Element of D;

        (( abs F) . r) in { 0 } by A2, FUNCT_1:def 7;

        then |.(F . r).| in { 0 } by VALUED_1: 18;

        then |.(F . r).| = 0 by TARSKI:def 1;

        then (F . r) = 0 by ABSVALUE: 2;

        then

         A3: (F . r) in { 0 } by TARSKI:def 1;

        r in ( dom ( abs F)) by A2, FUNCT_1:def 7;

        hence thesis by A1, A3, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A4: x in (F " { 0 });

      then

      reconsider r = x as Element of D;

      (F . r) in { 0 } by A4, FUNCT_1:def 7;

      then (F . r) = 0 by TARSKI:def 1;

      then |.(F . r).| = 0 by ABSVALUE: 2;

      then (( abs F) . r) = 0 by VALUED_1: 18;

      then

       A5: (( abs F) . r) in { 0 } by TARSKI:def 1;

      r in ( dom F) by A4, FUNCT_1:def 7;

      hence thesis by A1, A5, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:10

    

     Th10: for D be non empty set, F be PartFunc of D, REAL , r st r < 0 holds (( abs F) " {r}) = {}

    proof

      let D be non empty set, F be PartFunc of D, REAL , r;

      assume

       A1: r < 0 ;

      set x = the Element of (( abs F) " {r});

      assume

       A2: (( abs F) " {r}) <> {} ;

      then

      reconsider x as Element of D by TARSKI:def 3;

      (( abs F) . x) in {r} by A2, FUNCT_1:def 7;

      then |.(F . x).| in {r} by VALUED_1: 18;

      then |.(F . x).| = r by TARSKI:def 1;

      hence contradiction by A1, COMPLEX1: 46;

    end;

    theorem :: RFUNCT_3:11

    

     Th11: for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL , r st r <> 0 holds (F,G) are_fiberwise_equipotent iff ((r (#) F),(r (#) G)) are_fiberwise_equipotent

    proof

      let D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL , r;

      assume

       A1: r <> 0 ;

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

      

       A2: ( rng (rr (#) F)) c= REAL & ( rng (rr (#) G)) c= REAL ;

      thus (F,G) are_fiberwise_equipotent implies ((r (#) F),(r (#) G)) are_fiberwise_equipotent

      proof

        assume

         A3: (F,G) are_fiberwise_equipotent ;

        now

          let x be Element of REAL ;

          ( Coim (F,(x / r))) = ( Coim ((r (#) F),x)) & ( Coim (G,(x / r))) = ( Coim ((r (#) G),x)) by A1, Th6;

          hence ( card ( Coim ((r (#) F),x))) = ( card ( Coim ((r (#) G),x))) by A3, CLASSES1:def 10;

        end;

        hence thesis by A2, CLASSES1: 79;

      end;

      assume

       A4: ((r (#) F),(r (#) G)) are_fiberwise_equipotent ;

       A5:

      now

        let x be Element of REAL ;

        

         A6: (G " {((r * x) / r)}) = ( Coim ((r (#) G),(r * x))) by A1, Th6;

        ((r * x) / r) = x & (F " {((r * x) / r)}) = ( Coim ((r (#) F),(r * x))) by A1, Th6, XCMPLX_1: 89;

        hence ( card ( Coim (F,x))) = ( card ( Coim (G,x))) by A4, A6, CLASSES1:def 10;

      end;

      ( rng F) c= REAL & ( rng G) c= REAL ;

      hence thesis by A5, CLASSES1: 79;

    end;

    theorem :: RFUNCT_3:12

    for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL holds (F,G) are_fiberwise_equipotent iff (( - F),( - G)) are_fiberwise_equipotent by Th11;

    theorem :: RFUNCT_3:13

    for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL st (F,G) are_fiberwise_equipotent holds (( abs F),( abs G)) are_fiberwise_equipotent

    proof

      let D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL ;

      assume

       A1: (F,G) are_fiberwise_equipotent ;

       A2:

      now

        let r be Element of REAL ;

        now

          per cases ;

            case 0 < r;

            then (( abs F) " {r}) = (F " {( - r), r}) & (( abs G) " {r}) = (G " {( - r), r}) by Th8;

            hence ( card (( abs F) " {r})) = ( card (( abs G) " {r})) by A1, CLASSES1: 78;

          end;

            case 0 = r;

            then (( abs F) " {r}) = (F " {r}) & (( abs G) " {r}) = (G " {r}) by Th9;

            hence ( card (( abs F) " {r})) = ( card (( abs G) " {r})) by A1, CLASSES1: 78;

          end;

            case

             A3: r < 0 ;

            then (( abs F) " {r}) = {} by Th10;

            hence ( card (( abs F) " {r})) = ( card (( abs G) " {r})) by A3, Th10;

          end;

        end;

        hence ( card ( Coim (( abs F),r))) = ( card ( Coim (( abs G),r)));

      end;

      ( rng ( abs F)) c= REAL & ( rng ( abs G)) c= REAL ;

      hence thesis by A2, CLASSES1: 79;

    end;

    definition

      let X,Y be set;

      :: RFUNCT_3:def3

      mode PartFunc-set of X,Y -> set means

      : Def3: for x be Element of it holds x is PartFunc of X, Y;

      existence

      proof

        reconsider h = {} as PartFunc of X, Y by RELSET_1: 12;

        take {h};

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let X,Y be set;

      cluster non empty for PartFunc-set of X, Y;

      existence

      proof

        reconsider h = {} as PartFunc of X, Y by RELSET_1: 12;

         {h} is PartFunc-set of X, Y

        proof

          let x be Element of {h};

          thus thesis by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      let X,Y be set;

      mode PFUNC_DOMAIN of X,Y is non empty PartFunc-set of X, Y;

    end

    definition

      let X,Y be set;

      :: original: PFuncs

      redefine

      func PFuncs (X,Y) -> PartFunc-set of X, Y ;

      coherence

      proof

        for x be Element of ( PFuncs (X,Y)) holds x is PartFunc of X, Y by PARTFUN1: 47;

        hence thesis by Def3;

      end;

      let P be non empty PartFunc-set of X, Y;

      :: original: Element

      redefine

      mode Element of P -> PartFunc of X, Y ;

      coherence by Def3;

    end

    definition

      let D,C be non empty set, X be Subset of D, c be Element of C;

      :: original: -->

      redefine

      func X --> c -> Element of ( PFuncs (D,C)) ;

      coherence

      proof

        (X --> c) is PartFunc of D, C;

        hence thesis by PARTFUN1: 45;

      end;

    end

    registration

      let D be non empty set, E be real-membered set;

      cluster -> real-valued for Element of ( PFuncs (D,E));

      coherence ;

    end

    definition

      let D be non empty set, E be real-membered set, F1,F2 be Element of ( PFuncs (D,E));

      :: original: +

      redefine

      func F1 + F2 -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 + F2) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: -

      redefine

      func F1 - F2 -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 - F2) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: (#)

      redefine

      func F1 (#) F2 -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 (#) F2) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: /

      redefine

      func F1 / F2 -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F1, F2 as PartFunc of D, E;

        (F1 / F2) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    definition

      let D be non empty set, E be real-membered set, F be Element of ( PFuncs (D,E));

      :: original: abs

      redefine

      func abs (F) -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F as PartFunc of D, E;

        ( abs F) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: -

      redefine

      func - F -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F as PartFunc of D, E;

        ( - F) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

      :: original: ^

      redefine

      func F ^ -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F as PartFunc of D, E;

        (F ^ ) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    definition

      let D be non empty set, E be real-membered set, F be Element of ( PFuncs (D,E)), r be Real;

      :: original: (#)

      redefine

      func r (#) F -> Element of ( PFuncs (D, REAL )) ;

      coherence

      proof

        reconsider F as PartFunc of D, E;

        (r (#) F) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    definition

      let D be non empty set;

      :: RFUNCT_3:def4

      func addpfunc (D) -> BinOp of ( PFuncs (D, REAL )) means

      : Def4: for F1,F2 be Element of ( PFuncs (D, REAL )) holds (it . (F1,F2)) = (F1 + F2);

      existence

      proof

        deffunc O( Element of ( PFuncs (D, REAL )), Element of ( PFuncs (D, REAL ))) = ($1 + $2);

        ex o be BinOp of ( PFuncs (D, REAL )) st for a,b be Element of ( PFuncs (D, REAL )) holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( PFuncs (D, REAL ));

        assume that

         A1: for f1,f2 be Element of ( PFuncs (D, REAL )) holds (o1 . (f1,f2)) = (f1 + f2) and

         A2: for f1,f2 be Element of ( PFuncs (D, REAL )) holds (o2 . (f1,f2)) = (f1 + f2);

        now

          let f1,f2 be Element of ( PFuncs (D, REAL ));

          (o1 . (f1,f2)) = (f1 + f2) by A1;

          hence (o1 . (f1,f2)) = (o2 . (f1,f2)) by A2;

        end;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_3:14

    

     Th14: for D be non empty set holds ( addpfunc D) is commutative

    proof

      let D be non empty set;

      let F1,F2 be Element of ( PFuncs (D, REAL ));

      set o = ( addpfunc D);

      

      thus (o . (F1,F2)) = (F2 + F1) by Def4

      .= (o . (F2,F1)) by Def4;

    end;

    theorem :: RFUNCT_3:15

    

     Th15: for D be non empty set holds ( addpfunc D) is associative

    proof

      let D be non empty set;

      let F1,F2,F3 be Element of ( PFuncs (D, REAL ));

      set o = ( addpfunc D);

      

      thus (o . (F1,(o . (F2,F3)))) = (o . (F1,(F2 + F3))) by Def4

      .= (F1 + (F2 + F3)) by Def4

      .= ((F1 + F2) + F3) by RFUNCT_1: 8

      .= ((o . (F1,F2)) + F3) by Def4

      .= (o . ((o . (F1,F2)),F3)) by Def4;

    end;

    theorem :: RFUNCT_3:16

    

     Th16: for D be non empty set holds (( [#] D) --> 0 qua Real) is_a_unity_wrt ( addpfunc D)

    proof

      let D be non empty set;

      set F = (( [#] D) --> ( In ( 0 , REAL )));

      

       A1: ( dom F) = D by FUNCOP_1: 13;

       A2:

      now

        let G be Element of ( PFuncs (D, REAL ));

         A3:

        now

          let d be Element of D;

          assume d in ( dom (G + F));

          

          hence ((G + F) . d) = ((G . d) + (F . d)) by VALUED_1:def 1

          .= ((G . d) + 0 ) by FUNCOP_1: 7

          .= (G . d);

        end;

        (( dom G) /\ D) = ( dom G) by XBOOLE_1: 28;

        then ( dom (G + F)) = ( dom G) by A1, VALUED_1:def 1;

        then (G + F) = G by A3, PARTFUN1: 5;

        hence (( addpfunc D) . (G,F)) = G by Def4;

      end;

      ( addpfunc D) is commutative by Th14;

      hence thesis by A2, BINOP_1: 5;

    end;

    theorem :: RFUNCT_3:17

    

     Th17: for D be non empty set holds ( the_unity_wrt ( addpfunc D)) = (( [#] D) --> 0 qua Real)

    proof

      let D be non empty set;

      (( [#] D) --> ( In ( 0 , REAL ))) is_a_unity_wrt ( addpfunc D) by Th16;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: RFUNCT_3:18

    

     Th18: for D be non empty set holds ( addpfunc D) is having_a_unity

    proof

      let D be non empty set;

      take (( [#] D) --> ( In ( 0 , REAL )));

      thus thesis by Th16;

    end;

    definition

      let D be non empty set, f be FinSequence of ( PFuncs (D, REAL ));

      :: RFUNCT_3:def5

      func Sum (f) -> Element of ( PFuncs (D, REAL )) equals (( addpfunc D) $$ f);

      correctness ;

    end

    theorem :: RFUNCT_3:19

    

     Th19: for D be non empty set holds ( Sum ( <*> ( PFuncs (D, REAL )))) = (( [#] D) --> 0 qua Real)

    proof

      let D be non empty set;

      set o = ( addpfunc D), o0 = (( [#] D) --> 0 qua Real);

      ( the_unity_wrt o) = o0 by Th17;

      hence thesis by Th18, FINSOP_1: 10;

    end;

    theorem :: RFUNCT_3:20

    

     Th20: for D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), G be Element of ( PFuncs (D, REAL )) holds ( Sum (f ^ <*G*>)) = (( Sum f) + G)

    proof

      let D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), G be Element of ( PFuncs (D, REAL ));

      set o = ( addpfunc D);

      

      thus ( Sum (f ^ <*G*>)) = (o . ((o $$ f),G)) by Th18, FINSOP_1: 4

      .= (( Sum f) + G) by Def4;

    end;

    theorem :: RFUNCT_3:21

    

     Th21: for D be non empty set, f1,f2 be FinSequence of ( PFuncs (D, REAL )) holds ( Sum (f1 ^ f2)) = (( Sum f1) + ( Sum f2))

    proof

      let D be non empty set, f1,f2 be FinSequence of ( PFuncs (D, REAL ));

      set o = ( addpfunc D);

      o is associative by Th15;

      

      hence ( Sum (f1 ^ f2)) = (( addpfunc D) . (( Sum f1),( Sum f2))) by Th18, FINSOP_1: 5

      .= (( Sum f1) + ( Sum f2)) by Def4;

    end;

    theorem :: RFUNCT_3:22

    for D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), G be Element of ( PFuncs (D, REAL )) holds ( Sum ( <*G*> ^ f)) = (G + ( Sum f))

    proof

      let D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), G be Element of ( PFuncs (D, REAL ));

      

      thus ( Sum ( <*G*> ^ f)) = (( Sum <*G*>) + ( Sum f)) by Th21

      .= (G + ( Sum f)) by FINSOP_1: 11;

    end;

    theorem :: RFUNCT_3:23

    

     Th23: for D be non empty set, G1,G2 be Element of ( PFuncs (D, REAL )) holds ( Sum <*G1, G2*>) = (G1 + G2)

    proof

      let D be non empty set, G1,G2 be Element of ( PFuncs (D, REAL ));

      

      thus ( Sum <*G1, G2*>) = ( Sum ( <*G1*> ^ <*G2*>)) by FINSEQ_1:def 9

      .= (( Sum <*G1*>) + G2) by Th20

      .= (G1 + G2) by FINSOP_1: 11;

    end;

    theorem :: RFUNCT_3:24

    for D be non empty set, G1,G2,G3 be Element of ( PFuncs (D, REAL )) holds ( Sum <*G1, G2, G3*>) = ((G1 + G2) + G3)

    proof

      let D be non empty set, G1,G2,G3 be Element of ( PFuncs (D, REAL ));

      

      thus ( Sum <*G1, G2, G3*>) = ( Sum ( <*G1, G2*> ^ <*G3*>)) by FINSEQ_1: 43

      .= (( Sum <*G1, G2*>) + G3) by Th20

      .= ((G1 + G2) + G3) by Th23;

    end;

    theorem :: RFUNCT_3:25

    for D be non empty set, f,g be FinSequence of ( PFuncs (D, REAL )) st (f,g) are_fiberwise_equipotent holds ( Sum f) = ( Sum g)

    proof

      let D be non empty set;

      defpred P[ Nat] means for f,g be FinSequence of ( PFuncs (D, REAL )) st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds ( Sum f) = ( Sum g);

      let f,g be FinSequence of ( PFuncs (D, REAL ));

      assume

       A1: (f,g) are_fiberwise_equipotent ;

      

       A2: ( len f) = ( len f);

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let f,g be FinSequence of ( PFuncs (D, REAL ));

        assume that

         A5: (f,g) are_fiberwise_equipotent and

         A6: ( len f) = (n + 1);

        ( 0 + 1) <= (n + 1) by NAT_1: 13;

        then

         A7: (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then

        reconsider a = (f . (n + 1)) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

        ( rng f) = ( rng g) by A5, CLASSES1: 75;

        then a in ( rng g) by A7, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A8: m in ( dom g) and

         A9: (g . m) = a by FINSEQ_2: 10;

        

         A10: g = ((g | m) ^ (g /^ m)) by RFINSEQ: 8;

        set gg = (g /^ m), gm = (g | m);

        m <= ( len g) by A8, FINSEQ_3: 25;

        then

         A11: ( len gm) = m by FINSEQ_1: 59;

        set fn = (f | n);

        

         A12: f = (fn ^ <*a*>) by A6, RFINSEQ: 7;

        

         A13: 1 <= m by A8, FINSEQ_3: 25;

        then ( max ( 0 ,(m - 1))) = (m - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (m - 1) as Element of NAT by FINSEQ_2: 5;

        

         A14: m = (m1 + 1);

        then m1 <= m by NAT_1: 11;

        then

         A15: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5;

        m in ( Seg m) by A13, FINSEQ_1: 1;

        then (gm . m) = a by A8, A9, RFINSEQ: 6;

        then

         A16: gm = ((gm | m1) ^ <*a*>) by A11, A14, RFINSEQ: 7;

        

         A17: (gm | m1) = (gm | ( Seg m1)) by FINSEQ_1:def 15

        .= ((g | ( Seg m)) | ( Seg m1)) by FINSEQ_1:def 15

        .= (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | ( Seg m1)) by A15, XBOOLE_1: 28

        .= (g | m1) by FINSEQ_1:def 15;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A5, CLASSES1:def 10;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A10, A16, A17, A12, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A18: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent by CLASSES1:def 10;

        ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        then ( Sum fn) = ( Sum ((g | m1) ^ gg)) by A4, A18;

        

        hence ( Sum f) = (( Sum ((g | m1) ^ gg)) + ( Sum <*a*>)) by A12, Th21

        .= ((( Sum (g | m1)) + ( Sum gg)) + ( Sum <*a*>)) by Th21

        .= ((( Sum (g | m1)) + ( Sum <*a*>)) + ( Sum gg)) by RFUNCT_1: 8

        .= (( Sum gm) + ( Sum gg)) by A16, A17, Th21

        .= ( Sum g) by A10, Th21;

      end;

      

       A19: P[ 0 ]

      proof

        let f,g be FinSequence of ( PFuncs (D, REAL ));

        assume (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A20: ( len g) = 0 & f = ( <*> ( PFuncs (D, REAL ))) by RFINSEQ: 3;

        then g = ( <*> ( PFuncs (D, REAL )));

        hence thesis by A20;

      end;

      for n holds P[n] from NAT_1:sch 2( A19, A3);

      hence thesis by A1, A2;

    end;

    definition

      let D be non empty set, f be FinSequence;

      :: RFUNCT_3:def6

      func CHI (f,D) -> FinSequence of ( PFuncs (D, REAL )) means

      : Def6: ( len it ) = ( len f) & for n st n in ( dom it ) holds (it . n) = ( chi ((f . n),D));

      existence

      proof

        deffunc F( Nat) = ( chi ((f . $1),D));

        consider p be FinSequence such that

         A1: ( len p) = ( len f) and

         A2: for n be Nat st n in ( dom p) holds (p . n) = F(n) from FINSEQ_1:sch 2;

        ( rng p) c= ( PFuncs (D, REAL ))

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider n be Nat such that

           A3: n in ( dom p) & (p . n) = x by FINSEQ_2: 10;

          x = ( chi ((f . n),D)) by A2, A3;

          hence thesis by PARTFUN1: 45;

        end;

        then

        reconsider p as FinSequence of ( PFuncs (D, REAL )) by FINSEQ_1:def 4;

        take p;

        thus ( len p) = ( len f) by A1;

        let n;

        assume n in ( dom p);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of ( PFuncs (D, REAL ));

        assume that

         A4: ( len p1) = ( len f) and

         A5: for n st n in ( dom p1) holds (p1 . n) = ( chi ((f . n),D)) and

         A6: ( len p2) = ( len f) and

         A7: for n st n in ( dom p2) holds (p2 . n) = ( chi ((f . n),D));

        

         A8: ( dom p1) = ( Seg ( len p1)) & ( dom p2) = ( Seg ( len p2)) by FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A9: n in ( dom p1);

          then (p1 . n) = ( chi ((f . n),D)) by A5;

          hence (p1 . n) = (p2 . n) by A4, A6, A7, A8, A9;

        end;

        hence thesis by A4, A6, FINSEQ_2: 9;

      end;

    end

    definition

      let D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), R be FinSequence of REAL ;

      :: RFUNCT_3:def7

      func R (#) f -> FinSequence of ( PFuncs (D, REAL )) means

      : Def7: ( len it ) = ( min (( len R),( len f))) & for n st n in ( dom it ) holds for F be PartFunc of D, REAL , r st r = (R . n) & F = (f . n) holds (it . n) = (r (#) F);

      existence

      proof

        defpred P[ Nat, set] means for F be PartFunc of D, REAL , r st r = (R . $1) & F = (f . $1) holds $2 = (r (#) F);

        set m = ( min (( len R),( len f)));

        

         A1: m <= ( len f) by XXREAL_0: 17;

        

         A2: for n be Nat st n in ( Seg m) holds ex x be Element of ( PFuncs (D, REAL )) st P[n, x]

        proof

          let n be Nat;

          reconsider r = (R . n) as Real;

          assume

           A3: n in ( Seg m);

          then n <= m by FINSEQ_1: 1;

          then

           A4: n <= ( len f) by A1, XXREAL_0: 2;

          1 <= n by A3, FINSEQ_1: 1;

          then n in ( dom f) by A4, FINSEQ_3: 25;

          then

          reconsider F = (f . n) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

          reconsider a = (r (#) F) as Element of ( PFuncs (D, REAL ));

          take a;

          thus thesis;

        end;

        consider p be FinSequence of ( PFuncs (D, REAL )) such that

         A5: ( dom p) = ( Seg m) & for n be Nat st n in ( Seg m) holds P[n, (p . n)] from FINSEQ_1:sch 5( A2);

        take p;

        thus ( len p) = m by A5, FINSEQ_1:def 3;

        let n;

        assume n in ( dom p);

        hence thesis by A5;

      end;

      uniqueness

      proof

        set m = ( min (( len R),( len f)));

        let p1,p2 be FinSequence of ( PFuncs (D, REAL ));

        assume that

         A6: ( len p1) = m and

         A7: for n st n in ( dom p1) holds for F be PartFunc of D, REAL , r st r = (R . n) & F = (f . n) holds (p1 . n) = (r (#) F) and

         A8: ( len p2) = m and

         A9: for n st n in ( dom p2) holds for F be PartFunc of D, REAL , r st r = (R . n) & F = (f . n) holds (p2 . n) = (r (#) F);

        

         A10: ( dom p1) = ( Seg m) by A6, FINSEQ_1:def 3;

        

         A11: ( dom p1) = ( Seg ( len p1)) & ( dom p2) = ( Seg ( len p2)) by FINSEQ_1:def 3;

        

         A12: m <= ( len f) by XXREAL_0: 17;

        now

          let n be Nat;

          reconsider r = (R . n) as Real;

          assume

           A13: n in ( dom p1);

          then n <= m by A10, FINSEQ_1: 1;

          then

           A14: n <= ( len f) by A12, XXREAL_0: 2;

          1 <= n by A10, A13, FINSEQ_1: 1;

          then n in ( dom f) by A14, FINSEQ_3: 25;

          then

          reconsider F = (f . n) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

          (p1 . n) = (r (#) F) by A7, A13;

          hence (p1 . n) = (p2 . n) by A6, A8, A9, A11, A13;

        end;

        hence thesis by A6, A8, FINSEQ_2: 9;

      end;

    end

    definition

      let D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), d be Element of D;

      :: RFUNCT_3:def8

      func f # d -> FinSequence of REAL means

      : Def8: ( len it ) = ( len f) & for n be Element of NAT st n in ( dom it ) holds (it . n) = ((f . n) . d);

      existence

      proof

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

        

         A1: for n be Nat st n in ( Seg ( len f)) holds ex x be Element of REAL st P[n, x]

        proof

          let n be Nat;

          assume n in ( Seg ( len f));

          then n in ( dom f) by FINSEQ_1:def 3;

          then

          reconsider G = (f . n) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

          take (G . d);

          thus thesis by XREAL_0:def 1;

        end;

        consider p be FinSequence of REAL such that

         A2: ( dom p) = ( Seg ( len f)) and

         A3: for n be Nat st n in ( Seg ( len f)) holds P[n, (p . n)] from FINSEQ_1:sch 5( A1);

        take p;

        thus ( len p) = ( len f) by A2, FINSEQ_1:def 3;

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL ;

        assume that

         A4: ( len p1) = ( len f) and

         A5: for n be Element of NAT st n in ( dom p1) holds (p1 . n) = ((f . n) . d) and

         A6: ( len p2) = ( len f) and

         A7: for n be Element of NAT st n in ( dom p2) holds (p2 . n) = ((f . n) . d);

        

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

        

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

        now

          let n be Nat;

          assume

           A10: n in ( dom p1);

          then (p1 . n) = ((f . n) . d) by A5;

          hence (p1 . n) = (p2 . n) by A4, A6, A7, A8, A9, A10;

        end;

        hence thesis by A4, A6, FINSEQ_2: 9;

      end;

    end

    definition

      let D,C be non empty set, f be FinSequence of ( PFuncs (D,C)), d be Element of D;

      :: RFUNCT_3:def9

      pred d is_common_for_dom f means for n be Nat st n in ( dom f) holds d in ( dom (f . n));

    end

    theorem :: RFUNCT_3:26

    

     Th26: for D,C be non empty set, f be FinSequence of ( PFuncs (D,C)), d be Element of D, n be Nat st d is_common_for_dom f & n <> 0 holds d is_common_for_dom (f | n)

    proof

      let D1,D2 be non empty set, f be FinSequence of ( PFuncs (D1,D2)), d1 be Element of D1, n;

      assume that

       A1: d1 is_common_for_dom f and

       A2: n <> 0 ;

      let m;

      assume

       A3: m in ( dom (f | n));

      set G = ((f | n) . m);

      per cases ;

        suppose n >= ( len f);

        then (f | n) = f by Lm1;

        hence thesis by A1, A3;

      end;

        suppose

         A4: n < ( len f);

        ( 0 + 1) <= n by A2, NAT_1: 13;

        then

         A5: n in ( dom f) by A4, FINSEQ_3: 25;

        ( dom (f | n)) = ( Seg ( len (f | n))) & ( len (f | n)) = n by A4, FINSEQ_1: 59, FINSEQ_1:def 3;

        then G = (f . m) & m in ( dom f) by A3, A5, RFINSEQ: 6;

        hence thesis by A1;

      end;

    end;

    theorem :: RFUNCT_3:27

    for D,C be non empty set, f be FinSequence of ( PFuncs (D,C)), d be Element of D, n be Nat st d is_common_for_dom f holds d is_common_for_dom (f /^ n)

    proof

      let D1,D2 be non empty set, f be FinSequence of ( PFuncs (D1,D2)), d1 be Element of D1, n;

      assume

       A1: d1 is_common_for_dom f;

      let m;

      set fn = (f /^ n);

      assume

       A2: m in ( dom fn);

      set G = (fn . m);

      now

        per cases ;

          case ( len f) < n;

          hence thesis by A2, RELAT_1: 38, RFINSEQ:def 1;

        end;

          case

           A3: n <= ( len f);

          1 <= m & m <= (m + n) by A2, FINSEQ_3: 25, NAT_1: 11;

          then

           A4: 1 <= (m + n) by XXREAL_0: 2;

          

           A5: m <= ( len fn) by A2, FINSEQ_3: 25;

          ( len fn) = (( len f) - n) by A3, RFINSEQ:def 1;

          then (m + n) <= ( len f) by A5, XREAL_1: 19;

          then

           A6: (m + n) in ( dom f) by A4, FINSEQ_3: 25;

          G = (f . (m + n)) by A2, A3, RFINSEQ:def 1;

          hence thesis by A1, A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:28

    

     Th28: for D be non empty set, d be Element of D, f be FinSequence of ( PFuncs (D, REAL )) st ( len f) <> 0 holds d is_common_for_dom f iff d in ( dom ( Sum f))

    proof

      let D be non empty set, d be Element of D;

      defpred P[ Nat] means for f be FinSequence of ( PFuncs (D, REAL )) st ( len f) = $1 & ( len f) <> 0 holds d is_common_for_dom f iff d in ( dom ( Sum f));

      let f be FinSequence of ( PFuncs (D, REAL ));

      assume

       A1: ( len f) <> 0 ;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A3: P[n];

        let f be FinSequence of ( PFuncs (D, REAL ));

        assume that

         A4: ( len f) = (n + 1) and ( len f) <> 0 ;

        

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

        now

          per cases ;

            case

             A6: n = 0 ;

            then

             A7: 1 in ( dom f) by A4, FINSEQ_3: 25;

            then

            reconsider G = (f . 1) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

            f = <*G*> by A4, A6, FINSEQ_1: 40;

            then

             A8: ( Sum f) = G by FINSOP_1: 11;

            hence d is_common_for_dom f implies d in ( dom ( Sum f)) by A7;

            assume d in ( dom ( Sum f));

            then for m st m in ( dom f) holds d in ( dom (f . m)) by A4, A5, A6, A8, FINSEQ_1: 2, TARSKI:def 1;

            hence d is_common_for_dom f;

          end;

            case

             A9: n <> 0 ;

            

             A10: n <= (n + 1) by NAT_1: 11;

            ( 0 + 1) <= n by A9, NAT_1: 13;

            then

             A11: n in ( dom f) by A4, A10, FINSEQ_3: 25;

            ( 0 + 1) <= (n + 1) by NAT_1: 13;

            then

             A12: (n + 1) in ( dom f) by A4, FINSEQ_3: 25;

            then

            reconsider G = (f . (n + 1)) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

            set fn = (f | n);

            

             A13: ( len fn) = n by A4, FINSEQ_1: 59, NAT_1: 11;

            f = (fn ^ <*G*>) by A4, RFINSEQ: 7;

            then

             A14: ( Sum f) = (( Sum fn) + G) by Th20;

            thus d is_common_for_dom f implies d in ( dom ( Sum f))

            proof

              assume

               A15: d is_common_for_dom f;

              then d is_common_for_dom fn by A9, Th26;

              then

               A16: d in ( dom ( Sum fn)) by A3, A9, A13;

              d in ( dom G) by A12, A15;

              then d in (( dom ( Sum fn)) /\ ( dom G)) by A16, XBOOLE_0:def 4;

              hence thesis by A14, VALUED_1:def 1;

            end;

            assume d in ( dom ( Sum f));

            then

             A17: d in (( dom ( Sum fn)) /\ ( dom G)) by A14, VALUED_1:def 1;

            then d in ( dom ( Sum fn)) by XBOOLE_0:def 4;

            then

             A18: d is_common_for_dom fn by A3, A9, A13;

            now

              let m;

              assume that

               A19: m in ( dom f);

              set F = (f . m);

              

               A20: m <= ( len f) by A19, FINSEQ_3: 25;

              

               A21: 1 <= m by A19, FINSEQ_3: 25;

              now

                per cases ;

                  case m = ( len f);

                  hence d in ( dom F) by A4, A17, XBOOLE_0:def 4;

                end;

                  case m <> ( len f);

                  then m < ( len f) by A20, XXREAL_0: 1;

                  then m <= n by A4, NAT_1: 13;

                  then

                   A22: m in ( Seg n) by A21, FINSEQ_1: 1;

                  then ( dom fn) = ( Seg ( len fn)) & F = (fn . m) by A11, FINSEQ_1:def 3, RFINSEQ: 6;

                  hence d in ( dom F) by A13, A18, A22;

                end;

              end;

              hence d in ( dom F);

            end;

            hence d is_common_for_dom f;

          end;

        end;

        hence thesis;

      end;

      

       A23: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A23, A2);

      hence thesis by A1;

    end;

    theorem :: RFUNCT_3:29

    

     Th29: for D be non empty set, f be FinSequence of ( PFuncs (D, REAL )), d be Element of D, n be Nat holds ((f | n) # d) = ((f # d) | n)

    proof

      let D1 be non empty set, f be FinSequence of ( PFuncs (D1, REAL )), d1 be Element of D1, n be Nat;

      

       A1: ( len (f # d1)) = ( len f) by Def8;

      

       A2: ( len ((f | n) # d1)) = ( len (f | n)) by Def8;

      now

        per cases ;

          case

           A3: ( len f) <= n;

          then (f | n) = f by Lm1;

          hence thesis by A1, A3, Lm1;

        end;

          case

           A4: n < ( len f);

          then

           A5: ( len (f | n)) = n by FINSEQ_1: 59;

          

           A6: ( len ((f # d1) | n)) = n by A1, A4, FINSEQ_1: 59;

          

           A7: ( dom f) = ( Seg ( len f)) & ( dom (f # d1)) = ( Seg ( len (f # d1))) by FINSEQ_1:def 3;

          

           A8: ( dom ((f | n) # d1)) = ( Seg ( len ((f | n) # d1))) by FINSEQ_1:def 3;

          now

            per cases ;

              case

               A9: n = 0 ;

              thus thesis by A2, A9;

            end;

              case

               A10: n <> 0 ;

              

               A11: ( dom ((f # d1) | n)) = ( Seg ( len (f | n))) by A5, A6, FINSEQ_1:def 3;

              ( 0 + 1) <= n by A10, NAT_1: 13;

              then

               A12: n in ( dom f) by A4, FINSEQ_3: 25;

              now

                let m be Nat;

                assume

                 A13: m in ( dom ((f # d1) | n));

                then

                 A14: m in ( dom (f # d1)) by A1, A5, A7, A12, A11, RFINSEQ: 6;

                then

                reconsider G = (f . m) as Element of ( PFuncs (D1, REAL )) by A1, A7, FINSEQ_2: 11;

                (((f # d1) | n) . m) = ((f # d1) . m) by A1, A5, A7, A12, A11, A13, RFINSEQ: 6;

                then

                 A15: (((f # d1) | n) . m) = (G . d1) by A14, Def8;

                ((f | n) . m) = G by A5, A12, A11, A13, RFINSEQ: 6;

                hence (((f # d1) | n) . m) = (((f | n) # d1) . m) by A2, A8, A11, A13, A15, Def8;

              end;

              hence thesis by A2, A5, A6, FINSEQ_2: 9;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:30

    

     Th30: for D be non empty set, f be FinSequence, d be Element of D holds d is_common_for_dom ( CHI (f,D))

    proof

      let D be non empty set, f be FinSequence, d be Element of D;

      let n;

      assume n in ( dom ( CHI (f,D)));

      then (( CHI (f,D)) . n) = ( chi ((f . n),D)) by Def6;

      then ( dom (( CHI (f,D)) . n)) = D by RFUNCT_1: 61;

      hence thesis;

    end;

    theorem :: RFUNCT_3:31

    

     Th31: for D be non empty set, d be Element of D, f be FinSequence of ( PFuncs (D, REAL )), R be FinSequence of REAL st d is_common_for_dom f holds d is_common_for_dom (R (#) f)

    proof

      let D be non empty set, d be Element of D, f be FinSequence of ( PFuncs (D, REAL )), R be FinSequence of REAL ;

      assume

       A1: d is_common_for_dom f;

      set m = ( min (( len R),( len f)));

      let n;

      assume

       A2: n in ( dom (R (#) f));

      set G = ((R (#) f) . n);

      ( len (R (#) f)) = m by Def7;

      then m <= ( len f) & n <= m by A2, FINSEQ_3: 25, XXREAL_0: 17;

      then

       A3: n <= ( len f) by XXREAL_0: 2;

      1 <= n by A2, FINSEQ_3: 25;

      then

       A4: n in ( dom f) by A3, FINSEQ_3: 25;

      then

      reconsider F = (f . n) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

      

       A5: d in ( dom F) by A1, A4;

      reconsider r = (R . n) as Real;

      G = (r (#) F) by A2, Def7;

      hence thesis by A5, VALUED_1:def 5;

    end;

    theorem :: RFUNCT_3:32

    for D be non empty set, f be FinSequence, R be FinSequence of REAL , d be Element of D holds d is_common_for_dom (R (#) ( CHI (f,D))) by Th30, Th31;

    theorem :: RFUNCT_3:33

    for D be non empty set, d be Element of D, f be FinSequence of ( PFuncs (D, REAL )) st d is_common_for_dom f holds (( Sum f) . d) = ( Sum (f # d))

    proof

      let D be non empty set, d be Element of D;

      defpred P[ Nat] means for f be FinSequence of ( PFuncs (D, REAL )) st ( len f) = $1 & d is_common_for_dom f holds (( Sum f) . d) = ( Sum (f # d));

      let f be FinSequence of ( PFuncs (D, REAL ));

      assume

       A1: d is_common_for_dom f;

      

       A2: ( len f) = ( len f);

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let f be FinSequence of ( PFuncs (D, REAL ));

        assume that

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

         A6: d is_common_for_dom f;

        set fn = (f | n);

        

         A7: ( len fn) = n by A5, FINSEQ_1: 59, NAT_1: 11;

        ( 0 + 1) <= (n + 1) by NAT_1: 13;

        then

         A8: (n + 1) in ( dom f) by A5, FINSEQ_3: 25;

        then

        reconsider G = (f . (n + 1)) as Element of ( PFuncs (D, REAL )) by FINSEQ_2: 11;

        

         A9: ( dom f) = ( Seg ( len f)) & ( dom (f # d)) = ( Seg ( len (f # d))) by FINSEQ_1:def 3;

        f = (fn ^ <*G*>) by A5, RFINSEQ: 7;

        then

         A10: ( Sum f) = (( Sum fn) + G) by Th20;

        

         A11: ( len (f # d)) = ( len f) by Def8;

        

         A12: d in ( dom G) by A6, A8;

        now

          per cases ;

            case

             A13: n = 0 ;

            then

             A14: ( len (f # d)) = 1 by A5, Def8;

            then

             A15: 1 in ( dom (f # d)) by FINSEQ_3: 25;

             A16:

            now

              let m be Nat;

              assume m in ( Seg 1);

              then

               A17: m = 1 by FINSEQ_1: 2, TARSKI:def 1;

              

              hence ((f # d) . m) = (G . d) by A13, A15, Def8

              .= ( <*(G . d)*> . m) by A17, FINSEQ_1: 40;

            end;

            ( len <*(G . d)*>) = 1 & ( dom (f # d)) = ( Seg 1) by A14, FINSEQ_1: 40, FINSEQ_1:def 3;

            then

             A18: (f # d) = <*(G . d)*> by A14, A16, FINSEQ_2: 9;

            

             A19: (G . d) in REAL by XREAL_0:def 1;

            f = <*G*> by A5, A13, FINSEQ_1: 40;

            

            hence (( Sum f) . d) = (G . d) by FINSOP_1: 11

            .= ( Sum (f # d)) by A18, A19, FINSOP_1: 11;

          end;

            case

             A20: n <> 0 ;

            

             A21: ((f # d) . (n + 1)) = (G . d) by A9, A11, A8, Def8;

            d is_common_for_dom fn by A6, A20, Th26;

            then d in ( dom ( Sum fn)) by A7, A20, Th28;

            then d in (( dom ( Sum fn)) /\ ( dom G)) by A12, XBOOLE_0:def 4;

            then d in ( dom (( Sum fn) + G)) by VALUED_1:def 1;

            

            hence (( Sum f) . d) = ((( Sum fn) . d) + (G . d)) by A10, VALUED_1:def 1

            .= (( Sum (fn # d)) + (G . d)) by A4, A6, A7, A20, Th26

            .= (( Sum ((f # d) | n)) + (G . d)) by Th29

            .= ( Sum (((f # d) | n) ^ <*(G . d)*>)) by RVSUM_1: 74

            .= ( Sum (f # d)) by A5, A11, A21, RFINSEQ: 7;

          end;

        end;

        hence thesis;

      end;

      

       A22: P[ 0 ]

      proof

        let f be FinSequence of ( PFuncs (D, REAL ));

        assume that

         A23: ( len f) = 0 and d is_common_for_dom f;

        f = ( <*> ( PFuncs (D, REAL ))) by A23;

        

        then

         A24: (( Sum f) . d) = ((( [#] D) --> 0 qua Real) . d) by Th19

        .= 0 by FUNCOP_1: 7;

        ( len (f # d)) = 0 by A23, Def8;

        then (f # d) = ( <*> ( PFuncs (D, REAL )));

        hence thesis by A24, RVSUM_1: 72;

      end;

      for n holds P[n] from NAT_1:sch 2( A22, A3);

      hence thesis by A1, A2;

    end;

    definition

      let D be non empty set, F be PartFunc of D, REAL ;

      :: RFUNCT_3:def10

      func max+ (F) -> PartFunc of D, REAL means

      : Def10: ( dom it ) = ( dom F) & for d be Element of D st d in ( dom it ) holds (it . d) = ( max+ (F . d));

      existence

      proof

        deffunc Q( set) = ( In (( max+ (F . $1)), REAL ));

        defpred P[ set] means $1 in ( dom F);

        consider f be PartFunc of D, REAL such that

         A1: for d be Element of D holds d in ( dom f) iff P[d] and

         A2: for d be Element of D st d in ( dom f) holds (f . d) = Q(d) from SEQ_1:sch 3;

        take f;

        thus ( dom f) = ( dom F)

        proof

          thus ( dom f) c= ( dom F) by A1;

          let x be object;

          assume x in ( dom F);

          hence thesis by A1;

        end;

        let d be Element of D;

        assume d in ( dom f);

        then (f . d) = Q(d) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( set) = ( max+ (F . $1));

        for f,g be PartFunc of D, REAL st (( dom f) = ( dom F) & for c be Element of D st c in ( dom f) holds (f . c) = F(c)) & (( dom g) = ( dom F) & for c be Element of D st c in ( dom g) holds (g . c) = F(c)) holds f = g from SEQ_1:sch 4;

        hence thesis;

      end;

      :: RFUNCT_3:def11

      func max- (F) -> PartFunc of D, REAL means

      : Def11: ( dom it ) = ( dom F) & for d be Element of D st d in ( dom it ) holds (it . d) = ( max- (F . d));

      existence

      proof

        deffunc F( set) = ( In (( max- (F . $1)), REAL ));

        defpred P[ set] means $1 in ( dom F);

        consider f be PartFunc of D, REAL such that

         A3: for d be Element of D holds d in ( dom f) iff P[d] and

         A4: for d be Element of D st d in ( dom f) holds (f . d) = F(d) from SEQ_1:sch 3;

        take f;

        thus ( dom f) = ( dom F)

        proof

          thus ( dom f) c= ( dom F) by A3;

          let x be object;

          assume x in ( dom F);

          hence thesis by A3;

        end;

        let d be Element of D;

        assume d in ( dom f);

        then (f . d) = F(d) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( set) = ( max- (F . $1));

        for f,g be PartFunc of D, REAL st (( dom f) = ( dom F) & for c be Element of D st c in ( dom f) holds (f . c) = F(c)) & (( dom g) = ( dom F) & for c be Element of D st c in ( dom g) holds (g . c) = F(c)) holds f = g from SEQ_1:sch 4;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_3:34

    for D be non empty set, F be PartFunc of D, REAL holds F = (( max+ F) - ( max- F)) & ( abs F) = (( max+ F) + ( max- F)) & (2 (#) ( max+ F)) = (F + ( abs F))

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom F) = (( dom F) /\ ( dom F));

      

       A2: ( dom ( max+ F)) = ( dom F) by Def10;

      

       A3: ( dom ( max- F)) = ( dom F) by Def11;

      ( dom ( - ( max- F))) = ( dom ( max- F)) by VALUED_1:def 5;

      then

       A4: ( dom F) = ( dom (( max+ F) + ( - ( max- F)))) by A2, A3, A1, VALUED_1:def 1;

      now

        let d be Element of D;

        assume

         A5: d in ( dom F);

        

        hence ((( max+ F) - ( max- F)) . d) = ((( max+ F) . d) - (( max- F) . d)) by A4, VALUED_1: 13

        .= (( max+ (F . d)) - (( max- F) . d)) by A2, A5, Def10

        .= (( max+ (F . d)) - ( max- (F . d))) by A3, A5, Def11

        .= (F . d) by Th1;

      end;

      hence F = (( max+ F) - ( max- F)) by A4, PARTFUN1: 5;

      

       A6: ( dom ( abs F)) = ( dom F) by VALUED_1:def 11;

      then

       A7: ( dom ( abs F)) = ( dom (( max+ F) + ( max- F))) by A2, A3, A1, VALUED_1:def 1;

      now

        let d be Element of D;

        assume

         A8: d in ( dom ( abs F));

        

        hence ((( max+ F) + ( max- F)) . d) = ((( max+ F) . d) + (( max- F) . d)) by A7, VALUED_1:def 1

        .= (( max+ (F . d)) + (( max- F) . d)) by A2, A6, A8, Def10

        .= (( max+ (F . d)) + ( max- (F . d))) by A3, A6, A8, Def11

        .= |.(F . d).| by Th2

        .= (( abs F) . d) by VALUED_1: 18;

      end;

      hence ( abs F) = (( max+ F) + ( max- F)) by A7, PARTFUN1: 5;

      

       A9: ( dom (2 (#) ( max+ F))) = ( dom ( max+ F)) by VALUED_1:def 5;

      then

       A10: ( dom (2 (#) ( max+ F))) = ( dom (F + ( abs F))) by A2, A6, A1, VALUED_1:def 1;

      now

        let d be Element of D;

        assume

         A11: d in ( dom F);

        

        hence ((2 (#) ( max+ F)) . d) = (2 * (( max+ F) . d)) by A2, A9, VALUED_1:def 5

        .= (2 * ( max+ (F . d))) by A2, A11, Def10

        .= ((F . d) + |.(F . d).|) by Th3

        .= ((F . d) + (( abs F) . d)) by VALUED_1: 18

        .= ((F + ( abs F)) . d) by A2, A9, A10, A11, VALUED_1:def 1;

      end;

      hence thesis by A2, A9, A10, PARTFUN1: 5;

    end;

    theorem :: RFUNCT_3:35

    

     Th35: for D be non empty set, F be PartFunc of D, REAL , r st 0 < r holds (F " {r}) = (( max+ F) " {r})

    proof

      let D be non empty set, F be PartFunc of D, REAL , r;

      

       A1: ( dom ( max+ F)) = ( dom F) by Def10;

      assume

       A2: 0 < r;

      thus (F " {r}) c= (( max+ F) " {r})

      proof

        let x be object;

        assume

         A3: x in (F " {r});

        then

        reconsider d = x as Element of D;

        (F . d) in {r} by A3, FUNCT_1:def 7;

        then

         A4: (F . d) = r by TARSKI:def 1;

        

         A5: d in ( dom F) by A3, FUNCT_1:def 7;

        

        then (( max+ F) . d) = ( max+ (F . d)) by A1, Def10

        .= r by A2, A4, XXREAL_0:def 10;

        then (( max+ F) . d) in {r} by TARSKI:def 1;

        hence thesis by A1, A5, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A6: x in (( max+ F) " {r});

      then

      reconsider d = x as Element of D;

      (( max+ F) . d) in {r} by A6, FUNCT_1:def 7;

      then

       A7: (( max+ F) . d) = r by TARSKI:def 1;

      

       A8: d in ( dom F) by A1, A6, FUNCT_1:def 7;

      

      then (( max+ F) . d) = ( max+ (F . d)) by A1, Def10

      .= ( max ((F . d), 0 ));

      then (F . d) = r by A2, A7, XXREAL_0: 16;

      then (F . d) in {r} by TARSKI:def 1;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:36

    

     Th36: for D be non empty set, F be PartFunc of D, REAL holds (F " ( left_closed_halfline 0 )) = (( max+ F) " { 0 })

    proof

      set li = ( left_closed_halfline 0 );

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom ( max+ F)) = ( dom F) by Def10;

      

       A2: li = { s : s <= 0 } by XXREAL_1: 231;

      thus (F " li) c= (( max+ F) " { 0 })

      proof

        let x be object;

        assume

         A3: x in (F " li);

        then

        reconsider d = x as Element of D;

        (F . d) in li by A3, FUNCT_1:def 7;

        then ex s st s = (F . d) & s <= 0 by A2;

        then

         A4: ( max ((F . d), 0 )) = 0 by XXREAL_0:def 10;

        

         A5: d in ( dom F) by A3, FUNCT_1:def 7;

        

        then (( max+ F) . d) = ( max+ (F . d)) by A1, Def10

        .= ( max ((F . d), 0 ));

        then (( max+ F) . d) in { 0 } by A4, TARSKI:def 1;

        hence thesis by A1, A5, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A6: x in (( max+ F) " { 0 });

      then

      reconsider d = x as Element of D;

      (( max+ F) . d) in { 0 } by A6, FUNCT_1:def 7;

      then

       A7: (( max+ F) . d) = 0 by TARSKI:def 1;

      

       A8: d in ( dom F) by A1, A6, FUNCT_1:def 7;

      

      then (( max+ F) . d) = ( max+ (F . d)) by A1, Def10

      .= ( max ((F . d), 0 ));

      then (F . d) <= 0 by A7, XXREAL_0:def 10;

      then (F . d) in li by A2;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:37

    

     Th37: for D be non empty set, F be PartFunc of D, REAL , d be Element of D holds 0 <= (( max+ F) . d)

    proof

      let D be non empty set, F be PartFunc of D, REAL , d be Element of D;

      

       A1: ( dom F) = ( dom ( max+ F)) by Def10;

      per cases ;

        suppose d in ( dom F);

        

        then (( max+ F) . d) = ( max+ (F . d)) by A1, Def10

        .= ( max ((F . d), 0 ));

        hence thesis by XXREAL_0: 25;

      end;

        suppose not d in ( dom F);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: RFUNCT_3:38

    

     Th38: for D be non empty set, F be PartFunc of D, REAL , r st 0 < r holds (F " {( - r)}) = (( max- F) " {r})

    proof

      let D be non empty set, F be PartFunc of D, REAL , r;

      

       A1: ( dom ( max- F)) = ( dom F) by Def11;

      assume

       A2: 0 < r;

      thus (F " {( - r)}) c= (( max- F) " {r})

      proof

        let x be object;

        assume

         A3: x in (F " {( - r)});

        then

        reconsider d = x as Element of D;

        (F . d) in {( - r)} by A3, FUNCT_1:def 7;

        then

         A4: (F . d) = ( - r) by TARSKI:def 1;

        

         A5: d in ( dom F) by A3, FUNCT_1:def 7;

        

        then (( max- F) . d) = ( max- (F . d)) by A1, Def11

        .= r by A2, A4, XXREAL_0:def 10;

        then (( max- F) . d) in {r} by TARSKI:def 1;

        hence thesis by A1, A5, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A6: x in (( max- F) " {r});

      then

      reconsider d = x as Element of D;

      (( max- F) . d) in {r} by A6, FUNCT_1:def 7;

      then

       A7: (( max- F) . d) = r by TARSKI:def 1;

      

       A8: d in ( dom F) by A1, A6, FUNCT_1:def 7;

      

      then (( max- F) . d) = ( max- (F . d)) by A1, Def11

      .= ( max (( - (F . d)), 0 ));

      then ( - (F . d)) = r by A2, A7, XXREAL_0: 16;

      then (F . d) in {( - r)} by TARSKI:def 1;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:39

    

     Th39: for D be non empty set, F be PartFunc of D, REAL holds (F " ( right_closed_halfline 0 )) = (( max- F) " { 0 })

    proof

      set li = ( right_closed_halfline 0 );

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom ( max- F)) = ( dom F) by Def11;

      

       A2: li = { s : 0 <= s } by XXREAL_1: 232;

      thus (F " li) c= (( max- F) " { 0 })

      proof

        let x be object;

        assume

         A3: x in (F " li);

        then

        reconsider d = x as Element of D;

        (F . d) in li by A3, FUNCT_1:def 7;

        then ex s st s = (F . d) & 0 <= s by A2;

        then

         A4: ( max (( - (F . d)), 0 )) = 0 by XXREAL_0:def 10;

        

         A5: d in ( dom F) by A3, FUNCT_1:def 7;

        

        then (( max- F) . d) = ( max- (F . d)) by A1, Def11

        .= ( max (( - (F . d)), 0 ));

        then (( max- F) . d) in { 0 } by A4, TARSKI:def 1;

        hence thesis by A1, A5, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A6: x in (( max- F) " { 0 });

      then

      reconsider d = x as Element of D;

      (( max- F) . d) in { 0 } by A6, FUNCT_1:def 7;

      then

       A7: (( max- F) . d) = 0 by TARSKI:def 1;

      

       A8: d in ( dom F) by A1, A6, FUNCT_1:def 7;

      

      then (( max- F) . d) = ( max- (F . d)) by A1, Def11

      .= ( max (( - (F . d)), 0 ));

      then ( - (F . d)) <= ( - 0 ) by A7, XXREAL_0:def 10;

      then 0 <= (F . d) by XREAL_1: 24;

      then (F . d) in li by A2;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:40

    

     Th40: for D be non empty set, F be PartFunc of D, REAL , d be Element of D holds 0 <= (( max- F) . d)

    proof

      let D be non empty set, F be PartFunc of D, REAL , d be Element of D;

      

       A1: ( dom F) = ( dom ( max- F)) by Def11;

      per cases ;

        suppose d in ( dom F);

        

        then (( max- F) . d) = ( max- (F . d)) by A1, Def11

        .= ( max (( - (F . d)), 0 ));

        hence thesis by XXREAL_0: 25;

      end;

        suppose not d in ( dom F);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: RFUNCT_3:41

    for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL st (F,G) are_fiberwise_equipotent holds (( max+ F),( max+ G)) are_fiberwise_equipotent

    proof

      set li = ( left_closed_halfline 0 );

      let D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL ;

      assume

       A1: (F,G) are_fiberwise_equipotent ;

       A2:

      now

        let r be Element of REAL ;

        now

          per cases ;

            case 0 < r;

            then ( Coim (F,r)) = ( Coim (( max+ F),r)) & ( Coim (G,r)) = ( Coim (( max+ G),r)) by Th35;

            hence ( card ( Coim (( max+ F),r))) = ( card ( Coim (( max+ G),r))) by A1, CLASSES1:def 10;

          end;

            case

             A3: r = 0 ;

            (F " li) = (( max+ F) " { 0 }) & (G " li) = (( max+ G) " { 0 }) by Th36;

            hence ( card (( max+ F) " {r})) = ( card (( max+ G) " {r})) by A1, A3, CLASSES1: 78;

          end;

            case

             A4: r < 0 ;

            now

              assume r in ( rng ( max+ F));

              then ex d be Element of D st d in ( dom ( max+ F)) & (( max+ F) . d) = r by PARTFUN1: 3;

              hence contradiction by A4, Th37;

            end;

            then

             A5: (( max+ F) " {r}) = {} by Lm2;

            now

              assume r in ( rng ( max+ G));

              then ex c be Element of C st c in ( dom ( max+ G)) & (( max+ G) . c) = r by PARTFUN1: 3;

              hence contradiction by A4, Th37;

            end;

            hence ( card (( max+ F) " {r})) = ( card (( max+ G) " {r})) by A5, Lm2;

          end;

        end;

        hence ( card ( Coim (( max+ F),r))) = ( card ( Coim (( max+ G),r)));

      end;

      ( rng ( max+ F)) c= REAL & ( rng ( max+ G)) c= REAL ;

      hence thesis by A2, CLASSES1: 79;

    end;

    theorem :: RFUNCT_3:42

    for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL st (F,G) are_fiberwise_equipotent holds (( max- F),( max- G)) are_fiberwise_equipotent

    proof

      set li = ( right_closed_halfline 0 );

      let D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL ;

      assume

       A1: (F,G) are_fiberwise_equipotent ;

       A2:

      now

        let r be Element of REAL ;

        now

          per cases ;

            case 0 < r;

            then ( Coim (F,( - r))) = (( max- F) " {r}) & ( Coim (G,( - r))) = (( max- G) " {r}) by Th38;

            hence ( card ( Coim (( max- F),r))) = ( card ( Coim (( max- G),r))) by A1, CLASSES1:def 10;

          end;

            case

             A3: r = 0 ;

            (F " li) = (( max- F) " { 0 }) & (G " li) = (( max- G) " { 0 }) by Th39;

            hence ( card (( max- F) " {r})) = ( card (( max- G) " {r})) by A1, A3, CLASSES1: 78;

          end;

            case

             A4: r < 0 ;

            now

              assume r in ( rng ( max- F));

              then ex d be Element of D st d in ( dom ( max- F)) & (( max- F) . d) = r by PARTFUN1: 3;

              hence contradiction by A4, Th40;

            end;

            then

             A5: (( max- F) " {r}) = {} by Lm2;

            now

              assume r in ( rng ( max- G));

              then ex c be Element of C st c in ( dom ( max- G)) & (( max- G) . c) = r by PARTFUN1: 3;

              hence contradiction by A4, Th40;

            end;

            hence ( card (( max- F) " {r})) = ( card (( max- G) " {r})) by A5, Lm2;

          end;

        end;

        hence ( card ( Coim (( max- F),r))) = ( card ( Coim (( max- G),r)));

      end;

      ( rng ( max- F)) c= REAL & ( rng ( max- G)) c= REAL ;

      hence thesis by A2, CLASSES1: 79;

    end;

    registration

      let D be non empty set, F be finite PartFunc of D, REAL ;

      cluster ( max+ F) -> finite;

      coherence

      proof

        ( dom F) is finite;

        then ( dom ( max+ F)) is finite by Def10;

        hence thesis by FINSET_1: 10;

      end;

      cluster ( max- F) -> finite;

      coherence

      proof

        ( dom F) is finite;

        then ( dom ( max- F)) is finite by Def11;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: RFUNCT_3:43

    for D,C be non empty set, F be finite PartFunc of D, REAL , G be finite PartFunc of C, REAL st (( max+ F),( max+ G)) are_fiberwise_equipotent & (( max- F),( max- G)) are_fiberwise_equipotent holds (F,G) are_fiberwise_equipotent

    proof

      let D,C be non empty set, F be finite PartFunc of D, REAL , G be finite PartFunc of C, REAL ;

      assume that

       A1: (( max+ F),( max+ G)) are_fiberwise_equipotent and

       A2: (( max- F),( max- G)) are_fiberwise_equipotent ;

      set lh = ( left_closed_halfline 0 ), rh = ( right_closed_halfline 0 ), fp0 = (( max+ F) " { 0 }), fm0 = (( max- F) " { 0 }), gp0 = (( max+ G) " { 0 }), gm0 = (( max- G) " { 0 });

      

       A3: (lh /\ rh) = [. 0 , 0 .] by XXREAL_1: 272

      .= { 0 } by XXREAL_1: 17;

      (F " ( rng F)) c= (F " REAL ) by RELAT_1: 143;

      then

       A4: (F " REAL ) c= ( dom F) & ( dom F) c= (F " REAL ) by RELAT_1: 132, RELAT_1: 134;

      

       A5: (F " lh) = fp0 & (F " rh) = fm0 by Th36, Th39;

      (G " ( rng G)) c= (G " REAL ) by RELAT_1: 143;

      then

       A6: (G " REAL ) c= ( dom G) & ( dom G) c= (G " REAL ) by RELAT_1: 132, RELAT_1: 134;

      

       A7: (G " lh) = gp0 & (G " rh) = gm0 by Th36, Th39;

      reconsider fp0, fm0, gp0, gm0 as finite set;

      

       A8: (lh \/ rh) = ( REAL \ ]. 0 , 0 .[) by XXREAL_1: 398

      .= ( REAL \ {} ) by XXREAL_1: 28

      .= REAL ;

      then (fp0 \/ fm0) = (F " REAL ) by A5, RELAT_1: 140;

      then

       A9: (fp0 \/ fm0) = ( dom F) by A4;

      (gp0 \/ gm0) = (G " (lh \/ rh)) by A7, RELAT_1: 140;

      then

       A10: (gp0 \/ gm0) = ( dom G) by A8, A6;

      ( card (fp0 \/ fm0)) = ((( card fp0) + ( card fm0)) - ( card (fp0 /\ fm0))) by CARD_2: 45;

      then

       A11: ( card (fp0 /\ fm0)) = ((( card fp0) + ( card fm0)) - ( card (fp0 \/ fm0)));

      ( card (gp0 \/ gm0)) = ((( card gp0) + ( card gm0)) - ( card (gp0 /\ gm0))) by CARD_2: 45;

      then

       A12: ( card (gp0 /\ gm0)) = ((( card gp0) + ( card gm0)) - ( card (gp0 \/ gm0)));

      

       A13: ( dom F) = ( dom ( max+ F)) & ( dom G) = ( dom ( max+ G)) by Def10;

       A14:

      now

        let r be Element of REAL ;

        

         A15: ( card fp0) = ( card gp0) & ( card fm0) = ( card gm0) by A1, A2, CLASSES1: 78;

        now

          per cases ;

            case 0 < r;

            then ( Coim (F,r)) = ( Coim (( max+ F),r)) & ( Coim (G,r)) = ( Coim (( max+ G),r)) by Th35;

            hence ( card ( Coim (F,r))) = ( card ( Coim (G,r))) by A1, CLASSES1:def 10;

          end;

            case 0 = r;

            then (F " {r}) = ((F " lh) /\ (F " rh)) & (G " {r}) = ((G " lh) /\ (G " rh)) by A3, FUNCT_1: 68;

            hence ( card (F " {r})) = ( card (G " {r})) by A1, A13, A5, A7, A11, A12, A9, A10, A15, CLASSES1: 81;

          end;

            case

             A16: r < 0 ;

            

             A17: ( - ( - r)) = r;

             0 < ( - r) by A16, XREAL_1: 58;

            then ( Coim (F,r)) = ( Coim (( max- F),( - r))) & ( Coim (G,r)) = ( Coim (( max- G),( - r))) by A17, Th38;

            hence ( card ( Coim (F,r))) = ( card ( Coim (G,r))) by A2, CLASSES1:def 10;

          end;

        end;

        hence ( card ( Coim (F,r))) = ( card ( Coim (G,r)));

      end;

      ( rng F) c= REAL & ( rng G) c= REAL ;

      hence thesis by A14, CLASSES1: 79;

    end;

    theorem :: RFUNCT_3:44

    

     Th44: for D be non empty set, F be PartFunc of D, REAL , X be set holds (( max+ F) | X) = ( max+ (F | X))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      

       A1: ( dom (( max+ F) | X)) = (( dom ( max+ F)) /\ X) by RELAT_1: 61;

      

       A2: (( dom ( max+ F)) /\ X) = (( dom F) /\ X) by Def10

      .= ( dom (F | X)) by RELAT_1: 61;

      

       A3: ( dom (F | X)) = ( dom ( max+ (F | X))) by Def10;

      now

        let d be Element of D;

        assume

         A4: d in ( dom (( max+ F) | X));

        then

         A5: d in ( dom ( max+ F)) by A1, XBOOLE_0:def 4;

        

        thus ((( max+ F) | X) . d) = (( max+ F) . d) by A4, FUNCT_1: 47

        .= ( max+ (F . d)) by A5, Def10

        .= ( max+ ((F | X) . d)) by A1, A2, A4, FUNCT_1: 47

        .= (( max+ (F | X)) . d) by A1, A2, A3, A4, Def10;

      end;

      hence thesis by A2, A3, PARTFUN1: 5, RELAT_1: 61;

    end;

    theorem :: RFUNCT_3:45

    for D be non empty set, F be PartFunc of D, REAL , X be set holds (( max- F) | X) = ( max- (F | X))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      

       A1: ( dom (( max- F) | X)) = (( dom ( max- F)) /\ X) by RELAT_1: 61;

      

       A2: (( dom ( max- F)) /\ X) = (( dom F) /\ X) by Def11

      .= ( dom (F | X)) by RELAT_1: 61;

      

       A3: ( dom (F | X)) = ( dom ( max- (F | X))) by Def11;

      now

        let d be Element of D;

        assume

         A4: d in ( dom (( max- F) | X));

        then

         A5: d in ( dom ( max- F)) by A1, XBOOLE_0:def 4;

        

        thus ((( max- F) | X) . d) = (( max- F) . d) by A4, FUNCT_1: 47

        .= ( max- (F . d)) by A5, Def11

        .= ( max- ((F | X) . d)) by A1, A2, A4, FUNCT_1: 47

        .= (( max- (F | X)) . d) by A1, A2, A3, A4, Def11;

      end;

      hence thesis by A2, A3, PARTFUN1: 5, RELAT_1: 61;

    end;

    theorem :: RFUNCT_3:46

    

     Th46: for D be non empty set, F be PartFunc of D, REAL st (for d be Element of D st d in ( dom F) holds (F . d) >= 0 ) holds ( max+ F) = F

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom ( max+ F)) = ( dom F) by Def10;

      assume

       A2: for d be Element of D st d in ( dom F) holds (F . d) >= 0 ;

      now

        let d be Element of D;

        assume

         A3: d in ( dom F);

        then

         A4: (F . d) >= 0 by A2;

        

        thus (( max+ F) . d) = ( max+ (F . d)) by A1, A3, Def10

        .= (F . d) by A4, XXREAL_0:def 10;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: RFUNCT_3:47

    for D be non empty set, F be PartFunc of D, REAL st (for d be Element of D st d in ( dom F) holds (F . d) <= 0 ) holds ( max- F) = ( - F)

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      

       A1: ( dom ( max- F)) = ( dom F) by Def11;

      assume

       A2: for d be Element of D st d in ( dom F) holds (F . d) <= 0 ;

       A3:

      now

        let d be Element of D;

        assume

         A4: d in ( dom F);

        then

         A5: (F . d) <= 0 by A2;

        

        thus (( max- F) . d) = ( max- (F . d)) by A1, A4, Def11

        .= ( - (F . d)) by A5, XXREAL_0:def 10

        .= (( - F) . d) by VALUED_1: 8;

      end;

      ( dom F) = ( dom ( - F)) by VALUED_1: 8;

      hence thesis by A1, A3, PARTFUN1: 5;

    end;

    theorem :: RFUNCT_3:48

    

     Th48: for D be non empty set, F be PartFunc of D, REAL holds (F - 0 ) = F

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

       A1:

      now

        let d be Element of D;

        assume d in ( dom F);

        

        hence ((F - 0 ) . d) = ((F . d) - 0 ) by VALUED_1: 3

        .= (F . d);

      end;

      ( dom (F - 0 )) = ( dom F) by VALUED_1: 3;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: RFUNCT_3:49

    for D be non empty set, F be PartFunc of D, REAL , r be Real, X be set holds ((F | X) - r) = ((F - r) | X)

    proof

      let D be non empty set, F be PartFunc of D, REAL , r be Real, X be set;

      

       A1: ( dom ((F | X) - r)) = ( dom (F | X)) by VALUED_1: 3;

      

       A2: ( dom (F | X)) = (( dom F) /\ X) by RELAT_1: 61;

      

       A3: (( dom F) /\ X) = (( dom (F - r)) /\ X) by VALUED_1: 3

      .= ( dom ((F - r) | X)) by RELAT_1: 61;

      now

        let d be Element of D;

        assume

         A4: d in ( dom ((F | X) - r));

        then

         A5: d in ( dom F) by A1, A2, XBOOLE_0:def 4;

        

        thus (((F | X) - r) . d) = (((F | X) . d) - r) by A1, A4, VALUED_1: 3

        .= ((F . d) - r) by A1, A4, FUNCT_1: 47

        .= ((F - r) . d) by A5, VALUED_1: 3

        .= (((F - r) | X) . d) by A1, A2, A3, A4, FUNCT_1: 47;

      end;

      hence thesis by A2, A3, PARTFUN1: 5, VALUED_1: 3;

    end;

    theorem :: RFUNCT_3:50

    

     Th50: for D be non empty set, F be PartFunc of D, REAL , r, s holds (F " {(s + r)}) = ((F - r) " {s})

    proof

      let D be non empty set, F be PartFunc of D, REAL , r, s;

      thus (F " {(s + r)}) c= ((F - r) " {s})

      proof

        let x be object;

        assume

         A1: x in (F " {(s + r)});

        then

        reconsider d = x as Element of D;

        

         A2: d in ( dom F) by A1, FUNCT_1:def 7;

        (F . d) in {(s + r)} by A1, FUNCT_1:def 7;

        then (F . d) = (s + r) by TARSKI:def 1;

        then ((F . d) - r) = s;

        then ((F - r) . d) = s by A2, VALUED_1: 3;

        then

         A3: ((F - r) . d) in {s} by TARSKI:def 1;

        d in ( dom (F - r)) by A2, VALUED_1: 3;

        hence thesis by A3, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A4: x in ((F - r) " {s});

      then

      reconsider d = x as Element of D;

      d in ( dom (F - r)) by A4, FUNCT_1:def 7;

      then

       A5: d in ( dom F) by VALUED_1: 3;

      ((F - r) . d) in {s} by A4, FUNCT_1:def 7;

      then ((F - r) . d) = s by TARSKI:def 1;

      then ((F . d) - r) = s by A5, VALUED_1: 3;

      then (F . d) in {(s + r)} by TARSKI:def 1;

      hence thesis by A5, FUNCT_1:def 7;

    end;

    theorem :: RFUNCT_3:51

    for D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL , r be Real holds (F,G) are_fiberwise_equipotent iff ((F - r),(G - r)) are_fiberwise_equipotent

    proof

      let D,C be non empty set, F be PartFunc of D, REAL , G be PartFunc of C, REAL , r be Real;

      

       A1: ( rng (F - r)) c= REAL & ( rng (G - r)) c= REAL ;

      thus (F,G) are_fiberwise_equipotent implies ((F - r),(G - r)) are_fiberwise_equipotent

      proof

        assume

         A2: (F,G) are_fiberwise_equipotent ;

        now

          let s be Element of REAL ;

          

          thus ( card ( Coim ((F - r),s))) = ( card ( Coim (F,(s + r)))) by Th50

          .= ( card ( Coim (G,(s + r)))) by A2, CLASSES1:def 10

          .= ( card ( Coim ((G - r),s))) by Th50;

        end;

        hence thesis by A1, CLASSES1: 79;

      end;

      assume

       A3: ((F - r),(G - r)) are_fiberwise_equipotent ;

       A4:

      now

        let s be Element of REAL ;

        

         A5: s = ((s - r) + r);

        

        hence ( card ( Coim (F,s))) = ( card ( Coim ((F - r),(s - r)))) by Th50

        .= ( card ( Coim ((G - r),(s - r)))) by A3, CLASSES1:def 10

        .= ( card ( Coim (G,s))) by A5, Th50;

      end;

      ( rng F) c= REAL & ( rng G) c= REAL ;

      hence thesis by A4, CLASSES1: 79;

    end;

    definition

      let F be PartFunc of REAL , REAL , X be set;

      :: RFUNCT_3:def12

      pred F is_convex_on X means X c= ( dom F) & for p be Real st 0 <= p & p <= 1 holds for r,s be Real st r in X & s in X & ((p * r) + ((1 - p) * s)) in X holds (F . ((p * r) + ((1 - p) * s))) <= ((p * (F . r)) + ((1 - p) * (F . s)));

    end

    theorem :: RFUNCT_3:52

    for a,b be Real, F be PartFunc of REAL , REAL holds F is_convex_on [.a, b.] iff [.a, b.] c= ( dom F) & for p be Real st 0 <= p & p <= 1 holds for r,s be Real st r in [.a, b.] & s in [.a, b.] holds (F . ((p * r) + ((1 - p) * s))) <= ((p * (F . r)) + ((1 - p) * (F . s)))

    proof

      let a,b be Real, f be PartFunc of REAL , REAL ;

      set ab = { r : a <= r & r <= b };

      

       A1: [.a, b.] = ab by RCOMP_1:def 1;

      thus f is_convex_on [.a, b.] implies [.a, b.] c= ( dom f) & for p be Real st 0 <= p & p <= 1 holds for x,y be Real st x in [.a, b.] & y in [.a, b.] holds (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)))

      proof

        assume

         A2: f is_convex_on [.a, b.];

        hence [.a, b.] c= ( dom f);

        let p be Real;

        assume that

         A3: 0 <= p and

         A4: p <= 1;

        

         A5: 0 <= (1 - p) by A4, XREAL_1: 48;

        

         A6: ((p * b) + ((1 - p) * b)) = b;

        

         A7: ((p * a) + ((1 - p) * a)) = a;

        let x,y be Real;

        assume that

         A8: x in [.a, b.] and

         A9: y in [.a, b.];

        

         A10: ex r2 st r2 = y & a <= r2 & r2 <= b by A1, A9;

        then

         A11: ((1 - p) * y) <= ((1 - p) * b) by A5, XREAL_1: 64;

        

         A12: ex r1 st r1 = x & a <= r1 & r1 <= b by A1, A8;

        then (p * x) <= (p * b) by A3, XREAL_1: 64;

        then

         A13: ((p * x) + ((1 - p) * y)) <= b by A11, A6, XREAL_1: 7;

        

         A14: ((1 - p) * a) <= ((1 - p) * y) by A5, A10, XREAL_1: 64;

        (p * a) <= (p * x) by A3, A12, XREAL_1: 64;

        then a <= ((p * x) + ((1 - p) * y)) by A14, A7, XREAL_1: 7;

        then ((p * x) + ((1 - p) * y)) in ab by A13;

        hence thesis by A1, A2, A3, A4, A8, A9;

      end;

      assume that

       A15: [.a, b.] c= ( dom f) and

       A16: for p be Real st 0 <= p & p <= 1 holds for x,y be Real st x in [.a, b.] & y in [.a, b.] holds (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

      thus [.a, b.] c= ( dom f) by A15;

      let p be Real;

      assume

       A17: 0 <= p & p <= 1;

      let x,y be Real;

      assume that

       A18: x in [.a, b.] & y in [.a, b.] and ((p * x) + ((1 - p) * y)) in [.a, b.];

      thus thesis by A16, A17, A18;

    end;

    theorem :: RFUNCT_3:53

    for a,b be Real, F be PartFunc of REAL , REAL holds F is_convex_on [.a, b.] iff [.a, b.] c= ( dom F) & for x1,x2,x3 be Real st x1 in [.a, b.] & x2 in [.a, b.] & x3 in [.a, b.] & x1 < x2 & x2 < x3 holds (((F . x1) - (F . x2)) / (x1 - x2)) <= (((F . x2) - (F . x3)) / (x2 - x3))

    proof

      let a,b be Real, f be PartFunc of REAL , REAL ;

      thus f is_convex_on [.a, b.] implies [.a, b.] c= ( dom f) & for x1,x2,x3 be Real st x1 in [.a, b.] & x2 in [.a, b.] & x3 in [.a, b.] & x1 < x2 & x2 < x3 holds (((f . x1) - (f . x2)) / (x1 - x2)) <= (((f . x2) - (f . x3)) / (x2 - x3))

      proof

        assume

         A1: f is_convex_on [.a, b.];

        hence [.a, b.] c= ( dom f);

        let x1,x2,x3 be Real;

        assume that

         A2: x1 in [.a, b.] & x2 in [.a, b.] & x3 in [.a, b.] and

         A3: x1 < x2 and

         A4: x2 < x3;

        

         A5: (x2 - x3) < 0 by A4, XREAL_1: 49;

        set r = ((x2 - x3) / (x1 - x3));

        

         A6: (r * ((f . x2) - (f . x1))) = ((r * (f . x2)) - (r * (f . x1))) & ((1 - r) * ((f . x3) - (f . x2))) = (((1 - r) * (f . x3)) - ((1 - r) * (f . x2)));

        

         A7: ((x1 - x2) / (x1 - x3)) = (((x1 - x3) " ) * (x1 - x2)) by XCMPLX_0:def 9;

        x1 < x3 by A3, A4, XXREAL_0: 2;

        then

         A8: (x1 - x3) < 0 by XREAL_1: 49;

        

         A9: (r + ((x1 - x2) / (x1 - x3))) = (((x1 - x2) + (x2 - x3)) / (x1 - x3)) by XCMPLX_1: 62

        .= 1 by A8, XCMPLX_1: 60;

        

        then

         A10: ((r * x1) + ((1 - r) * x3)) = (((x1 * (x2 - x3)) / (x1 - x3)) + (x3 * ((x1 - x2) / (x1 - x3)))) by XCMPLX_1: 74

        .= (((x1 * (x2 - x3)) / (x1 - x3)) + ((x3 * (x1 - x2)) / (x1 - x3))) by XCMPLX_1: 74

        .= ((((x2 * x1) - (x3 * x1)) + ((x1 - x2) * x3)) / (x1 - x3)) by XCMPLX_1: 62

        .= ((x2 * (x1 - x3)) / (x1 - x3))

        .= x2 by A8, XCMPLX_1: 89;

        

         A11: (x1 - x2) < 0 by A3, XREAL_1: 49;

        then r <= 1 by A8, A9, XREAL_1: 29, XREAL_1: 140;

        then ((r * (f . x2)) + ((1 - r) * (f . x2))) <= ((r * (f . x1)) + ((1 - r) * (f . x3))) by A1, A2, A5, A8, A10;

        then (r * ((f . x2) - (f . x1))) <= ((1 - r) * ((f . x3) - (f . x2))) by A6, XREAL_1: 21;

        then ( - ((1 - r) * ((f . x3) - (f . x2)))) <= ( - (r * ((f . x2) - (f . x1)))) by XREAL_1: 24;

        then ((1 - r) * ( - ((f . x3) - (f . x2)))) <= (r * ( - ((f . x2) - (f . x1))));

        then ((((x1 - x3) " ) * (x1 - x2)) * ((f . x2) - (f . x3))) <= ((((x1 - x3) " ) * (x2 - x3)) * ((f . x1) - (f . x2))) by A9, A7, XCMPLX_0:def 9;

        then

         A12: ((x1 - x3) * ((((x1 - x3) " ) * (x2 - x3)) * ((f . x1) - (f . x2)))) <= ((x1 - x3) * ((((x1 - x3) " ) * (x1 - x2)) * ((f . x2) - (f . x3)))) by A8, XREAL_1: 65;

        set v = ((x1 - x2) * ((f . x2) - (f . x3)));

        set u = ((x2 - x3) * ((f . x1) - (f . x2)));

        

         A13: ((x1 - x3) * ((((x1 - x3) " ) * (x1 - x2)) * ((f . x2) - (f . x3)))) = (((x1 - x3) * ((x1 - x3) " )) * v)

        .= (1 * v) by A8, XCMPLX_0:def 7

        .= v;

        ((x1 - x3) * ((((x1 - x3) " ) * (x2 - x3)) * ((f . x1) - (f . x2)))) = (((x1 - x3) * ((x1 - x3) " )) * u)

        .= (1 * u) by A8, XCMPLX_0:def 7

        .= u;

        hence thesis by A5, A11, A12, A13, XREAL_1: 103;

      end;

      assume that

       A14: [.a, b.] c= ( dom f) and

       A15: for x1,x2,x3 be Real st x1 in [.a, b.] & x2 in [.a, b.] & x3 in [.a, b.] & x1 < x2 & x2 < x3 holds (((f . x1) - (f . x2)) / (x1 - x2)) <= (((f . x2) - (f . x3)) / (x2 - x3));

      now

        let p be Real;

        assume that

         A16: 0 <= p and

         A17: p <= 1;

        

         A18: 0 <= (1 - p) by A17, XREAL_1: 48;

        let x,y be Real;

        set r = ((p * x) + ((1 - p) * y));

        assume that

         A19: x in [.a, b.] and

         A20: y in [.a, b.];

        

         A21: ((p * y) + ((1 - p) * y)) = y;

        

         A22: { s : a <= s & s <= b } = [.a, b.] by RCOMP_1:def 1;

        then

         A23: ex t st t = y & a <= t & t <= b by A20;

        then

         A24: ((1 - p) * y) <= ((1 - p) * b) by A18, XREAL_1: 64;

        

         A25: ex t st t = x & a <= t & t <= b by A22, A19;

        then ((p * b) + ((1 - p) * b)) = b & (p * x) <= (p * b) by A16, XREAL_1: 64;

        then

         A26: r <= b by A24, XREAL_1: 7;

        

         A27: ((1 - p) * a) <= ((1 - p) * y) by A18, A23, XREAL_1: 64;

        ((p * a) + ((1 - p) * a)) = a & (p * a) <= (p * x) by A16, A25, XREAL_1: 64;

        then a <= r by A27, XREAL_1: 7;

        then

         A28: r in [.a, b.] by A22, A26;

        

         A29: ((p * x) + ((1 - p) * x)) = x;

        now

          per cases ;

            case x = y;

            hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

          end;

            case

             A30: x <> y;

            now

              per cases ;

                case p = 0 ;

                hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

              end;

                case

                 A31: p <> 0 ;

                now

                  per cases ;

                    case p = 1;

                    hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

                  end;

                    case p <> 1;

                    then p < 1 by A17, XXREAL_0: 1;

                    then

                     A32: 0 < (1 - p) by XREAL_1: 50;

                    now

                      per cases by A30, XXREAL_0: 1;

                        case

                         A33: x < y;

                        then ((1 - p) * x) < ((1 - p) * y) by A32, XREAL_1: 68;

                        then

                         A34: x < r by A29, XREAL_1: 8;

                        then

                         A35: (x - r) < 0 by XREAL_1: 49;

                        (p * x) < (p * y) by A16, A31, A33, XREAL_1: 68;

                        then

                         A36: r < y by A21, XREAL_1: 8;

                        then

                         A37: (r - y) < 0 by XREAL_1: 49;

                        

                         A38: (x - y) < 0 by A33, XREAL_1: 49;

                        (((f . x) - (f . r)) / (x - r)) <= (((f . r) - (f . y)) / (r - y)) by A15, A19, A20, A28, A36, A34;

                        then (((f . x) - (f . r)) * (p * (x - y))) <= (((f . r) - (f . y)) * ((1 - p) * (x - y))) by A37, A35, XREAL_1: 107;

                        then (((((f . x) - (f . r)) * p) * (x - y)) / (x - y)) >= (((((f . r) - (f . y)) * (1 - p)) * (x - y)) / (x - y)) by A38, XREAL_1: 73;

                        then (((((f . r) - (f . y)) * (1 - p)) * (x - y)) / (x - y)) <= (((f . x) - (f . r)) * p) by A38, XCMPLX_1: 89;

                        then (((f . r) * (1 - p)) - ((f . y) * (1 - p))) <= (((f . x) * p) - ((f . r) * p)) by A38, XCMPLX_1: 89;

                        then (((f . r) * p) + (((f . r) * (1 - p)) - ((f . y) * (1 - p)))) <= ((f . x) * p) by XREAL_1: 19;

                        then ((((f . r) * p) + ((f . r) * (1 - p))) - ((f . y) * (1 - p))) <= ((f . x) * p);

                        hence (f . r) <= ((p * (f . x)) + ((1 - p) * (f . y))) by XREAL_1: 20;

                      end;

                        case

                         A39: y < x;

                        then ((1 - p) * y) < ((1 - p) * x) by A32, XREAL_1: 68;

                        then

                         A40: r < x by A29, XREAL_1: 8;

                        then

                         A41: (r - x) < 0 by XREAL_1: 49;

                        (p * y) < (p * x) by A16, A31, A39, XREAL_1: 68;

                        then

                         A42: y < r by A21, XREAL_1: 8;

                        then

                         A43: (y - r) < 0 by XREAL_1: 49;

                        

                         A44: (y - x) < 0 by A39, XREAL_1: 49;

                        (((f . y) - (f . r)) / (y - r)) <= (((f . r) - (f . x)) / (r - x)) by A15, A19, A20, A28, A42, A40;

                        then (((f . y) - (f . r)) * ((1 - p) * (y - x))) <= (((f . r) - (f . x)) * (p * (y - x))) by A43, A41, XREAL_1: 107;

                        then (((((f . y) - (f . r)) * (1 - p)) * (y - x)) / (y - x)) >= (((((f . r) - (f . x)) * p) * (y - x)) / (y - x)) by A44, XREAL_1: 73;

                        then (((((f . r) - (f . x)) * p) * (y - x)) / (y - x)) <= (((f . y) - (f . r)) * (1 - p)) by A44, XCMPLX_1: 89;

                        then (((f . r) * p) - ((f . x) * p)) <= (((f . y) * (1 - p)) - ((f . r) * (1 - p))) by A44, XCMPLX_1: 89;

                        then ((((f . r) * p) - ((f . x) * p)) + ((f . r) * (1 - p))) <= ((f . y) * (1 - p)) by XREAL_1: 19;

                        then ((((f . r) * p) + ((f . r) * (1 - p))) - ((f . x) * p)) <= ((f . y) * (1 - p));

                        hence (f . r) <= ((p * (f . x)) + ((1 - p) * (f . y))) by XREAL_1: 20;

                      end;

                    end;

                    hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

                  end;

                end;

                hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

              end;

            end;

            hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

          end;

        end;

        hence (f . ((p * x) + ((1 - p) * y))) <= ((p * (f . x)) + ((1 - p) * (f . y)));

      end;

      hence thesis by A14;

    end;

    theorem :: RFUNCT_3:54

    for F be PartFunc of REAL , REAL , X,Y be set st F is_convex_on X & Y c= X holds F is_convex_on Y

    proof

      let F be PartFunc of REAL , REAL , X,Y be set;

      assume that

       A1: F is_convex_on X and

       A2: Y c= X;

      X c= ( dom F) by A1;

      hence Y c= ( dom F) by A2;

      let p be Real;

      assume

       A3: 0 <= p & p <= 1;

      let x,y be Real;

      assume x in Y & y in Y & ((p * x) + ((1 - p) * y)) in Y;

      hence thesis by A1, A2, A3;

    end;

    theorem :: RFUNCT_3:55

    for F be PartFunc of REAL , REAL , X be set, r holds F is_convex_on X iff (F - r) is_convex_on X

    proof

      let F be PartFunc of REAL , REAL , X be set, r;

      

       A1: ( dom F) = ( dom (F - r)) by VALUED_1: 3;

      thus F is_convex_on X implies (F - r) is_convex_on X

      proof

        assume

         A2: F is_convex_on X;

        hence

         A3: X c= ( dom (F - r)) by A1;

        let p be Real;

        assume

         A4: 0 <= p & p <= 1;

        let x,y be Real;

        assume that

         A5: x in X and

         A6: y in X and

         A7: ((p * x) + ((1 - p) * y)) in X;

        (F . ((p * x) + ((1 - p) * y))) <= ((p * (F . x)) + ((1 - p) * (F . y))) by A2, A4, A5, A6, A7;

        then

         A8: ((F . ((p * x) + ((1 - p) * y))) - r) <= (((p * (F . x)) + ((1 - p) * (F . y))) - r) by XREAL_1: 9;

        (((p * (F . x)) + ((1 - p) * (F . y))) - r) = ((p * ((F . x) - r)) + ((1 - p) * ((F . y) - r)))

        .= ((p * ((F - r) . x)) + ((1 - p) * ((F . y) - r))) by A1, A3, A5, VALUED_1: 3

        .= ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) by A1, A3, A6, VALUED_1: 3;

        hence thesis by A1, A3, A7, A8, VALUED_1: 3;

      end;

      assume

       A9: (F - r) is_convex_on X;

      hence

       A10: X c= ( dom F) by A1;

      let p be Real;

      assume

       A11: 0 <= p & p <= 1;

      let x,y be Real;

      assume that

       A12: x in X and

       A13: y in X and

       A14: ((p * x) + ((1 - p) * y)) in X;

      ((F - r) . ((p * x) + ((1 - p) * y))) <= ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) by A9, A11, A12, A13, A14;

      then

       A15: ((F . ((p * x) + ((1 - p) * y))) - r) <= ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) by A10, A14, VALUED_1: 3;

      ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) = ((p * ((F - r) . x)) + ((1 - p) * ((F . y) - r))) by A10, A13, VALUED_1: 3

      .= ((p * ((F . x) - r)) + (((1 - p) * (F . y)) - ((1 - p) * r))) by A10, A12, VALUED_1: 3

      .= (((p * (F . x)) + ((1 - p) * (F . y))) - r);

      hence thesis by A15, XREAL_1: 9;

    end;

    theorem :: RFUNCT_3:56

    for F be PartFunc of REAL , REAL , X be set, r st 0 < r holds F is_convex_on X iff (r (#) F) is_convex_on X

    proof

      let F be PartFunc of REAL , REAL , X be set, r;

      assume

       A1: 0 < r;

      

       A2: ( dom F) = ( dom (r (#) F)) by VALUED_1:def 5;

      thus F is_convex_on X implies (r (#) F) is_convex_on X

      proof

        assume

         A3: F is_convex_on X;

        then

         A4: X c= ( dom F);

        thus X c= ( dom (r (#) F)) by A2, A3;

        let p be Real;

        assume

         A5: 0 <= p & p <= 1;

        let x,y be Real;

        assume that

         A6: x in X and

         A7: y in X and

         A8: ((p * x) + ((1 - p) * y)) in X;

        (F . ((p * x) + ((1 - p) * y))) <= ((p * (F . x)) + ((1 - p) * (F . y))) by A3, A5, A6, A7, A8;

        then (r * (F . ((p * x) + ((1 - p) * y)))) <= (r * ((p * (F . x)) + ((1 - p) * (F . y)))) by A1, XREAL_1: 64;

        then ((r (#) F) . ((p * x) + ((1 - p) * y))) <= ((p * (r * (F . x))) + (((1 - p) * r) * (F . y))) by A2, A4, A8, VALUED_1:def 5;

        then ((r (#) F) . ((p * x) + ((1 - p) * y))) <= ((p * ((r (#) F) . x)) + ((1 - p) * (r * (F . y)))) by A2, A4, A6, VALUED_1:def 5;

        hence thesis by A2, A4, A7, VALUED_1:def 5;

      end;

      assume

       A9: (r (#) F) is_convex_on X;

      then

       A10: X c= ( dom (r (#) F));

      hence X c= ( dom F) by VALUED_1:def 5;

      let p be Real;

      assume

       A11: 0 <= p & p <= 1;

      let x,y be Real;

      assume that

       A12: x in X and

       A13: y in X and

       A14: ((p * x) + ((1 - p) * y)) in X;

      ((r (#) F) . ((p * x) + ((1 - p) * y))) <= ((p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))) by A9, A11, A12, A13, A14;

      then (r * (F . ((p * x) + ((1 - p) * y)))) <= ((p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))) by A10, A14, VALUED_1:def 5;

      then (r * (F . ((p * x) + ((1 - p) * y)))) <= ((p * (r * (F . x))) + ((1 - p) * ((r (#) F) . y))) by A10, A12, VALUED_1:def 5;

      then (r * (F . ((p * x) + ((1 - p) * y)))) <= ((p * (r * (F . x))) + ((1 - p) * (r * (F . y)))) by A10, A13, VALUED_1:def 5;

      then ((r * (F . ((p * x) + ((1 - p) * y)))) / r) <= ((r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r) by A1, XREAL_1: 72;

      then (F . ((p * x) + ((1 - p) * y))) <= ((r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r) by A1, XCMPLX_1: 89;

      hence thesis by A1, XCMPLX_1: 89;

    end;

    theorem :: RFUNCT_3:57

    for F be PartFunc of REAL , REAL , X be set st X c= ( dom F) holds ( 0 (#) F) is_convex_on X

    proof

      let F be PartFunc of REAL , REAL , X be set;

      assume

       A1: X c= ( dom F);

      hence X c= ( dom ( 0 (#) F)) by VALUED_1:def 5;

      let p be Real;

      assume that 0 <= p and p <= 1;

      let x,y be Real;

      assume that

       A2: x in X and

       A3: y in X and

       A4: ((p * x) + ((1 - p) * y)) in X;

      

       A5: ( dom F) = ( dom ( 0 (#) F)) by VALUED_1:def 5;

      

      then

       A6: (( 0 (#) F) . ((p * x) + ((1 - p) * y))) = ( 0 * (F . ((p * x) + ((1 - p) * y)))) by A1, A4, VALUED_1:def 5

      .= 0 ;

      ((p * (( 0 (#) F) . x)) + ((1 - p) * (( 0 (#) F) . y))) = ((p * ( 0 * (F . x))) + ((1 - p) * (( 0 (#) F) . y))) by A1, A5, A2, VALUED_1:def 5

      .= ((p * 0 ) + ((1 - p) * ( 0 * (F . y)))) by A1, A5, A3, VALUED_1:def 5

      .= ( 0 + 0 );

      hence thesis by A6;

    end;

    theorem :: RFUNCT_3:58

    for F,G be PartFunc of REAL , REAL , X be set st F is_convex_on X & G is_convex_on X holds (F + G) is_convex_on X

    proof

      let F,G be PartFunc of REAL , REAL , X be set;

      

       A1: ( dom (F + G)) = (( dom F) /\ ( dom G)) by VALUED_1:def 1;

      assume

       A2: F is_convex_on X & G is_convex_on X;

      then X c= ( dom F) & X c= ( dom G);

      hence

       A3: X c= ( dom (F + G)) by A1, XBOOLE_1: 19;

      let p be Real;

      assume

       A4: 0 <= p & p <= 1;

      let x,y be Real;

      assume that

       A5: x in X and

       A6: y in X and

       A7: ((p * x) + ((1 - p) * y)) in X;

      (F . ((p * x) + ((1 - p) * y))) <= ((p * (F . x)) + ((1 - p) * (F . y))) & (G . ((p * x) + ((1 - p) * y))) <= ((p * (G . x)) + ((1 - p) * (G . y))) by A2, A4, A5, A6, A7;

      then ((F . ((p * x) + ((1 - p) * y))) + (G . ((p * x) + ((1 - p) * y)))) <= (((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y)))) by XREAL_1: 7;

      then

       A8: ((F + G) . ((p * x) + ((1 - p) * y))) <= (((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y)))) by A3, A7, VALUED_1:def 1;

      (((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y)))) = (((p * ((F . x) + (G . x))) + ((1 - p) * (F . y))) + ((1 - p) * (G . y)))

      .= (((p * ((F + G) . x)) + ((1 - p) * (F . y))) + ((1 - p) * (G . y))) by A3, A5, VALUED_1:def 1

      .= ((p * ((F + G) . x)) + ((1 - p) * ((F . y) + (G . y))));

      hence thesis by A3, A6, A8, VALUED_1:def 1;

    end;

    theorem :: RFUNCT_3:59

    

     Th59: for F be PartFunc of REAL , REAL , X be set, r st F is_convex_on X holds ( max+ (F - r)) is_convex_on X

    proof

      let F be PartFunc of REAL , REAL , X be set, r;

      assume

       A1: F is_convex_on X;

      then

       A2: X c= ( dom F);

      

       A3: ( dom F) = ( dom (F - r)) & ( dom ( max+ (F - r))) = ( dom (F - r)) by Def10, VALUED_1: 3;

      hence X c= ( dom ( max+ (F - r))) by A1;

      let p be Real;

      assume that

       A4: 0 <= p and

       A5: p <= 1;

      let x,y be Real;

      assume that

       A6: x in X and

       A7: y in X and

       A8: ((p * x) + ((1 - p) * y)) in X;

      (F . ((p * x) + ((1 - p) * y))) <= ((p * (F . x)) + ((1 - p) * (F . y))) by A1, A4, A5, A6, A7, A8;

      then ((F . ((p * x) + ((1 - p) * y))) - r) <= (((p * (F . x)) + ((1 - p) * (F . y))) - r) by XREAL_1: 9;

      then

       A9: ( max+ ((F . ((p * x) + ((1 - p) * y))) - r)) <= ( max ((((p * (F . x)) + ((1 - p) * (F . y))) - r), 0 )) by XXREAL_0: 26;

      ( 0 + p) <= 1 by A5;

      then 0 <= (1 - p) by XREAL_1: 19;

      then

       A10: ( max+ ((1 - p) * ((F - r) . y))) = ((1 - p) * ( max+ ((F - r) . y))) by Th4;

      

       A11: ( max+ ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)))) <= (( max+ (p * ((F - r) . x))) + ( max+ ((1 - p) * ((F - r) . y)))) by Th5;

      

       A12: ( max+ (p * ((F - r) . x))) = (p * ( max+ ((F - r) . x))) by A4, Th4;

      reconsider pc = ((p * x) + ((1 - p) * y)) as Element of REAL by XREAL_0:def 1;

      reconsider x, y as Element of REAL by XREAL_0:def 1;

      (((p * (F . x)) + ((1 - p) * (F . y))) - r) = ((p * ((F . x) - r)) + ((1 - p) * ((F . y) - r)))

      .= ((p * ((F - r) . x)) + ((1 - p) * ((F . y) - r))) by A6, A2, VALUED_1: 3

      .= ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) by A7, A2, VALUED_1: 3;

      then ( max+ ((F . ((p * x) + ((1 - p) * y))) - r)) <= ((p * ( max+ ((F - r) . x))) + ((1 - p) * ( max+ ((F - r) . y)))) by A9, A11, A12, A10, XXREAL_0: 2;

      then ( max+ ((F - r) . pc)) <= ((p * ( max+ ((F - r) . x))) + ((1 - p) * ( max+ ((F - r) . y)))) by A8, A2, VALUED_1: 3;

      then (( max+ (F - r)) . pc) <= ((p * ( max+ ((F - r) . x))) + ((1 - p) * ( max+ ((F - r) . y)))) by A3, A8, A2, Def10;

      then (( max+ (F - r)) . pc) <= ((p * (( max+ (F - r)) . x)) + ((1 - p) * ( max+ ((F - r) . y)))) by A3, A6, A2, Def10;

      hence thesis by A3, A7, A2, Def10;

    end;

    theorem :: RFUNCT_3:60

    for F be PartFunc of REAL , REAL , X be set st F is_convex_on X holds ( max+ F) is_convex_on X

    proof

      let F be PartFunc of REAL , REAL , X be set;

      assume F is_convex_on X;

      then ( max+ (F - 0 )) is_convex_on X by Th59;

      hence thesis by Th48;

    end;

    theorem :: RFUNCT_3:61

    

     Th61: ( id ( [#] REAL )) is_convex_on REAL

    proof

      set i = ( id ( [#] REAL ));

      thus REAL c= ( dom i) by FUNCT_1: 17;

      let p be Real;

      assume that 0 <= p and p <= 1;

      let x,y be Real;

      assume that

       A1: x in REAL and

       A2: y in REAL and

       A3: ((p * x) + ((1 - p) * y)) in REAL ;

      (i . x) = x & (i . y) = y by A1, A2, FUNCT_1: 17;

      hence thesis by A3, FUNCT_1: 17;

    end;

    theorem :: RFUNCT_3:62

    for r be Real holds ( max+ (( id ( [#] REAL )) - r)) is_convex_on REAL by Th59, Th61;

    definition

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      assume

       A1: ( dom (F | X)) is finite;

      :: RFUNCT_3:def13

      func FinS (F,X) -> non-increasing FinSequence of REAL means

      : Def13: ((F | X),it ) are_fiberwise_equipotent ;

      existence

      proof

        set x = ( dom (F | X));

        consider b be FinSequence such that

         A2: ((F | x),b) are_fiberwise_equipotent by A1, RFINSEQ: 5;

        ( rng (F | x)) = ( rng b) by A2, CLASSES1: 75;

        then

        reconsider b as FinSequence of REAL by FINSEQ_1:def 4;

        consider a be non-increasing FinSequence of REAL such that

         A3: (b,a) are_fiberwise_equipotent by RFINSEQ: 22;

        take a;

        x = (( dom F) /\ X) by RELAT_1: 61;

        

        then (F | x) = ((F | ( dom F)) | X) by RELAT_1: 71

        .= (F | X) by RELAT_1: 68;

        hence thesis by A2, A3, CLASSES1: 76;

      end;

      uniqueness by CLASSES1: 76, RFINSEQ: 23;

    end

    theorem :: RFUNCT_3:63

    

     Th63: for D be non empty set, F be PartFunc of D, REAL , X be set st ( dom (F | X)) is finite holds ( FinS (F,( dom (F | X)))) = ( FinS (F,X))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      

       A1: (F | ( dom (F | X))) = (F | (( dom F) /\ X)) by RELAT_1: 61

      .= ((F | ( dom F)) | X) by RELAT_1: 71

      .= (F | X) by RELAT_1: 68;

      assume

       A2: ( dom (F | X)) is finite;

      then (( FinS (F,X)),(F | X)) are_fiberwise_equipotent by Def13;

      hence thesis by A2, A1, Def13;

    end;

    theorem :: RFUNCT_3:64

    

     Th64: for D be non empty set, F be PartFunc of D, REAL , X be set st ( dom (F | X)) is finite holds ( FinS ((F | X),X)) = ( FinS (F,X))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      

       A1: ((F | X) | X) = (F | X) by RELAT_1: 72;

      assume

       A2: ( dom (F | X)) is finite;

      then (( FinS (F,X)),(F | X)) are_fiberwise_equipotent by Def13;

      hence thesis by A2, A1, Def13;

    end;

    theorem :: RFUNCT_3:65

    

     Th65: for D be non empty set, d be Element of D, X be set, F be PartFunc of D, REAL st X is finite & d in ( dom (F | X)) holds ((( FinS (F,(X \ {d}))) ^ <*(F . d)*>),(F | X)) are_fiberwise_equipotent

    proof

      for D be non empty set, X be finite set, F be PartFunc of D, REAL , x be object st x in ( dom (F | X)) holds ((( FinS (F,(X \ {x}))) ^ <*(F . x)*>),(F | X)) are_fiberwise_equipotent

      proof

        let D be non empty set, X be finite set, F be PartFunc of D, REAL , x be object;

        set Y = (X \ {x});

        set A = (( FinS (F,Y)) ^ <*(F . x)*>);

        assume x in ( dom (F | X));

        then

         A1: x in (( dom F) /\ X) by RELAT_1: 61;

        then x in X by XBOOLE_0:def 4;

        then

         A2: {x} c= X by ZFMISC_1: 31;

        x in ( dom F) by A1, XBOOLE_0:def 4;

        then

         A3: {x} c= ( dom F) by ZFMISC_1: 31;

        ( dom (F | Y)) is finite;

        then

         A4: ((F | Y),( FinS (F,Y))) are_fiberwise_equipotent by Def13;

        now

          let y be object;

          

           A5: Y misses {x} by XBOOLE_1: 79;

          

           A6: ( card ( Coim ((F | Y),y))) = ( card ( Coim (( FinS (F,Y)),y))) by A4, CLASSES1:def 10;

          

           A7: ( dom (F | {x})) = {x} by A3, RELAT_1: 62;

          

           A8: ( dom <*(F . x)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

           A9:

          now

            per cases ;

              case

               A10: y = (F . x);

              

               A11: {x} c= ((F | {x}) " {y})

              proof

                let z be object;

                

                 A12: y in {y} by TARSKI:def 1;

                assume

                 A13: z in {x};

                then z = x by TARSKI:def 1;

                then y = ((F | {x}) . z) by A7, A10, A13, FUNCT_1: 47;

                hence thesis by A7, A13, A12, FUNCT_1:def 7;

              end;

              ((F | {x}) " {y}) c= {x} by A7, RELAT_1: 132;

              then ((F | {x}) " {y}) = {x} by A11;

              then

               A14: ( card ((F | {x}) " {y})) = 1 by CARD_1: 30;

              

               A15: {1} c= ( <*(F . x)*> " {y})

              proof

                let z be object;

                

                 A16: y in {y} by TARSKI:def 1;

                assume

                 A17: z in {1};

                then z = 1 by TARSKI:def 1;

                then y = ( <*(F . x)*> . z) by A10, FINSEQ_1: 40;

                hence thesis by A8, A17, A16, FUNCT_1:def 7;

              end;

              ( <*(F . x)*> " {y}) c= {1} by A8, RELAT_1: 132;

              then ( <*(F . x)*> " {y}) = {1} by A15;

              hence ( card ((F | {x}) " {y})) = ( card ( <*(F . x)*> " {y})) by A14, CARD_1: 30;

            end;

              case

               A18: y <> (F . x);

               A19:

              now

                set z = the Element of ( <*(F . x)*> " {y});

                assume

                 A20: ( <*(F . x)*> " {y}) <> {} ;

                then ( <*(F . x)*> . z) in {y} by FUNCT_1:def 7;

                then

                 A21: ( <*(F . x)*> . z) = y by TARSKI:def 1;

                z in {1} by A8, A20, FUNCT_1:def 7;

                then z = 1 by TARSKI:def 1;

                hence contradiction by A18, A21, FINSEQ_1: 40;

              end;

              now

                set z = the Element of ((F | {x}) " {y});

                assume

                 A22: ((F | {x}) " {y}) <> {} ;

                then ((F | {x}) . z) in {y} by FUNCT_1:def 7;

                then

                 A23: ((F | {x}) . z) = y by TARSKI:def 1;

                

                 A24: z in {x} by A7, A22, FUNCT_1:def 7;

                then z = x by TARSKI:def 1;

                hence contradiction by A7, A18, A24, A23, FUNCT_1: 47;

              end;

              hence ( card ((F | {x}) " {y})) = ( card ( <*(F . x)*> " {y})) by A19;

            end;

          end;

          

           A25: (((F | Y) " {y}) \/ ((F | {x}) " {y})) = ((Y /\ (F " {y})) \/ ((F | {x}) " {y})) by FUNCT_1: 70

          .= ((Y /\ (F " {y})) \/ ( {x} /\ (F " {y}))) by FUNCT_1: 70

          .= ((Y \/ {x}) /\ (F " {y})) by XBOOLE_1: 23

          .= ((X \/ {x}) /\ (F " {y})) by XBOOLE_1: 39

          .= (X /\ (F " {y})) by A2, XBOOLE_1: 12

          .= ((F | X) " {y}) by FUNCT_1: 70;

          (((F | Y) " {y}) /\ ((F | {x}) " {y})) = ((Y /\ (F " {y})) /\ ((F | {x}) " {y})) by FUNCT_1: 70

          .= ((Y /\ (F " {y})) /\ ( {x} /\ (F " {y}))) by FUNCT_1: 70

          .= ((((F " {y}) /\ Y) /\ {x}) /\ (F " {y})) by XBOOLE_1: 16

          .= (((F " {y}) /\ (Y /\ {x})) /\ (F " {y})) by XBOOLE_1: 16

          .= ( {} /\ (F " {y})) by A5

          .= {} ;

          

          hence ( card ( Coim ((F | X),y))) = ((( card ((F | Y) " {y})) + ( card ( <*(F . x)*> " {y}))) - ( card {} )) by A25, A9, CARD_2: 45

          .= ( card ( Coim (A,y))) by A6, FINSEQ_3: 57;

        end;

        hence thesis by CLASSES1:def 10;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_3:66

    

     Th66: for D be non empty set, d be Element of D, X be set, F be PartFunc of D, REAL st ( dom (F | X)) is finite & d in ( dom (F | X)) holds ((( FinS (F,(X \ {d}))) ^ <*(F . d)*>),(F | X)) are_fiberwise_equipotent

    proof

      let D be non empty set, d be Element of D, X be set, F be PartFunc of D, REAL ;

      set dx = ( dom (F | X));

      assume that

       A1: dx is finite and

       A2: d in dx;

      set Y = (X \ {d}), dy = ( dom (F | Y));

      

       A3: dy = (( dom F) /\ Y) by RELAT_1: 61;

      

       A4: dx = (( dom F) /\ X) by RELAT_1: 61;

      

       A5: dy = (dx \ {d})

      proof

        thus dy c= (dx \ {d})

        proof

          let y be object;

          assume

           A6: y in dy;

          then y in (X \ {d}) by A3, XBOOLE_0:def 4;

          then

           A7: not y in {d} by XBOOLE_0:def 5;

          y in ( dom F) by A3, A6, XBOOLE_0:def 4;

          then y in dx by A3, A4, A6, XBOOLE_0:def 4;

          hence thesis by A7, XBOOLE_0:def 5;

        end;

        let y be object;

        assume

         A8: y in (dx \ {d});

        then

         A9: not y in {d} by XBOOLE_0:def 5;

        

         A10: y in dx by A8, XBOOLE_0:def 5;

        then y in X by A4, XBOOLE_0:def 4;

        then

         A11: y in Y by A9, XBOOLE_0:def 5;

        y in ( dom F) by A4, A10, XBOOLE_0:def 4;

        hence thesis by A3, A11, XBOOLE_0:def 4;

      end;

      (F | dx) = (F | (( dom F) /\ X)) by RELAT_1: 61

      .= ((F | ( dom F)) | X) by RELAT_1: 71

      .= (F | X) by RELAT_1: 68;

      then ((( FinS (F,(dx \ {d}))) ^ <*(F . d)*>),(F | X)) are_fiberwise_equipotent by A1, A2, Th65;

      hence thesis by A1, A5, Th63;

    end;

    theorem :: RFUNCT_3:67

    

     Th67: for D be non empty set, F be PartFunc of D, REAL , X be set, Y be finite set st Y = ( dom (F | X)) holds ( len ( FinS (F,X))) = ( card Y)

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      let Y be finite set;

      reconsider fs = ( dom ( FinS (F,X))) as finite set;

      

       A1: ( dom ( FinS (F,X))) = ( Seg ( len ( FinS (F,X)))) by FINSEQ_1:def 3;

      assume

       A2: Y = ( dom (F | X));

      (( FinS (F,X)),(F | X)) are_fiberwise_equipotent by A2, Def13;

      

      hence ( card Y) = ( card fs) by A2, CLASSES1: 81

      .= ( len ( FinS (F,X))) by A1, FINSEQ_1: 57;

    end;

    theorem :: RFUNCT_3:68

    

     Th68: for D be non empty set, F be PartFunc of D, REAL holds ( FinS (F, {} )) = ( <*> REAL )

    proof

      let D be non empty set, F be PartFunc of D, REAL ;

      ( dom (F | {} )) = (( dom F) /\ {} ) by RELAT_1: 61

      .= {} ;

      then ( len ( FinS (F, {} ))) = 0 by Th67, CARD_1: 27;

      hence thesis;

    end;

    theorem :: RFUNCT_3:69

    

     Th69: for D be non empty set, F be PartFunc of D, REAL , d be Element of D st d in ( dom F) holds ( FinS (F, {d})) = <*(F . d)*>

    proof

      let D be non empty set, F be PartFunc of D, REAL , d be Element of D;

      assume d in ( dom F);

      then {d} c= ( dom F) by ZFMISC_1: 31;

      

      then

       A1: {d} = (( dom F) /\ {d}) by XBOOLE_1: 28

      .= ( dom (F | {d})) by RELAT_1: 61;

      then (( FinS (F, {d})),(F | {d})) are_fiberwise_equipotent by Def13;

      then

       A2: ( rng ( FinS (F, {d}))) = ( rng (F | {d})) by CLASSES1: 75;

      

       A3: ( rng (F | {d})) = {(F . d)}

      proof

        thus ( rng (F | {d})) c= {(F . d)}

        proof

          let x be object;

          assume x in ( rng (F | {d}));

          then

          consider e be Element of D such that

           A4: e in ( dom (F | {d})) and

           A5: ((F | {d}) . e) = x by PARTFUN1: 3;

          e = d by A1, A4, TARSKI:def 1;

          then x = (F . d) by A4, A5, FUNCT_1: 47;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        

         A6: d in ( dom (F | {d})) by A1, TARSKI:def 1;

        assume x in {(F . d)};

        then x = (F . d) by TARSKI:def 1;

        then x = ((F | {d}) . d) by A6, FUNCT_1: 47;

        hence thesis by A6, FUNCT_1:def 3;

      end;

      ( len ( FinS (F, {d}))) = ( card {d}) by A1, Th67

      .= 1 by CARD_1: 30;

      hence thesis by A2, A3, FINSEQ_1: 39;

    end;

    theorem :: RFUNCT_3:70

    

     Th70: for D be non empty set, F be PartFunc of D, REAL , X be set, d be Element of D st ( dom (F | X)) is finite & d in ( dom (F | X)) & (( FinS (F,X)) . ( len ( FinS (F,X)))) = (F . d) holds ( FinS (F,X)) = (( FinS (F,(X \ {d}))) ^ <*(F . d)*>)

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set, d be Element of D;

      set dx = ( dom (F | X)), fx = ( FinS (F,X)), fy = ( FinS (F,(X \ {d})));

      assume that

       A1: dx is finite and

       A2: d in dx and

       A3: (fx . ( len fx)) = (F . d);

      

       A4: (fx,(F | X)) are_fiberwise_equipotent by A1, Def13;

      then ( rng fx) = ( rng (F | X)) by CLASSES1: 75;

      then fx <> {} by A2, FUNCT_1: 3, RELAT_1: 38;

      then ( 0 + 1) <= ( len fx) by NAT_1: 13;

      then ( max ( 0 ,(( len fx) - 1))) = (( len fx) - 1) by FINSEQ_2: 4;

      then

      reconsider n = (( len fx) - 1) as Element of NAT by FINSEQ_2: 5;

      ( len fx) = (n + 1);

      then

       A5: fx = ((fx | n) ^ <*(F . d)*>) by A3, RFINSEQ: 7;

      

       A6: (fx | n) is non-increasing by RFINSEQ: 20;

      ((fy ^ <*(F . d)*>),(F | X)) are_fiberwise_equipotent by A1, A2, Th66;

      then (fx,(fy ^ <*(F . d)*>)) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then (fy,(fx | n)) are_fiberwise_equipotent by A5, RFINSEQ: 1;

      hence thesis by A5, A6, RFINSEQ: 23;

    end;

    defpred P[ Nat] means for D be non empty set, F be PartFunc of D, REAL , X be set holds for Y be set, Z be finite set st Z = ( dom (F | Y)) & ( dom (F | X)) is finite & Y c= X & $1 = ( card Z) & (for d1,d2 be Element of D st d1 in ( dom (F | Y)) & d2 in ( dom (F | (X \ Y))) holds (F . d1) >= (F . d2)) holds ( FinS (F,X)) = (( FinS (F,Y)) ^ ( FinS (F,(X \ Y))));

    

     Lm3: P[ 0 ]

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      let Y be set;

      let Z be finite set such that

       A1: Z = ( dom (F | Y));

      assume that

       A2: ( dom (F | X)) is finite and Y c= X and

       A3: 0 = ( card Z) and for d1,d2 be Element of D st d1 in ( dom (F | Y)) & d2 in ( dom (F | (X \ Y))) holds (F . d1) >= (F . d2);

      

       A4: ( dom (F | Y)) = {} by A1, A3;

      

       A5: ( dom (F | (X \ Y))) = (( dom F) /\ (X \ Y)) by RELAT_1: 61;

      ( dom (F | X)) = (( dom F) /\ X) & ( dom (F | Y)) = (( dom F) /\ Y) by RELAT_1: 61;

      

      then ( dom (F | (X \ Y))) = (( dom (F | X)) \ {} ) by A5, A4, XBOOLE_1: 50

      .= ( dom (F | X));

      

      then

       A6: ( FinS (F,(X \ Y))) = ( FinS (F,( dom (F | X)))) by A2, Th63

      .= ( FinS (F,X)) by A2, Th63;

      ( FinS (F,Y)) = ( FinS (F, {} )) by A4, Th63

      .= {} by Th68;

      hence thesis by A6, FINSEQ_1: 34;

    end;

    

     Lm4: for n st P[n] holds P[(n + 1)]

    proof

      let n;

      assume

       A1: P[n];

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      let Y be set;

      set dx = ( dom (F | X)), dxy = ( dom (F | (X \ Y))), fy = ( FinS (F,Y)), fxy = ( FinS (F,(X \ Y)));

      let dy be finite set such that

       A2: dy = ( dom (F | Y)) and

       A3: ( dom (F | X)) is finite and

       A4: Y c= X and

       A5: (n + 1) = ( card dy) and

       A6: for d1,d2 be Element of D st d1 in ( dom (F | Y)) & d2 in dxy holds (F . d1) >= (F . d2);

      

       A7: ( len fy) = (n + 1) by A2, A5, Th67;

      

       A8: ((F | Y),fy) are_fiberwise_equipotent by A2, Def13;

      then

       A9: ( rng fy) = ( rng (F | Y)) by CLASSES1: 75;

      ( 0 + 1) <= (n + 1) by NAT_1: 13;

      then

       A10: ( len fy) in ( dom fy) by A7, FINSEQ_3: 25;

      then (fy . ( len fy)) in ( rng fy) by FUNCT_1:def 3;

      then

      consider d be Element of D such that

       A11: d in dy and

       A12: ((F | Y) . d) = (fy . ( len fy)) by A2, A9, PARTFUN1: 3;

      

       A13: dxy = (( dom F) /\ (X \ Y)) by RELAT_1: 61;

      

       A14: dy = (( dom F) /\ Y) by A2, RELAT_1: 61;

      then

       A15: d in Y by A11, XBOOLE_0:def 4;

      then

       A16: {d} c= X by A4, ZFMISC_1: 31;

      

       A17: d in ( dom F) by A14, A11, XBOOLE_0:def 4;

      then

       A18: {d} c= ( dom F) by ZFMISC_1: 31;

      

       A19: {d} c= Y by A15, ZFMISC_1: 31;

      

       A20: ((fxy ^ <*(F . d)*>),( <*(F . d)*> ^ fxy)) are_fiberwise_equipotent by RFINSEQ: 2;

      set Yd = (Y \ {d}), dyd = ( dom (F | Yd)), xyd = ( dom (F | (X \ Yd)));

      

       A21: xyd = (( dom F) /\ (X \ Yd)) by RELAT_1: 61;

      

       A22: dyd = (( dom F) /\ Yd) by RELAT_1: 61;

      

       A23: dyd = (dy \ {d})

      proof

        thus dyd c= (dy \ {d})

        proof

          let y be object;

          assume

           A24: y in dyd;

          then y in (Y \ {d}) by A22, XBOOLE_0:def 4;

          then

           A25: not y in {d} by XBOOLE_0:def 5;

          y in ( dom F) by A22, A24, XBOOLE_0:def 4;

          then y in dy by A14, A22, A24, XBOOLE_0:def 4;

          hence thesis by A25, XBOOLE_0:def 5;

        end;

        let y be object;

        assume

         A26: y in (dy \ {d});

        then ( not y in {d}) & y in Y by A14, XBOOLE_0:def 4, XBOOLE_0:def 5;

        then

         A27: y in Yd by XBOOLE_0:def 5;

        y in ( dom F) by A14, A26, XBOOLE_0:def 4;

        hence thesis by A22, A27, XBOOLE_0:def 4;

      end;

      

       A28: (F . d) = (fy . ( len fy)) by A2, A11, A12, FUNCT_1: 47;

      then

       A29: fy = ((fy | n) ^ <*(F . d)*>) by A7, RFINSEQ: 7;

      reconsider dyd as finite set by A23;

      

       A30: (X \ Yd) = ((X \ Y) \/ (X /\ {d})) by XBOOLE_1: 52

      .= ((X \ Y) \/ {d}) by A16, XBOOLE_1: 28;

      

      then

       A31: xyd = (dxy \/ (( dom F) /\ {d})) by A13, A21, XBOOLE_1: 23

      .= (dxy \/ {d}) by A18, XBOOLE_1: 28;

       A32:

      now

        let d1,d2 be Element of D;

        assume that

         A33: d1 in dyd and

         A34: d2 in xyd;

        now

          per cases by A31, A34, XBOOLE_0:def 3;

            case d2 in dxy;

            hence (F . d1) >= (F . d2) by A2, A6, A23, A33;

          end;

            case d2 in {d};

            then

             A35: d2 = d by TARSKI:def 1;

            ((F | Y) . d1) in ( rng (F | Y)) by A2, A23, A33, FUNCT_1:def 3;

            then (F . d1) in ( rng (F | Y)) by A2, A23, A33, FUNCT_1: 47;

            then

            consider m be Nat such that

             A36: m in ( dom fy) and

             A37: (fy . m) = (F . d1) by A9, FINSEQ_2: 10;

            

             A38: m <= ( len fy) by A36, FINSEQ_3: 25;

            now

              per cases ;

                case m = ( len fy);

                hence (F . d1) >= (F . d2) by A2, A11, A12, A35, A37, FUNCT_1: 47;

              end;

                case m <> ( len fy);

                then m < ( len fy) by A38, XXREAL_0: 1;

                hence (F . d1) >= (F . d2) by A10, A28, A35, A36, A37, RFINSEQ: 19;

              end;

            end;

            hence (F . d1) >= (F . d2);

          end;

        end;

        hence (F . d1) >= (F . d2);

      end;

      dx = (( dom F) /\ X) by RELAT_1: 61;

      then

       A39: dxy is finite by A3, A13, FINSET_1: 1, XBOOLE_1: 26;

      then ((F | (X \ Y)),fxy) are_fiberwise_equipotent by Def13;

      then

       A40: ( rng fxy) = ( rng (F | (X \ Y))) by CLASSES1: 75;

      

       A41: ( <*(F . d)*> ^ fxy) is non-increasing

      proof

        set xfy = ( <*(F . d)*> ^ fxy);

        let n;

        assume that

         A42: n in ( dom ( <*(F . d)*> ^ fxy)) and

         A43: (n + 1) in ( dom ( <*(F . d)*> ^ fxy));

        

         A44: 1 <= n by A42, FINSEQ_3: 25;

        then ( max ( 0 ,(n - 1))) = (n - 1) by FINSEQ_2: 4;

        then

        reconsider n1 = (n - 1) as Element of NAT by FINSEQ_2: 5;

        set r = (xfy . n), s = (xfy . (n + 1));

        

         A45: ( len <*(F . d)*>) = 1 by FINSEQ_1: 40;

        then ( len xfy) = (1 + ( len fxy)) by FINSEQ_1: 22;

        then

         A46: ( len fxy) = (( len xfy) - 1);

        

         A47: (n + 1) <= ( len xfy) by A43, FINSEQ_3: 25;

        then (n1 + 1) <= ( len fxy) by A46, XREAL_1: 19;

        then

         A48: (n1 + 1) in ( dom fxy) by A44, FINSEQ_3: 25;

        then (fxy . (n1 + 1)) in ( rng fxy) by FUNCT_1:def 3;

        then

        consider d1 be Element of D such that

         A49: d1 in dxy & ((F | (X \ Y)) . d1) = (fxy . (n1 + 1)) by A40, PARTFUN1: 3;

        1 < (n + 1) by A44, NAT_1: 13;

        

        then

         A50: (xfy . (n + 1)) = (fxy . ((n + 1) - 1)) by A45, A47, FINSEQ_1: 24

        .= (fxy . (n1 + 1));

        

         A51: n <= ( len xfy) by A42, FINSEQ_3: 25;

        then

         A52: n1 <= ( len fxy) by A46, XREAL_1: 9;

        

         A53: (F . d1) = (fxy . (n1 + 1)) & (F . d) >= (F . d1) by A2, A6, A11, A49, FUNCT_1: 47;

        now

          per cases ;

            suppose n = 1;

            hence r >= s by A50, A53, FINSEQ_1: 41;

          end;

            suppose n <> 1;

            then

             A54: 1 < n by A44, XXREAL_0: 1;

            then (1 + 1) <= n by NAT_1: 13;

            then 1 <= n1 by XREAL_1: 19;

            then

             A55: n1 in ( dom fxy) by A52, FINSEQ_3: 25;

            (xfy . n) = (fxy . n1) by A45, A51, A54, FINSEQ_1: 24;

            hence r >= s by A48, A50, A55, RFINSEQ:def 3;

          end;

        end;

        hence r >= s;

      end;

      

       A56: ( <*(F . d)*> ^ fxy) is FinSequence of REAL by RVSUM_1: 145;

      d in {d} by TARSKI:def 1;

      then d in (X \ Yd) by A30, XBOOLE_0:def 3;

      then

       A57: d in xyd by A21, A17, XBOOLE_0:def 4;

      ((X \ Yd) \ {d}) = (X \ (Yd \/ {d})) by XBOOLE_1: 41

      .= (X \ (Y \/ {d})) by XBOOLE_1: 39

      .= (X \ Y) by A19, XBOOLE_1: 12;

      then ((fxy ^ <*(F . d)*>),(F | (X \ Yd))) are_fiberwise_equipotent by A39, A31, A57, Th66;

      then (( <*(F . d)*> ^ fxy),(F | (X \ Yd))) are_fiberwise_equipotent by A20, CLASSES1: 76;

      then

       A58: ( <*(F . d)*> ^ fxy) = ( FinS (F,(X \ Yd))) by A39, A31, A41, Def13, A56;

       {d} c= dy by A11, ZFMISC_1: 31;

      

      then ( card dyd) = (( card dy) - ( card {d})) by A23, CARD_2: 44

      .= ((n + 1) - 1) by A5, CARD_1: 30

      .= n;

      then ( FinS (F,X)) = (( FinS (F,Yd)) ^ ( FinS (F,(X \ Yd)))) by A1, A3, A4, A32, XBOOLE_1: 1;

      then

       A59: ( FinS (F,X)) = ((( FinS (F,Yd)) ^ <*(F . d)*>) ^ fxy) by A58, FINSEQ_1: 32;

      

       A60: (fy | n) is non-increasing by RFINSEQ: 20;

      ((F | Y),(( FinS (F,Yd)) ^ <*(F . d)*>)) are_fiberwise_equipotent by A2, A11, Th66;

      then ((( FinS (F,Yd)) ^ <*(F . d)*>),fy) are_fiberwise_equipotent by A8, CLASSES1: 76;

      then (( FinS (F,Yd)),(fy | n)) are_fiberwise_equipotent by A29, RFINSEQ: 1;

      hence thesis by A59, A29, A60, RFINSEQ: 23;

    end;

    theorem :: RFUNCT_3:71

    for D be non empty set, F be PartFunc of D, REAL , X,Y be set st ( dom (F | X)) is finite & Y c= X & (for d1,d2 be Element of D st d1 in ( dom (F | Y)) & d2 in ( dom (F | (X \ Y))) holds (F . d1) >= (F . d2)) holds ( FinS (F,X)) = (( FinS (F,Y)) ^ ( FinS (F,(X \ Y))))

    proof

      

       A1: for n holds P[n] from NAT_1:sch 2( Lm3, Lm4);

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      let Y be set;

      assume that

       A2: ( dom (F | X)) is finite and

       A3: Y c= X and

       A4: for d1,d2 be Element of D st d1 in ( dom (F | Y)) & d2 in ( dom (F | (X \ Y))) holds (F . d1) >= (F . d2);

      (F | Y) c= (F | X) by A3, RELAT_1: 75;

      then

      reconsider dFY = ( dom (F | Y)) as finite set by A2, FINSET_1: 1, RELAT_1: 11;

      ( card dFY) = ( card dFY);

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: RFUNCT_3:72

    

     Th72: for D be non empty set, F be PartFunc of D, REAL , r be Real, X be set, d be Element of D st ( dom (F | X)) is finite & d in ( dom (F | X)) holds (( FinS ((F - r),X)) . ( len ( FinS ((F - r),X)))) = ((F - r) . d) iff (( FinS (F,X)) . ( len ( FinS (F,X)))) = (F . d)

    proof

      let D be non empty set, F be PartFunc of D, REAL , r be Real, X be set, d be Element of D;

      set dx = ( dom (F | X)), drx = ( dom ((F - r) | X)), frx = ( FinS ((F - r),X)), fx = ( FinS (F,X));

      assume that

       A1: dx is finite and

       A2: d in dx;

      reconsider dx as finite set by A1;

      

       A3: drx = (( dom (F - r)) /\ X) by RELAT_1: 61

      .= (( dom F) /\ X) by VALUED_1: 3

      .= dx by RELAT_1: 61;

      then (fx,(F | X)) are_fiberwise_equipotent by Def13;

      then

       A4: ( rng fx) = ( rng (F | X)) by CLASSES1: 75;

      then fx <> {} by A2, FUNCT_1: 3, RELAT_1: 38;

      then ( 0 + 1) <= ( len fx) by NAT_1: 13;

      then

       A5: ( len fx) in ( dom fx) by FINSEQ_3: 25;

      ((F | X) . d) in ( rng (F | X)) by A2, FUNCT_1:def 3;

      then (F . d) in ( rng (F | X)) by A2, FUNCT_1: 47;

      then

      consider n be Nat such that

       A6: n in ( dom fx) and

       A7: (fx . n) = (F . d) by A4, FINSEQ_2: 10;

      

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

      (frx,((F - r) | X)) are_fiberwise_equipotent by A3, Def13;

      then

       A9: ( rng frx) = ( rng ((F - r) | X)) by CLASSES1: 75;

      

       A10: ( len fx) = ( card dx) & ( dom frx) = ( Seg ( len frx)) by Th67, FINSEQ_1:def 3;

      

       A11: ( len frx) = ( card dx) by A3, Th67;

      then (frx . ( len frx)) in ( rng frx) by A10, A8, A5, FUNCT_1:def 3;

      then

      consider d1 be Element of D such that

       A12: d1 in drx and

       A13: (((F - r) | X) . d1) = (frx . ( len frx)) by A9, PARTFUN1: 3;

      ((F | X) . d1) = (F . d1) by A3, A12, FUNCT_1: 47;

      then (F . d1) in ( rng (F | X)) by A3, A12, FUNCT_1:def 3;

      then

      consider m be Nat such that

       A14: m in ( dom fx) and

       A15: (fx . m) = (F . d1) by A4, FINSEQ_2: 10;

      

       A16: ( dom (F - r)) = ( dom F) by VALUED_1: 3;

      

       A17: drx = (( dom (F - r)) /\ X) by RELAT_1: 61;

      then

       A18: d1 in ( dom (F - r)) by A12, XBOOLE_0:def 4;

      

       A19: (frx . ( len frx)) = ((F - r) . d1) by A12, A13, FUNCT_1: 47

      .= ((F . d1) - r) by A16, A18, VALUED_1: 3;

      

       A20: d in ( dom (F - r)) by A2, A3, A17, XBOOLE_0:def 4;

      then

       A21: ((F - r) . d) = ((F . d) - r) by A16, VALUED_1: 3;

      

       A22: n <= ( len fx) by A6, FINSEQ_3: 25;

      thus (frx . ( len frx)) = ((F - r) . d) implies (fx . ( len fx)) = (F . d)

      proof

        (fx . ( len fx)) in ( rng fx) by A5, FUNCT_1:def 3;

        then

        consider d1 be Element of D such that

         A23: d1 in dx and

         A24: ((F | X) . d1) = (fx . ( len fx)) by A4, PARTFUN1: 3;

        

         A25: d1 in ( dom (F - r)) by A3, A17, A23, XBOOLE_0:def 4;

        

         A26: (F . d1) = (fx . ( len fx)) by A23, A24, FUNCT_1: 47;

        (((F - r) | X) . d1) = ((F - r) . d1) by A3, A23, FUNCT_1: 47

        .= ((F . d1) - r) by A16, A25, VALUED_1: 3;

        then ((F . d1) - r) in ( rng ((F - r) | X)) by A3, A23, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A27: m in ( dom frx) and

         A28: (frx . m) = ((F . d1) - r) by A9, FINSEQ_2: 10;

        

         A29: m <= ( len frx) by A27, FINSEQ_3: 25;

        assume that

         A30: (frx . ( len frx)) = ((F - r) . d) and

         A31: (fx . ( len fx)) <> (F . d);

        n < ( len fx) by A7, A22, A31, XXREAL_0: 1;

        then

         A32: (F . d) >= (F . d1) by A5, A6, A7, A26, RFINSEQ: 19;

        now

          per cases ;

            case ( len frx) = m;

            then ((F . d1) + ( - r)) = ((F . d) - r) by A16, A20, A30, A28, VALUED_1: 3;

            hence contradiction by A31, A23, A24, FUNCT_1: 47;

          end;

            case ( len frx) <> m;

            then m < ( len frx) by A29, XXREAL_0: 1;

            then ((F . d1) - r) >= ((F . d) - r) by A11, A10, A8, A21, A5, A30, A27, A28, RFINSEQ: 19;

            then (F . d1) >= (F . d) by XREAL_1: 9;

            hence contradiction by A31, A26, A32, XXREAL_0: 1;

          end;

        end;

        hence contradiction;

      end;

      assume that

       A33: (fx . ( len fx)) = (F . d) and

       A34: (frx . ( len frx)) <> ((F - r) . d);

      (((F - r) | X) . d) in ( rng ((F - r) | X)) by A2, A3, FUNCT_1:def 3;

      then ((F - r) . d) in ( rng ((F - r) | X)) by A2, A3, FUNCT_1: 47;

      then

      consider n1 be Nat such that

       A35: n1 in ( dom frx) and

       A36: (frx . n1) = ((F . d) - r) by A9, A21, FINSEQ_2: 10;

      n1 <= ( len frx) by A35, FINSEQ_3: 25;

      then n1 < ( len frx) by A21, A34, A36, XXREAL_0: 1;

      then ((F . d) - r) >= ((F . d1) - r) by A11, A10, A8, A5, A19, A35, A36, RFINSEQ: 19;

      then

       A37: (F . d) >= (F . d1) by XREAL_1: 9;

      

       A38: m <= ( len fx) by A14, FINSEQ_3: 25;

      now

        per cases ;

          case ( len fx) = m;

          hence contradiction by A16, A20, A33, A34, A19, A15, VALUED_1: 3;

        end;

          case ( len fx) <> m;

          then m < ( len fx) by A38, XXREAL_0: 1;

          then (F . d1) >= (F . d) by A5, A33, A14, A15, RFINSEQ: 19;

          hence contradiction by A21, A34, A19, A37, XXREAL_0: 1;

        end;

      end;

      hence contradiction;

    end;

    theorem :: RFUNCT_3:73

    

     Th73: for D be non empty set, F be PartFunc of D, REAL , r be Real, X be set, Z be finite set st Z = ( dom (F | X)) holds ( FinS ((F - r),X)) = (( FinS (F,X)) - (( card Z) |-> r))

    proof

      let D be non empty set, F be PartFunc of D, REAL , r be Real;

      let X be set;

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

      defpred P[ Nat] means for X be set, G be finite set st G = ( dom (F | X)) & $1 = ( card G) holds ( FinS ((F - r),X)) = (( FinS (F,X)) - (( card G) |-> r));

      

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

      proof

        let n;

        assume

         A2: P[n];

        let X be set, G be finite set;

        assume

         A3: G = ( dom (F | X));

        set frx = ( FinS ((F - rr),X)), fx = ( FinS (F,X));

        

         A4: ( dom ((F - r) | X)) = (( dom (F - r)) /\ X) by RELAT_1: 61

        .= (( dom F) /\ X) by VALUED_1: 3

        .= ( dom (F | X)) by RELAT_1: 61;

        then

         A5: ( len frx) = ( card G) by A3, Th67;

        

         A6: (( FinS ((F - r),X)),((F - r) | X)) are_fiberwise_equipotent by A3, A4, Def13;

        then

         A7: ( rng ( FinS ((F - r),X))) = ( rng ((F - r) | X)) by CLASSES1: 75;

        assume

         A8: (n + 1) = ( card G);

        then

         A9: ( len fx) = (n + 1) by A3, Th67;

        ( 0 + 1) <= (n + 1) by NAT_1: 13;

        then ( len frx) in ( dom frx) by A8, A5, FINSEQ_3: 25;

        then (frx . ( len frx)) in ( rng frx) by FUNCT_1:def 3;

        then

        consider d be Element of D such that

         A10: d in ( dom ((F - r) | X)) and

         A11: (((F - r) | X) . d) = (frx . ( len frx)) by A7, PARTFUN1: 3;

        set Y = (X \ {d}), dx = ( dom (F | X)), dy = ( dom (F | Y)), fry = ( FinS ((F - r),Y)), fy = ( FinS (F,Y)), n1r = ((n + 1) |-> rr), nr = (n |-> rr);

        

         A12: {d} c= dx by A4, A10, ZFMISC_1: 31;

        ((F - r) . d) = (frx . ( len frx)) by A10, A11, FUNCT_1: 47;

        then

         A13: (fx . ( len fx)) = (F . d) by A3, A4, A10, Th72;

        ( len fx) = ( card G) by A3, Th67;

        then

         A14: fx = ((fx | n) ^ <*(F . d)*>) by A8, A13, RFINSEQ: 7;

        fx = (fy ^ <*(F . d)*>) by A3, A4, A10, A13, Th70;

        then

         A15: fy = (fx | n) by A14, FINSEQ_1: 33;

        

         A16: ( dom (fy - nr)) = ( Seg ( len (fy - nr))) by FINSEQ_1:def 3;

        

         A17: dy = (( dom F) /\ Y) by RELAT_1: 61;

        

         A18: dx = (( dom F) /\ X) by RELAT_1: 61;

        

         A19: dy = (dx \ {d})

        proof

          thus dy c= (dx \ {d})

          proof

            let y be object;

            assume

             A20: y in dy;

            then y in (X \ {d}) by A17, XBOOLE_0:def 4;

            then

             A21: not y in {d} by XBOOLE_0:def 5;

            y in ( dom F) by A17, A20, XBOOLE_0:def 4;

            then y in dx by A17, A18, A20, XBOOLE_0:def 4;

            hence thesis by A21, XBOOLE_0:def 5;

          end;

          let y be object;

          assume

           A22: y in (dx \ {d});

          then

           A23: not y in {d} by XBOOLE_0:def 5;

          

           A24: y in dx by A22, XBOOLE_0:def 5;

          then y in X by A18, XBOOLE_0:def 4;

          then

           A25: y in Y by A23, XBOOLE_0:def 5;

          y in ( dom F) by A18, A24, XBOOLE_0:def 4;

          hence thesis by A17, A25, XBOOLE_0:def 4;

        end;

        then

        reconsider dx, dy as finite set by A3;

        

         A26: ( card dy) = (( card dx) - ( card {d})) by A12, A19, CARD_2: 44

        .= ((n + 1) - 1) by A3, A8, CARD_1: 30

        .= n;

        then ( len nr) = n & ( len fy) = n by Th67, CARD_1:def 7;

        then

         A27: ( len (fy - nr)) = n by FINSEQ_2: 72;

        ((F - r) . d) = (frx . ( len frx)) by A10, A11, FUNCT_1: 47;

        then

         A28: frx = ((frx | n) ^ <*((F - r) . d)*>) by A8, A5, RFINSEQ: 7;

        ((fry ^ <*((F - r) . d)*>),((F - r) | X)) are_fiberwise_equipotent by A3, A4, A10, Th66;

        then ((fry ^ <*((F - r) . d)*>),frx) are_fiberwise_equipotent by A6, CLASSES1: 76;

        then (frx | n) is non-increasing & (fry,(frx | n)) are_fiberwise_equipotent by A28, RFINSEQ: 1, RFINSEQ: 20;

        then

         A29: fry = (frx | n) by RFINSEQ: 23;

        ( len n1r) = (n + 1) by CARD_1:def 7;

        then

         A30: ( len (fx - n1r)) = (n + 1) by A9, FINSEQ_2: 72;

        then

         A31: ( dom (fx - n1r)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

        ( dom ((F - r) | X)) = (( dom (F - r)) /\ X) by RELAT_1: 61;

        then d in ( dom (F - r)) by A10, XBOOLE_0:def 4;

        then d in ( dom F) by VALUED_1: 3;

        then ((F - r) . d) = ((F . d) - r) by VALUED_1: 3;

        then

         A32: <*((F - r) . d)*> = ( <*(F . d)*> - <*r*>) by RVSUM_1: 29;

        

         A33: n < (n + 1) by NAT_1: 13;

        

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

        reconsider Fd = <*(F . d)*>, rr = <*r*> as FinSequence of REAL by RVSUM_1: 145;

        ( len <*(F . d)*>) = 1 & ( len <*r*>) = 1 by FINSEQ_1: 40;

        then

         A35: ( len (Fd - rr)) = 1 by FINSEQ_2: 72;

        then

         A36: ( len ((fy - nr) ^ ( <*(F . d)*> - <*r*>))) = (n + 1) by A27, FINSEQ_1: 22;

        1 in ( Seg 1) by FINSEQ_1: 1;

        then

         A37: 1 in ( dom ( <*(F . d)*> - <*r*>)) by A35, FINSEQ_1:def 3;

        

         A38: ( <*(F . d)*> . 1) = (F . d) & ( <*r*> . 1) = r by FINSEQ_1: 40;

         A39:

        now

          let m be Nat;

          assume

           A40: m in ( dom (fx - n1r));

          per cases ;

            suppose

             A41: m = (n + 1);

            then

             A42: (n1r . m) = r by FINSEQ_1: 4, FUNCOP_1: 7;

            (((fy - nr) ^ ( <*(F . d)*> - <*r*>)) . m) = (( <*(F . d)*> - <*r*>) . ((n + 1) - n)) by A27, A36, A33, A41, FINSEQ_1: 24

            .= ((F . d) - r) by A38, A37, VALUED_1: 13;

            hence ((fx - n1r) . m) = (((fy - nr) ^ ( <*(F . d)*> - <*r*>)) . m) by A13, A9, A40, A41, A42, VALUED_1: 13;

          end;

            suppose

             A43: m <> (n + 1);

            m <= (n + 1) by A31, A40, FINSEQ_1: 1;

            then m < (n + 1) by A43, XXREAL_0: 1;

            then

             A44: m <= n by NAT_1: 13;

            reconsider s = (fx . m) as Element of REAL by XREAL_0:def 1;

            

             A45: n <= (n + 1) by NAT_1: 11;

            

             A46: (n1r . m) = r by A31, A40, FUNCOP_1: 7;

            

             A47: 1 <= m by A31, A40, FINSEQ_1: 1;

            then

             A48: m in ( Seg n) by A44, FINSEQ_1: 1;

            then

             A49: m in ( dom (fy - nr)) by A27, FINSEQ_1:def 3;

            1 <= n by A47, A44, XXREAL_0: 2;

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

            then

             A50: ((fx | n) . m) = (fx . m) by A9, A34, A48, RFINSEQ: 6;

            (((fy - nr) ^ ( <*(F . d)*> - <*r*>)) . m) = ((fy - nr) . m) & (nr . m) = r by A27, A16, A48, FINSEQ_1:def 7, FUNCOP_1: 7;

            

            hence (((fy - nr) ^ ( <*(F . d)*> - <*r*>)) . m) = (s - r) by A15, A50, A49, VALUED_1: 13

            .= ((fx - n1r) . m) by A40, A46, VALUED_1: 13;

          end;

        end;

        fry = (fy - nr) by A2, A26;

        hence thesis by A8, A28, A29, A32, A30, A36, A39, FINSEQ_2: 9;

      end;

      

       A51: P[ 0 ]

      proof

        let X be set, G be finite set;

        assume

         A52: G = ( dom (F | X));

        assume 0 = ( card G);

        then

         A53: ( dom (F | X)) = {} by A52;

        

        then ( FinS (F,X)) = ( FinS (F, {} )) by Th63

        .= ( <*> REAL ) by Th68;

        then

         A54: (( FinS (F,X)) - (( card G) |-> rr)) = ( <*> REAL ) by FINSEQ_2: 73;

        ( dom ((F - r) | X)) = (( dom (F - r)) /\ X) by RELAT_1: 61

        .= (( dom F) /\ X) by VALUED_1: 3

        .= ( dom (F | X)) by RELAT_1: 61;

        

        hence ( FinS ((F - r),X)) = ( FinS ((F - r), {} )) by A53, Th63

        .= (( FinS (F,X)) - (( card G) |-> r)) by A54, Th68;

      end;

      

       A55: for n holds P[n] from NAT_1:sch 2( A51, A1);

      let G be finite set;

      assume G = ( dom (F | X));

      hence thesis by A55;

    end;

    theorem :: RFUNCT_3:74

    for D be non empty set, F be PartFunc of D, REAL , X be set st ( dom (F | X)) is finite & (for d be Element of D st d in ( dom (F | X)) holds (F . d) >= 0 ) holds ( FinS (( max+ F),X)) = ( FinS (F,X))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      assume that

       A1: ( dom (F | X)) is finite and

       A2: for d be Element of D st d in ( dom (F | X)) holds (F . d) >= 0 ;

      now

        let d be Element of D;

        assume

         A3: d in ( dom (F | X));

        then (F . d) >= 0 by A2;

        hence ((F | X) . d) >= 0 by A3, FUNCT_1: 47;

      end;

      

      then

       A4: (F | X) = ( max+ (F | X)) by Th46

      .= (( max+ F) | X) by Th44;

      

      hence ( FinS (F,X)) = ( FinS ((( max+ F) | X),X)) by A1, Th64

      .= ( FinS (( max+ F),X)) by A1, A4, Th64;

    end;

    theorem :: RFUNCT_3:75

    for D be non empty set, F be PartFunc of D, REAL , X be set, r be Real, Z be finite set st Z = ( dom (F | X)) & ( rng (F | X)) = {r} holds ( FinS (F,X)) = (( card Z) |-> r)

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set, r be Real;

      let dx be finite set such that

       A1: dx = ( dom (F | X));

      set fx = ( FinS (F,X));

      assume

       A2: ( rng (F | X)) = {r};

      ((F | X),fx) are_fiberwise_equipotent by A1, Def13;

      then

       A3: ( rng fx) = {r} by A2, CLASSES1: 75;

      

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

      ( len fx) = ( card dx) by A1, Th67;

      hence thesis by A3, A4, FUNCOP_1: 9;

    end;

    theorem :: RFUNCT_3:76

    

     Th76: for D be non empty set, F be PartFunc of D, REAL , X,Y be set st ( dom (F | (X \/ Y))) is finite & X misses Y holds (( FinS (F,(X \/ Y))),(( FinS (F,X)) ^ ( FinS (F,Y)))) are_fiberwise_equipotent

    proof

      let D be non empty set, F be PartFunc of D, REAL , X,Y be set;

      assume

       A1: ( dom (F | (X \/ Y))) is finite;

      (F | Y) c= (F | (X \/ Y)) by RELAT_1: 75, XBOOLE_1: 7;

      then

      reconsider dfy = ( dom (F | Y)) as finite set by A1, FINSET_1: 1, RELAT_1: 11;

      defpred P[ Nat] means for Y be set, Z be finite set st Z = ( dom (F | Y)) & ( dom (F | (X \/ Y))) is finite & (X /\ Y) = {} & $1 = ( card Z) holds (( FinS (F,(X \/ Y))),(( FinS (F,X)) ^ ( FinS (F,Y)))) are_fiberwise_equipotent ;

      

       A2: ( card dfy) = ( card dfy);

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let Y be set, Z be finite set;

        assume that

         A5: Z = ( dom (F | Y)) and

         A6: ( dom (F | (X \/ Y))) is finite and

         A7: (X /\ Y) = {} and

         A8: (n + 1) = ( card Z);

        set x = the Element of ( dom (F | Y));

        reconsider x as Element of D by A5, A8, CARD_1: 27, TARSKI:def 3;

        set y1 = (Y \ {x});

        

         A9: ( dom (F | Y)) = (( dom F) /\ Y) by RELAT_1: 61;

        now

          assume

           A10: x in X;

          x in Y by A5, A8, A9, CARD_1: 27, XBOOLE_0:def 4;

          hence contradiction by A7, A10, XBOOLE_0:def 4;

        end;

        then (X \ {x}) = X by ZFMISC_1: 57;

        then

         A11: ((X \/ Y) \ {x}) = (X \/ y1) by XBOOLE_1: 42;

        

         A12: ( dom (F | y1)) = (( dom F) /\ y1) by RELAT_1: 61;

        

         A13: ( dom (F | y1)) = (( dom (F | Y)) \ {x})

        proof

          thus ( dom (F | y1)) c= (( dom (F | Y)) \ {x})

          proof

            let y be object;

            assume

             A14: y in ( dom (F | y1));

            then y in (Y \ {x}) by A12, XBOOLE_0:def 4;

            then

             A15: not y in {x} by XBOOLE_0:def 5;

            y in ( dom F) by A12, A14, XBOOLE_0:def 4;

            then y in ( dom (F | Y)) by A12, A9, A14, XBOOLE_0:def 4;

            hence thesis by A15, XBOOLE_0:def 5;

          end;

          let y be object;

          assume

           A16: y in (( dom (F | Y)) \ {x});

          then

           A17: not y in {x} by XBOOLE_0:def 5;

          

           A18: y in ( dom (F | Y)) by A16, XBOOLE_0:def 5;

          then y in Y by A9, XBOOLE_0:def 4;

          then

           A19: y in y1 by A17, XBOOLE_0:def 5;

          y in ( dom F) by A9, A18, XBOOLE_0:def 4;

          hence thesis by A12, A19, XBOOLE_0:def 4;

        end;

        then

        reconsider dFy = ( dom (F | y1)) as finite set by A5;

         {x} c= ( dom (F | Y)) by A5, A8, CARD_1: 27, ZFMISC_1: 31;

        

        then

         A20: ( card dFy) = ((n + 1) - ( card {x})) by A5, A8, A13, CARD_2: 44

        .= ((n + 1) - 1) by CARD_1: 30

        .= n;

        (X \/ y1) c= (X \/ Y) by XBOOLE_1: 13;

        then (( dom F) /\ (X \/ y1)) c= (( dom F) /\ (X \/ Y)) by XBOOLE_1: 27;

        then ( dom (F | (X \/ y1))) c= (( dom F) /\ (X \/ Y)) by RELAT_1: 61;

        then

         A21: ( dom (F | (X \/ y1))) c= ( dom (F | (X \/ Y))) by RELAT_1: 61;

        

         A22: (( FinS (F,(X \/ Y))),(F | (X \/ Y))) are_fiberwise_equipotent by A6, Def13;

        ( dom (F | (X \/ Y))) = (( dom F) /\ (X \/ Y)) by RELAT_1: 61

        .= ((( dom F) /\ X) \/ (( dom F) /\ Y)) by XBOOLE_1: 23

        .= (( dom (F | X)) \/ (( dom F) /\ Y)) by RELAT_1: 61

        .= (( dom (F | X)) \/ ( dom (F | Y))) by RELAT_1: 61;

        then x in ( dom (F | (X \/ Y))) by A5, A8, CARD_1: 27, XBOOLE_0:def 3;

        then ((( FinS (F,(X \/ y1))) ^ <*(F . x)*>),(F | (X \/ Y))) are_fiberwise_equipotent by A6, A11, Th66;

        then

         A23: ((( FinS (F,(X \/ y1))) ^ <*(F . x)*>),( FinS (F,(X \/ Y)))) are_fiberwise_equipotent by A22, CLASSES1: 76;

        (X /\ y1) c= (X /\ Y) by XBOOLE_1: 27;

        then (( FinS (F,(X \/ y1))),(( FinS (F,X)) ^ ( FinS (F,y1)))) are_fiberwise_equipotent by A4, A6, A7, A21, A20, XBOOLE_1: 3;

        then ((( FinS (F,(X \/ y1))) ^ <*(F . x)*>),((( FinS (F,X)) ^ ( FinS (F,y1))) ^ <*(F . x)*>)) are_fiberwise_equipotent by RFINSEQ: 1;

        then

         A24: ((( FinS (F,(X \/ y1))) ^ <*(F . x)*>),(( FinS (F,X)) ^ (( FinS (F,y1)) ^ <*(F . x)*>))) are_fiberwise_equipotent by FINSEQ_1: 32;

        ((( FinS (F,y1)) ^ <*(F . x)*>),(F | Y)) are_fiberwise_equipotent & (( FinS (F,Y)),(F | Y)) are_fiberwise_equipotent by A5, A8, Def13, Th66, CARD_1: 27;

        then ((( FinS (F,y1)) ^ <*(F . x)*>),( FinS (F,Y))) are_fiberwise_equipotent by CLASSES1: 76;

        then

         A25: (((( FinS (F,y1)) ^ <*(F . x)*>) ^ ( FinS (F,X))),(( FinS (F,Y)) ^ ( FinS (F,X)))) are_fiberwise_equipotent by RFINSEQ: 1;

        ((( FinS (F,X)) ^ (( FinS (F,y1)) ^ <*(F . x)*>)),((( FinS (F,y1)) ^ <*(F . x)*>) ^ ( FinS (F,X)))) are_fiberwise_equipotent by RFINSEQ: 2;

        then ((( FinS (F,Y)) ^ ( FinS (F,X))),(( FinS (F,X)) ^ ( FinS (F,Y)))) are_fiberwise_equipotent & ((( FinS (F,X)) ^ (( FinS (F,y1)) ^ <*(F . x)*>)),(( FinS (F,Y)) ^ ( FinS (F,X)))) are_fiberwise_equipotent by A25, CLASSES1: 76, RFINSEQ: 2;

        then ((( FinS (F,X)) ^ (( FinS (F,y1)) ^ <*(F . x)*>)),(( FinS (F,X)) ^ ( FinS (F,Y)))) are_fiberwise_equipotent by CLASSES1: 76;

        then ((( FinS (F,(X \/ y1))) ^ <*(F . x)*>),(( FinS (F,X)) ^ ( FinS (F,Y)))) are_fiberwise_equipotent by A24, CLASSES1: 76;

        hence thesis by A23, CLASSES1: 76;

      end;

      

       A26: P[ 0 ]

      proof

        let Y be set, Z be finite set;

        assume that

         A27: Z = ( dom (F | Y)) and

         A28: ( dom (F | (X \/ Y))) is finite and (X /\ Y) = {} and

         A29: 0 = ( card Z);

        

         A30: ( dom (F | (X \/ Y))) = (( dom F) /\ (X \/ Y)) by RELAT_1: 61

        .= ((( dom F) /\ X) \/ (( dom F) /\ Y)) by XBOOLE_1: 23

        .= (( dom (F | X)) \/ (( dom F) /\ Y)) by RELAT_1: 61

        .= (( dom (F | X)) \/ ( dom (F | Y))) by RELAT_1: 61;

        then

         A31: ( dom (F | X)) is finite by A28, FINSET_1: 1, XBOOLE_1: 7;

        

         A32: ( dom (F | Y)) = {} by A27, A29;

        

        then ( FinS (F,(X \/ Y))) = ( FinS (F,( dom (F | X)))) by A28, A30, Th63

        .= ( FinS (F,X)) by A31, Th63

        .= (( FinS (F,X)) ^ ( <*> REAL )) by FINSEQ_1: 34

        .= (( FinS (F,X)) ^ ( FinS (F,( dom (F | Y))))) by A32, Th68

        .= (( FinS (F,X)) ^ ( FinS (F,Y))) by A27, Th63;

        hence thesis;

      end;

      

       A33: for n holds P[n] from NAT_1:sch 2( A26, A3);

      assume (X /\ Y) = {} ;

      hence thesis by A1, A33, A2;

    end;

    definition

      let D be non empty set, F be PartFunc of D, REAL , X be set;

      :: RFUNCT_3:def14

      func Sum (F,X) -> Real equals ( Sum ( FinS (F,X)));

      correctness ;

    end

    theorem :: RFUNCT_3:77

    

     Th77: for D be non empty set, F be PartFunc of D, REAL , X be set, r st ( dom (F | X)) is finite holds ( Sum ((r (#) F),X)) = (r * ( Sum (F,X)))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set, r;

      set x = ( dom (F | X));

      reconsider rr = r as Real;

      assume

       A1: ( dom (F | X)) is finite;

      then

      reconsider FX = (F | X) as finite Function by FINSET_1: 10;

      ( dom ((r (#) F) | X)) = ( dom (r (#) (F | X))) by RFUNCT_1: 49

      .= ( dom (F | X)) by VALUED_1:def 5;

      then

      reconsider rFX = ((r (#) F) | X) as finite Function by A1, FINSET_1: 10;

      consider b be FinSequence such that

       A2: ((F | x),b) are_fiberwise_equipotent by A1, RFINSEQ: 5;

      ( rng (F | x)) = ( rng b) by A2, CLASSES1: 75;

      then

      reconsider b as FinSequence of REAL by FINSEQ_1:def 4;

      x = (( dom F) /\ X) by RELAT_1: 61;

      

      then

       A3: (F | x) = ((F | ( dom F)) | X) by RELAT_1: 71

      .= (F | X) by RELAT_1: 68;

      then

       A4: ( rng b) = ( rng (F | X)) by A2, CLASSES1: 75;

       A5:

      now

        let x be Element of REAL ;

        

         A6: ( len (r * b)) = ( len b) by FINSEQ_2: 33;

        now

          per cases ;

            case

             A7: not x in ( rng (r * b));

             A8:

            now

              assume x in ( rng ((r (#) F) | X));

              then x in ( rng (r (#) (F | X))) by RFUNCT_1: 49;

              then

              consider d be Element of D such that

               A9: d in ( dom (r (#) (F | X))) and

               A10: ((r (#) (F | X)) . d) = x by PARTFUN1: 3;

              d in ( dom (F | X)) by A9, VALUED_1:def 5;

              then ((F | X) . d) in ( rng (F | X)) by FUNCT_1:def 3;

              then

              consider n be Nat such that

               A11: n in ( dom b) and

               A12: (b . n) = ((F | X) . d) by A4, FINSEQ_2: 10;

              x = (r * ((F | X) . d)) by A9, A10, VALUED_1:def 5;

              then

               A13: x = ((r * b) . n) by A12, RVSUM_1: 44;

              n in ( dom (r * b)) by A6, A11, FINSEQ_3: 29;

              hence contradiction by A7, A13, FUNCT_1:def 3;

            end;

            ((r * b) " {x}) = {} by A7, Lm2;

            hence ( card ((r * b) " {x})) = ( card (rFX " {x})) by A8, Lm2;

          end;

            case x in ( rng (r * b));

            then

            consider n be Nat such that n in ( dom (r * b)) and

             A14: ((r * b) . n) = x by FINSEQ_2: 10;

            reconsider p = (b . n) as Real;

            

             A15: x = (r * p) by A14, RVSUM_1: 44;

            now

              per cases ;

                case

                 A16: r = 0 ;

                then

                 A17: ((r * b) " {x}) = ( dom b) by A15, RFINSEQ: 25;

                ( dom FX) = ((r (#) (F | X)) " {x}) by A15, A16, Th7

                .= (((r (#) F) | X) " {x}) by RFUNCT_1: 49;

                hence ( card ((r * b) " {x})) = ( card (rFX " {x})) by A2, A3, A17, CLASSES1: 81;

              end;

                case

                 A18: r <> 0 ;

                then

                 A19: ( Coim ((rr * b),x)) = ( Coim (b,(x / rr))) by RFINSEQ: 24;

                ( Coim (((r (#) F) | X),x)) = ((r (#) (F | X)) " {x}) by RFUNCT_1: 49

                .= ( Coim (FX,(x / r))) by A18, Th6;

                hence ( card ( Coim ((r * b),x))) = ( card ( Coim (rFX,x))) by A2, A3, A19, CLASSES1:def 10;

              end;

            end;

            hence ( card ((r * b) " {x})) = ( card (rFX " {x}));

          end;

        end;

        hence ( card ( Coim ((r * b),x))) = ( card ( Coim (rFX,x)));

      end;

      ( rng (r * b)) c= REAL & ( rng ((r (#) F) | X)) c= REAL ;

      then

       A20: ((r * b),((r (#) F) | X)) are_fiberwise_equipotent by A5, CLASSES1: 79;

      ((F | X),( FinS (F,X))) are_fiberwise_equipotent by A1, Def13;

      then

       A21: ( Sum b) = ( Sum (F,X)) by A2, A3, CLASSES1: 76, RFINSEQ: 9;

      ( dom ((r (#) F) | X)) = (( dom (r (#) F)) /\ X) by RELAT_1: 61

      .= (( dom F) /\ X) by VALUED_1:def 5

      .= ( dom (F | X)) by RELAT_1: 61;

      then (((r (#) F) | X),( FinS ((r (#) F),X))) are_fiberwise_equipotent by A1, Def13;

      

      hence ( Sum ((r (#) F),X)) = ( Sum (r * b)) by A20, CLASSES1: 76, RFINSEQ: 9

      .= (r * ( Sum (F,X))) by A21, RVSUM_1: 87;

    end;

    theorem :: RFUNCT_3:78

    

     Th78: for D be non empty set, F,G be PartFunc of D, REAL , X be set, Y be finite set st Y = ( dom (F | X)) & ( dom (F | X)) = ( dom (G | X)) holds ( Sum ((F + G),X)) = (( Sum (F,X)) + ( Sum (G,X)))

    proof

      let D be non empty set;

      let F,G be PartFunc of D, REAL , X be set, Y be finite set such that

       A1: Y = ( dom (F | X));

      defpred P[ Nat] means for F,G be PartFunc of D, REAL , X be set, Y be finite set st ( card Y) = $1 & Y = ( dom (F | X)) & ( dom (F | X)) = ( dom (G | X)) holds ( Sum ((F + G),X)) = (( Sum (F,X)) + ( Sum (G,X)));

      

       A2: ( card Y) = ( card Y);

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let F,G be PartFunc of D, REAL , X be set, dx be finite set;

        set gx = ( dom (G | X));

        assume that

         A5: ( card dx) = (n + 1) and

         A6: dx = ( dom (F | X)) and

         A7: ( dom (F | X)) = ( dom (G | X));

        set x = the Element of dx;

        reconsider x as Element of D by A5, A6, CARD_1: 27, TARSKI:def 3;

        

         A8: dx = (( dom F) /\ X) by A6, RELAT_1: 61;

        then

         A9: x in ( dom F) by A5, CARD_1: 27, XBOOLE_0:def 4;

        set Y = (X \ {x}), dy = ( dom (F | Y)), gy = ( dom (G | Y));

        

         A10: gx = (( dom G) /\ X) by RELAT_1: 61;

        then x in ( dom G) by A5, A6, A7, CARD_1: 27, XBOOLE_0:def 4;

        then x in (( dom F) /\ ( dom G)) by A9, XBOOLE_0:def 4;

        then

         A11: x in ( dom (F + G)) by VALUED_1:def 1;

        

         A12: dy = (( dom F) /\ Y) by RELAT_1: 61;

        

         A13: dy = (dx \ {x})

        proof

          thus dy c= (dx \ {x})

          proof

            let y be object;

            assume

             A14: y in dy;

            then y in (X \ {x}) by A12, XBOOLE_0:def 4;

            then

             A15: not y in {x} by XBOOLE_0:def 5;

            y in ( dom F) by A12, A14, XBOOLE_0:def 4;

            then y in dx by A12, A8, A14, XBOOLE_0:def 4;

            hence thesis by A15, XBOOLE_0:def 5;

          end;

          let y be object;

          assume

           A16: y in (dx \ {x});

          then ( not y in {x}) & y in X by A8, XBOOLE_0:def 4, XBOOLE_0:def 5;

          then

           A17: y in Y by XBOOLE_0:def 5;

          y in ( dom F) by A8, A16, XBOOLE_0:def 4;

          hence thesis by A12, A17, XBOOLE_0:def 4;

        end;

        then

        reconsider dy as finite set;

        

         A18: gy = (( dom G) /\ Y) by RELAT_1: 61;

        

         A19: dy = gy

        proof

          thus dy c= gy

          proof

            let y be object;

            assume

             A20: y in dy;

            then y in ( dom F) by A12, XBOOLE_0:def 4;

            then y in gx by A6, A7, A12, A8, A20, XBOOLE_0:def 4;

            then

             A21: y in ( dom G) by A10, XBOOLE_0:def 4;

            y in Y by A12, A20, XBOOLE_0:def 4;

            hence thesis by A18, A21, XBOOLE_0:def 4;

          end;

          let y be object;

          assume

           A22: y in gy;

          then y in ( dom G) by A18, XBOOLE_0:def 4;

          then y in dx by A6, A7, A18, A10, A22, XBOOLE_0:def 4;

          then

           A23: y in ( dom F) by A8, XBOOLE_0:def 4;

          y in Y by A18, A22, XBOOLE_0:def 4;

          hence thesis by A12, A23, XBOOLE_0:def 4;

        end;

         {x} c= dx by A5, CARD_1: 27, ZFMISC_1: 31;

        

        then ( card dy) = (( card dx) - ( card {x})) by A13, CARD_2: 44

        .= ((n + 1) - 1) by A5, CARD_1: 30

        .= n;

        then

         A24: ( Sum ((F + G),Y)) = (( Sum (F,Y)) + ( Sum (G,Y))) by A4, A19;

        

         A25: ( dom ((F + G) | X)) = ( dom ((F | X) + (G | X))) by RFUNCT_1: 44

        .= (dx /\ gx) by A6, VALUED_1:def 1;

        then

         A26: (( FinS ((F + G),X)),((F + G) | X)) are_fiberwise_equipotent by Def13;

        x in X by A5, A8, CARD_1: 27, XBOOLE_0:def 4;

        then x in (( dom (F + G)) /\ X) by A11, XBOOLE_0:def 4;

        then x in ( dom ((F + G) | X)) by RELAT_1: 61;

        then

         A27: ((( FinS ((F + G),Y)) ^ <*((F + G) . x)*>),((F + G) | X)) are_fiberwise_equipotent by A25, Th66;

        reconsider Fx = <*(F . x)*>, Gx = <*(G . x)*>, FGx = <*((F + G) . x)*> as FinSequence of REAL by RVSUM_1: 145;

        ((( FinS (F,Y)) ^ <*(F . x)*>),(F | X)) are_fiberwise_equipotent & (( FinS (F,X)),(F | X)) are_fiberwise_equipotent by A5, A6, Def13, Th66, CARD_1: 27;

        

        then

         A28: ( Sum (F,X)) = ( Sum (( FinS (F,Y)) ^ Fx)) by CLASSES1: 76, RFINSEQ: 9

        .= (( Sum (F,Y)) + (F . x)) by RVSUM_1: 74;

        ((( FinS (G,Y)) ^ <*(G . x)*>),(G | X)) are_fiberwise_equipotent & (( FinS (G,X)),(G | X)) are_fiberwise_equipotent by A5, A6, A7, Def13, Th66, CARD_1: 27;

        

        then ( Sum (G,X)) = ( Sum (( FinS (G,Y)) ^ Gx)) by CLASSES1: 76, RFINSEQ: 9

        .= (( Sum (G,Y)) + (G . x)) by RVSUM_1: 74;

        

        hence (( Sum (F,X)) + ( Sum (G,X))) = (( Sum ( FinS ((F + G),Y))) + ((F . x) + (G . x))) by A24, A28

        .= (( Sum ( FinS ((F + G),Y))) + ((F + G) . x)) by A11, VALUED_1:def 1

        .= ( Sum (( FinS ((F + G),Y)) ^ FGx)) by RVSUM_1: 74

        .= ( Sum ((F + G),X)) by A27, A26, CLASSES1: 76, RFINSEQ: 9;

      end;

      

       A29: P[ 0 ]

      proof

        let F,G be PartFunc of D, REAL , X be set, Y be finite set;

        assume that

         A30: ( card Y) = 0 and

         A31: Y = ( dom (F | X)) and

         A32: ( dom (F | X)) = ( dom (G | X));

        ( dom (F | X)) = {} by A30, A31;

        then

         A33: ( rng (F | X)) = {} by RELAT_1: 42;

        ((F + G) | X) = ((F | X) + (G | X)) by RFUNCT_1: 44;

        

        then ( dom ((F + G) | X)) = (( dom (F | X)) /\ ( dom (G | X))) by VALUED_1:def 1

        .= {} by A30, A31, A32;

        then ( rng ((F + G) | X)) = {} & (( FinS ((F + G),X)),((F + G) | X)) are_fiberwise_equipotent by Def13, RELAT_1: 42;

        then

         A34: ( rng ( FinS ((F + G),X))) = {} by CLASSES1: 75;

        (( FinS (F,X)),(F | X)) are_fiberwise_equipotent by A31, Def13;

        then ( rng ( FinS (F,X))) = {} by A33, CLASSES1: 75;

        then

         A35: ( Sum (F,X)) = 0 by RELAT_1: 41, RVSUM_1: 72;

        ( dom (G | X)) = {} by A30, A31, A32;

        then

         A36: ( rng (G | X)) = {} by RELAT_1: 42;

        (( FinS (G,X)),(G | X)) are_fiberwise_equipotent by A31, A32, Def13;

        then ( rng ( FinS (G,X))) = {} by A36, CLASSES1: 75;

        then (( Sum (F,X)) + ( Sum (G,X))) = ( 0 + 0 ) by A35, RELAT_1: 41, RVSUM_1: 72;

        hence thesis by A34, RELAT_1: 41, RVSUM_1: 72;

      end;

      

       A37: for n holds P[n] from NAT_1:sch 2( A29, A3);

      assume ( dom (F | X)) = ( dom (G | X));

      hence thesis by A1, A37, A2;

    end;

    theorem :: RFUNCT_3:79

    for D be non empty set, F,G be PartFunc of D, REAL , X be set st ( dom (F | X)) is finite & ( dom (F | X)) = ( dom (G | X)) holds ( Sum ((F - G),X)) = (( Sum (F,X)) - ( Sum (G,X)))

    proof

      let D be non empty set, F,G be PartFunc of D, REAL , X be set;

      assume

       A1: ( dom (F | X)) is finite & ( dom (F | X)) = ( dom (G | X));

      ( dom ((( - 1) (#) G) | X)) = (( dom (( - 1) (#) G)) /\ X) by RELAT_1: 61

      .= (( dom G) /\ X) by VALUED_1:def 5

      .= ( dom (G | X)) by RELAT_1: 61;

      

      hence ( Sum ((F - G),X)) = (( Sum (F,X)) + ( Sum ((( - 1) (#) G),X))) by A1, Th78

      .= (( Sum (F,X)) + (( - 1) * ( Sum (G,X)))) by A1, Th77

      .= (( Sum (F,X)) - ( Sum (G,X)));

    end;

    theorem :: RFUNCT_3:80

    for D be non empty set, F be PartFunc of D, REAL , X be set, r be Real, Y be finite set st Y = ( dom (F | X)) holds ( Sum ((F - r),X)) = (( Sum (F,X)) - (r * ( card Y)))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X be set, r be Real;

      set fx = ( FinS (F,X));

      let Y be finite set;

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

      set dr = (( card Y) |-> rr);

      assume

       A1: Y = ( dom (F | X));

      then ( len fx) = ( card Y) by Th67;

      then

      reconsider xf = fx, rd = dr as Element of (( card Y) -tuples_on REAL ) by FINSEQ_2: 92;

      ( FinS ((F - r),X)) = (fx - dr) by A1, Th73;

      

      hence ( Sum ((F - r),X)) = (( Sum xf) - ( Sum rd)) by RVSUM_1: 90

      .= (( Sum (F,X)) - (r * ( card Y))) by RVSUM_1: 80;

    end;

    theorem :: RFUNCT_3:81

    for D be non empty set, F be PartFunc of D, REAL holds ( Sum (F, {} )) = 0 by Th68, RVSUM_1: 72;

    theorem :: RFUNCT_3:82

    for D be non empty set, F be PartFunc of D, REAL , d be Element of D st d in ( dom F) holds ( Sum (F, {d})) = (F . d)

    proof

      let D be non empty set, F be PartFunc of D, REAL , d be Element of D;

      reconsider Fd = (F . d) as Element of REAL by XREAL_0:def 1;

      assume d in ( dom F);

      

      hence ( Sum (F, {d})) = ( Sum <*Fd*>) by Th69

      .= (F . d) by FINSOP_1: 11;

    end;

    theorem :: RFUNCT_3:83

    for D be non empty set, F be PartFunc of D, REAL , X,Y be set st ( dom (F | (X \/ Y))) is finite & X misses Y holds ( Sum (F,(X \/ Y))) = (( Sum (F,X)) + ( Sum (F,Y)))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X,Y be set;

      assume ( dom (F | (X \/ Y))) is finite & X misses Y;

      

      hence ( Sum (F,(X \/ Y))) = ( Sum (( FinS (F,X)) ^ ( FinS (F,Y)))) by Th76, RFINSEQ: 9

      .= (( Sum (F,X)) + ( Sum (F,Y))) by RVSUM_1: 75;

    end;

    theorem :: RFUNCT_3:84

    for D be non empty set, F be PartFunc of D, REAL , X,Y be set st ( dom (F | (X \/ Y))) is finite & ( dom (F | X)) misses ( dom (F | Y)) holds ( Sum (F,(X \/ Y))) = (( Sum (F,X)) + ( Sum (F,Y)))

    proof

      let D be non empty set, F be PartFunc of D, REAL , X,Y be set;

      assume that

       A1: ( dom (F | (X \/ Y))) is finite and

       A2: ( dom (F | X)) misses ( dom (F | Y));

      

       A3: ( dom (F | (X \/ Y))) = (( dom F) /\ (X \/ Y)) by RELAT_1: 61

      .= ((( dom F) /\ X) \/ (( dom F) /\ Y)) by XBOOLE_1: 23

      .= (( dom (F | X)) \/ (( dom F) /\ Y)) by RELAT_1: 61

      .= (( dom (F | X)) \/ ( dom (F | Y))) by RELAT_1: 61;

      then ( dom (F | X)) is finite by A1, FINSET_1: 1, XBOOLE_1: 7;

      then

       A4: ( FinS (F,X)) = ( FinS (F,( dom (F | X)))) by Th63;

      ( dom (F | Y)) is finite by A1, A3, FINSET_1: 1, XBOOLE_1: 7;

      then

       A5: ( FinS (F,Y)) = ( FinS (F,( dom (F | Y)))) by Th63;

      

       A6: ( dom (F | ( dom (F | (X \/ Y))))) = (( dom F) /\ ( dom (F | (X \/ Y)))) by RELAT_1: 61

      .= (( dom F) /\ (( dom F) /\ (X \/ Y))) by RELAT_1: 61

      .= ((( dom F) /\ ( dom F)) /\ (X \/ Y)) by XBOOLE_1: 16

      .= ( dom (F | (X \/ Y))) by RELAT_1: 61;

      ( FinS (F,(X \/ Y))) = ( FinS (F,( dom (F | (X \/ Y))))) by A1, Th63;

      

      hence ( Sum (F,(X \/ Y))) = ( Sum (( FinS (F,X)) ^ ( FinS (F,Y)))) by A1, A2, A3, A4, A5, A6, Th76, RFINSEQ: 9

      .= (( Sum (F,X)) + ( Sum (F,Y))) by RVSUM_1: 75;

    end;