valued_1.miz



    begin

    

     Lm1: for f be FinSequence, h be Function st ( dom h) = ( dom f) holds h is FinSequence

    proof

      let f be FinSequence, h be Function such that

       A1: ( dom h) = ( dom f);

      h is FinSequence-like

      proof

        take ( len f);

        thus thesis by A1, FINSEQ_1:def 3;

      end;

      hence thesis;

    end;

    

     Lm2: for f,g be FinSequence, h be Function st ( dom h) = (( dom f) /\ ( dom g)) holds h is FinSequence

    proof

      let f,g be FinSequence, h be Function such that

       A1: ( dom h) = (( dom f) /\ ( dom g));

      consider n be Nat such that

       A2: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

      consider m be Nat such that

       A3: ( dom g) = ( Seg m) by FINSEQ_1:def 2;

      h is FinSequence-like

      proof

        per cases ;

          suppose

           A4: n <= m;

          take n;

          thus thesis by A1, A2, A3, A4, FINSEQ_1: 7;

        end;

          suppose

           A5: m <= n;

          take m;

          thus thesis by A1, A2, A3, A5, FINSEQ_1: 7;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster complex-valued for FinSequence;

      existence

      proof

        take ( <*> COMPLEX );

        thus thesis;

      end;

    end

    registration

      let r be Rational;

      cluster |.r.| -> rational;

      coherence

      proof

         |.r.| = ( - r) or |.r.| = r by COMPLEX1: 71;

        hence thesis;

      end;

    end

    definition

      let f1,f2 be complex-valued Function;

      deffunc F( object) = ((f1 . $1) + (f2 . $1));

      set X = (( dom f1) /\ ( dom f2));

      :: VALUED_1:def1

      func f1 + f2 -> Function means

      : Def1: ( dom it ) = (( dom f1) /\ ( dom f2)) & for c be object st c in ( dom it ) holds (it . c) = ((f1 . c) + (f2 . c));

      existence

      proof

        ex f be Function st ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function such that

         A1: ( dom f) = X and

         A2: for c be object st c in ( dom f) holds (f . c) = F(c) and

         A3: ( dom g) = X and

         A4: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A5: x in ( dom f);

          

          hence (f . x) = F(x) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

      commutativity ;

    end

    registration

      let f1,f2 be complex-valued Function;

      cluster (f1 + f2) -> complex-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 + f2));

        then ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by Def1;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be real-valued Function;

      cluster (f1 + f2) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 + f2));

        then ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by Def1;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be RAT -valued Function;

      cluster (f1 + f2) -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f1 + f2));

        then

        consider x be object such that

         A1: x in ( dom (f1 + f2)) and

         A2: ((f1 + f2) . x) = y by FUNCT_1:def 3;

        ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A1, Def1;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    registration

      let f1,f2 be INT -valued Function;

      cluster (f1 + f2) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f1 + f2));

        then

        consider x be object such that

         A1: x in ( dom (f1 + f2)) and

         A2: ((f1 + f2) . x) = y by FUNCT_1:def 3;

        ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A1, Def1;

        hence thesis by A2, INT_1:def 2;

      end;

    end

    registration

      let f1,f2 be natural-valued Function;

      cluster (f1 + f2) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 + f2));

        then ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by Def1;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D1,D2 be complex-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: +

      redefine

      func f1 + f2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 + f2)) c= COMPLEX by Def1, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be real-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: +

      redefine

      func f1 + f2 -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 + f2)) c= REAL by Def1, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be rational-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: +

      redefine

      func f1 + f2 -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 + f2)) c= RAT by Def1, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be integer-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: +

      redefine

      func f1 + f2 -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 + f2)) c= INT by Def1, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be natural-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: +

      redefine

      func f1 + f2 -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 + f2)) c= NAT by Def1, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 + f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 + f2)) = (C /\ C) by Def1

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be real-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 + f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 + f2)) = (C /\ C) by Def1

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be rational-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 + f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 + f2)) = (C /\ C) by Def1

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be integer-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 + f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 + f2)) = (C /\ C) by Def1

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be natural-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 + f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 + f2)) = (C /\ C) by Def1

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: VALUED_1:1

    for C be set, D1,D2 be complex-membered non empty set holds for f1 be Function of C, D1, f2 be Function of C, D2 holds for c be Element of C holds ((f1 + f2) . c) = ((f1 . c) + (f2 . c))

    proof

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1, f2 be Function of C, D2;

      

       A1: ( dom (f1 + f2)) = C by FUNCT_2:def 1;

      let c be Element of C;

      per cases ;

        suppose C is non empty;

        hence thesis by A1, Def1;

      end;

        suppose

         A2: C is empty;

        then (f1 . c) = 0 ;

        hence thesis by A2;

      end;

    end;

    registration

      let f1,f2 be complex-valued FinSequence;

      cluster (f1 + f2) -> FinSequence-like;

      coherence

      proof

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by Def1;

        hence thesis by Lm2;

      end;

    end

    begin

    definition

      let f be complex-valued Function, r be Complex;

      deffunc F( object) = (r + (f . $1));

      :: VALUED_1:def2

      func r + f -> Function means

      : Def2: ( dom it ) = ( dom f) & for c be object st c in ( dom it ) holds (it . c) = (r + (f . c));

      existence

      proof

        ex g be Function st ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let h,g be Function such that

         A1: ( dom h) = ( dom f) and

         A2: for c be object st c in ( dom h) holds (h . c) = F(c) and

         A3: ( dom g) = ( dom f) and

         A4: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A5: x in ( dom h);

          

          hence (h . x) = F(x) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    notation

      let f be complex-valued Function, r be Complex;

      synonym f + r for r + f;

    end

    registration

      let f be complex-valued Function, r be Complex;

      cluster (r + f) -> complex-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r + f));

        then ((r + f) . x) = (r + (f . x)) by Def2;

        hence thesis;

      end;

    end

    registration

      let f be real-valued Function, r be Real;

      cluster (r + f) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r + f));

        then ((r + f) . x) = (r + (f . x)) by Def2;

        hence thesis;

      end;

    end

    registration

      let f be RAT -valued Function, r be Rational;

      cluster (r + f) -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (r + f));

        then

        consider x be object such that

         A1: x in ( dom (r + f)) and

         A2: ((r + f) . x) = y by FUNCT_1:def 3;

        ((r + f) . x) = (r + (f . x)) by A1, Def2;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    registration

      let f be INT -valued Function, r be Integer;

      cluster (r + f) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (r + f));

        then

        consider x be object such that

         A1: x in ( dom (r + f)) and

         A2: ((r + f) . x) = y by FUNCT_1:def 3;

        ((r + f) . x) = (r + (f . x)) by A1, Def2;

        hence thesis by A2, INT_1:def 2;

      end;

    end

    registration

      let f be natural-valued Function, r be Nat;

      cluster (r + f) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r + f));

        then ((r + f) . x) = (r + (f . x)) by Def2;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      let r be Complex;

      :: original: +

      redefine

      func r + f -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (r + f)) = ( dom f) & ( rng (r + f)) c= COMPLEX by Def2, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      let r be Real;

      :: original: +

      redefine

      func r + f -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (r + f)) = ( dom f) & ( rng (r + f)) c= REAL by Def2, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      let r be Rational;

      :: original: +

      redefine

      func r + f -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (r + f)) = ( dom f) & ( rng (r + f)) c= RAT by Def2, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      let r be Integer;

      :: original: +

      redefine

      func r + f -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (r + f)) = ( dom f) & ( rng (r + f)) c= INT by Def2, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be natural-membered set;

      let f be PartFunc of C, D;

      let r be Nat;

      :: original: +

      redefine

      func r + f -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom (r + f)) = ( dom f) & ( rng (r + f)) c= NAT by Def2, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      let r be Complex;

      cluster (r + f) -> total;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      let r be Real;

      cluster (r + f) -> total;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      let r be Rational;

      cluster (r + f) -> total;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      let r be Integer;

      cluster (r + f) -> total;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be natural-membered non empty set;

      let f be Function of C, D;

      let r be Nat;

      cluster (r + f) -> total;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: VALUED_1:2

    for C be non empty set, D be complex-membered non empty set holds for f be Function of C, D, r be Complex holds for c be Element of C holds ((r + f) . c) = (r + (f . c))

    proof

      let C be non empty set;

      let D be complex-membered non empty set;

      let f be Function of C, D, r be Complex;

      ( dom (r + f)) = C by FUNCT_2:def 1;

      hence thesis by Def2;

    end;

    registration

      let f be complex-valued FinSequence, r be Complex;

      cluster (r + f) -> FinSequence-like;

      coherence

      proof

        ( dom (r + f)) = ( dom f) by Def2;

        hence thesis by Lm1;

      end;

    end

    begin

    definition

      let f be complex-valued Function, r be Complex;

      :: VALUED_1:def3

      func f - r -> Function equals (( - r) + f);

      coherence ;

    end

    theorem :: VALUED_1:3

    for f be complex-valued Function, r be Complex holds ( dom (f - r)) = ( dom f) & for c be object st c in ( dom f) holds ((f - r) . c) = ((f . c) - r)

    proof

      let f be complex-valued Function, r be Complex;

      ( dom (f - r)) = ( dom f) by Def2;

      hence thesis by Def2;

    end;

    registration

      let f be complex-valued Function, r be Complex;

      cluster (f - r) -> complex-valued;

      coherence ;

    end

    registration

      let f be real-valued Function, r be Real;

      cluster (f - r) -> real-valued;

      coherence ;

    end

    registration

      let f be RAT -valued Function, r be Rational;

      cluster (f - r) -> RAT -valued;

      coherence ;

    end

    registration

      let f be INT -valued Function, r be Integer;

      cluster (f - r) -> INT -valued;

      coherence ;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      let r be Complex;

      :: original: -

      redefine

      func f - r -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f - r)) = ( dom f) & ( rng (f - r)) c= COMPLEX by Def2, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      let r be Real;

      :: original: -

      redefine

      func f - r -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f - r)) = ( dom f) & ( rng (f - r)) c= REAL by Def2, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      let r be Rational;

      :: original: -

      redefine

      func f - r -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f - r)) = ( dom f) & ( rng (f - r)) c= RAT by Def2, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      let r be Integer;

      :: original: -

      redefine

      func f - r -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (f - r)) = ( dom f) & ( rng (f - r)) c= INT by Def2, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      let r be Complex;

      cluster (f - r) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      let r be Real;

      cluster (f - r) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      let r be Rational;

      cluster (f - r) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      let r be Integer;

      cluster (f - r) -> total;

      coherence ;

    end

    theorem :: VALUED_1:4

    for C be non empty set, D be complex-membered non empty set holds for f be Function of C, D, r be Complex holds for c be Element of C holds ((f - r) . c) = ((f . c) - r)

    proof

      let C be non empty set;

      let D be complex-membered non empty set;

      let f be Function of C, D, r be Complex;

      ( dom (f - r)) = C by FUNCT_2:def 1;

      hence thesis by Def2;

    end;

    registration

      let f be complex-valued FinSequence, r be Complex;

      cluster (f - r) -> FinSequence-like;

      coherence ;

    end

    begin

    definition

      let f1,f2 be complex-valued Function;

      deffunc F( object) = ((f1 . $1) * (f2 . $1));

      set X = (( dom f1) /\ ( dom f2));

      :: VALUED_1:def4

      func f1 (#) f2 -> Function means

      : Def4: ( dom it ) = (( dom f1) /\ ( dom f2)) & for c be object st c in ( dom it ) holds (it . c) = ((f1 . c) * (f2 . c));

      existence

      proof

        ex f be Function st ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function such that

         A1: ( dom f) = X and

         A2: for c be object st c in ( dom f) holds (f . c) = F(c) and

         A3: ( dom g) = X and

         A4: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A5: x in ( dom f);

          

          hence (f . x) = F(x) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

      commutativity ;

    end

    theorem :: VALUED_1:5

    for f1,f2 be complex-valued Function holds for c be object holds ((f1 (#) f2) . c) = ((f1 . c) * (f2 . c))

    proof

      let f1,f2 be complex-valued Function;

      let c be object;

      

       A1: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def4;

      per cases ;

        suppose c in ( dom (f1 (#) f2));

        hence thesis by Def4;

      end;

        suppose

         A2: not c in ( dom (f1 (#) f2));

        then not c in ( dom f1) or not c in ( dom f2) by A1, XBOOLE_0:def 4;

        then (f1 . c) = 0 or (f2 . c) = 0 by FUNCT_1:def 2;

        hence thesis by A2, FUNCT_1:def 2;

      end;

    end;

    registration

      let f1,f2 be complex-valued Function;

      cluster (f1 (#) f2) -> complex-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 (#) f2));

        then ((f1 (#) f2) . x) = ((f1 . x) * (f2 . x)) by Def4;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be real-valued Function;

      cluster (f1 (#) f2) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 (#) f2));

        then ((f1 (#) f2) . x) = ((f1 . x) * (f2 . x)) by Def4;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be RAT -valued Function;

      cluster (f1 (#) f2) -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f1 (#) f2));

        then

        consider x be object such that

         A1: x in ( dom (f1 (#) f2)) and

         A2: ((f1 (#) f2) . x) = y by FUNCT_1:def 3;

        ((f1 (#) f2) . x) = ((f1 . x) * (f2 . x)) by A1, Def4;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    registration

      let f1,f2 be INT -valued Function;

      cluster (f1 (#) f2) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f1 (#) f2));

        then

        consider x be object such that

         A1: x in ( dom (f1 (#) f2)) and

         A2: ((f1 (#) f2) . x) = y by FUNCT_1:def 3;

        ((f1 (#) f2) . x) = ((f1 . x) * (f2 . x)) by A1, Def4;

        hence thesis by A2, INT_1:def 2;

      end;

    end

    registration

      let f1,f2 be natural-valued Function;

      cluster (f1 (#) f2) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f1 (#) f2));

        then ((f1 (#) f2) . x) = ((f1 . x) * (f2 . x)) by Def4;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D1,D2 be complex-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: (#)

      redefine

      func f1 (#) f2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 (#) f2)) c= COMPLEX by Def4, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be real-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: (#)

      redefine

      func f1 (#) f2 -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 (#) f2)) c= REAL by Def4, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be rational-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: (#)

      redefine

      func f1 (#) f2 -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 (#) f2)) c= RAT by Def4, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be integer-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: (#)

      redefine

      func f1 (#) f2 -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 (#) f2)) c= INT by Def4, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be natural-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: (#)

      redefine

      func f1 (#) f2 -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 (#) f2)) c= NAT by Def4, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 (#) f2)) = (C /\ C) by Def4

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be real-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 (#) f2)) = (C /\ C) by Def4

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be rational-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 (#) f2)) = (C /\ C) by Def4

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be integer-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 (#) f2)) = (C /\ C) by Def4

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D1,D2 be natural-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

        

        then ( dom (f1 (#) f2)) = (C /\ C) by Def4

        .= C;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let f1,f2 be complex-valued FinSequence;

      cluster (f1 (#) f2) -> FinSequence-like;

      coherence

      proof

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def4;

        hence thesis by Lm2;

      end;

    end

    begin

    definition

      let f be complex-valued Function, r be Complex;

      deffunc F( object) = (r * (f . $1));

      :: VALUED_1:def5

      func r (#) f -> Function means

      : Def5: ( dom it ) = ( dom f) & for c be object st c in ( dom it ) holds (it . c) = (r * (f . c));

      existence

      proof

        ex g be Function st ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let h,g be Function such that

         A1: ( dom h) = ( dom f) and

         A2: for c be object st c in ( dom h) holds (h . c) = F(c) and

         A3: ( dom g) = ( dom f) and

         A4: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A5: x in ( dom h);

          

          hence (h . x) = F(x) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    notation

      let f be complex-valued Function, r be Complex;

      synonym f (#) r for r (#) f;

    end

    theorem :: VALUED_1:6

    

     Th6: for f be complex-valued Function, r be Complex holds for c be object holds ((r (#) f) . c) = (r * (f . c))

    proof

      let f be complex-valued Function, r be Complex;

      let c be object;

      

       A1: ( dom f) = ( dom (r (#) f)) by Def5;

      per cases ;

        suppose c in ( dom f);

        hence thesis by A1, Def5;

      end;

        suppose

         A2: not c in ( dom f);

        

        hence ((r (#) f) . c) = (r * 0 ) by A1, FUNCT_1:def 2

        .= (r * (f . c)) by A2, FUNCT_1:def 2;

      end;

    end;

    registration

      let f be complex-valued Function, r be Complex;

      cluster (r (#) f) -> complex-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r (#) f));

        then ((r (#) f) . x) = (r * (f . x)) by Def5;

        hence thesis;

      end;

    end

    registration

      let f be real-valued Function, r be Real;

      cluster (r (#) f) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r (#) f));

        then ((r (#) f) . x) = (r * (f . x)) by Def5;

        hence thesis;

      end;

    end

    registration

      let f be RAT -valued Function, r be Rational;

      cluster (r (#) f) -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (r (#) f));

        then

        consider x be object such that

         A1: x in ( dom (r (#) f)) and

         A2: ((r (#) f) . x) = y by FUNCT_1:def 3;

        ((r (#) f) . x) = (r * (f . x)) by A1, Def5;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    registration

      let f be INT -valued Function, r be Integer;

      cluster (r (#) f) -> INT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (r (#) f));

        then

        consider x be object such that

         A1: x in ( dom (r (#) f)) and

         A2: ((r (#) f) . x) = y by FUNCT_1:def 3;

        ((r (#) f) . x) = (r * (f . x)) by A1, Def5;

        hence thesis by A2, INT_1:def 2;

      end;

    end

    registration

      let f be natural-valued Function, r be Nat;

      cluster (r (#) f) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (r (#) f));

        then ((r (#) f) . x) = (r * (f . x)) by Def5;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      let r be Complex;

      :: original: (#)

      redefine

      func r (#) f -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) & ( rng (r (#) f)) c= COMPLEX by Def5, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      let r be Real;

      :: original: (#)

      redefine

      func r (#) f -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) & ( rng (r (#) f)) c= REAL by Def5, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      let r be Rational;

      :: original: (#)

      redefine

      func r (#) f -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) & ( rng (r (#) f)) c= RAT by Def5, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      let r be Integer;

      :: original: (#)

      redefine

      func r (#) f -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) & ( rng (r (#) f)) c= INT by Def5, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be natural-membered set;

      let f be PartFunc of C, D;

      let r be Nat;

      :: original: (#)

      redefine

      func r (#) f -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) & ( rng (r (#) f)) c= NAT by Def5, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      let r be Complex;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      let r be Real;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      let r be Rational;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      let r be Integer;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be natural-membered non empty set;

      let f be Function of C, D;

      let r be Nat;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: VALUED_1:7

    for C be non empty set, D be complex-membered non empty set holds for f be Function of C, D, r be Complex holds for g be Function of C, COMPLEX st for c be Element of C holds (g . c) = (r * (f . c)) holds g = (r (#) f)

    proof

      let C be non empty set, D be complex-membered non empty set;

      let f be Function of C, D, r be Complex;

      let g be Function of C, COMPLEX such that

       A1: for c be Element of C holds (g . c) = (r * (f . c));

      let x be Element of C;

      

      thus (g . x) = (r * (f . x)) by A1

      .= ((r (#) f) . x) by Th6;

    end;

    registration

      let f be complex-valued FinSequence, r be Complex;

      cluster (r (#) f) -> FinSequence-like;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def5;

        hence thesis by Lm1;

      end;

    end

    begin

    definition

      let f be complex-valued Function;

      :: VALUED_1:def6

      func - f -> complex-valued Function equals (( - 1) (#) f);

      coherence ;

      involutiveness

      proof

        let r,h be complex-valued Function;

        assume

         A1: r = (( - 1) (#) h);

        

        thus ( dom (( - 1) (#) r)) = ( dom r) by Def5

        .= ( dom h) by A1, Def5;

        let c be object;

        assume c in ( dom h);

        reconsider a = (( - 1) * (h . c)) as Complex;

        

        thus (h . c) = (( - 1) * a)

        .= (( - 1) * (r . c)) by A1, Th6

        .= ((( - 1) (#) r) . c) by Th6;

      end;

    end

    theorem :: VALUED_1:8

    

     Th8: for f be complex-valued Function holds ( dom ( - f)) = ( dom f) & for c be object holds (( - f) . c) = ( - (f . c))

    proof

      let f be complex-valued Function;

      thus

       A1: ( dom ( - f)) = ( dom f) by Def5;

      let c be object;

      per cases ;

        suppose c in ( dom f);

        

        hence (( - f) . c) = (( - 1) * (f . c)) by A1, Def5

        .= ( - (f . c));

      end;

        suppose

         A2: not c in ( dom f);

        

        hence (( - f) . c) = ( - 0 qua Complex) by A1, FUNCT_1:def 2

        .= ( - (f . c)) by A2, FUNCT_1:def 2;

      end;

    end;

    theorem :: VALUED_1:9

    for f be complex-valued Function, g be Function st ( dom f) = ( dom g) & for c be object st c in ( dom f) holds (g . c) = ( - (f . c)) holds g = ( - f)

    proof

      let f be complex-valued Function, g be Function;

      assume that

       A1: ( dom f) = ( dom g) and

       A2: for c be object st c in ( dom f) holds (g . c) = ( - (f . c));

      thus ( dom ( - f)) = ( dom g) by A1, Def5;

      let c be object;

      assume

       A3: c in ( dom g);

      

      thus (( - f) . c) = ( - (f . c)) by Th8

      .= (g . c) by A1, A2, A3;

    end;

    registration

      let f be complex-valued Function;

      cluster ( - f) -> complex-valued;

      coherence ;

    end

    registration

      let f be real-valued Function;

      cluster ( - f) -> real-valued;

      coherence ;

    end

    registration

      let f be RAT -valued Function;

      cluster ( - f) -> RAT -valued;

      coherence ;

    end

    registration

      let f be INT -valued Function;

      cluster ( - f) -> INT -valued;

      coherence ;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      :: original: -

      redefine

      func - f -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom ( - f)) = ( dom f) & ( rng ( - f)) c= COMPLEX by Def5, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      :: original: -

      redefine

      func - f -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom ( - f)) = ( dom f) & ( rng ( - f)) c= REAL by Def5, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      :: original: -

      redefine

      func - f -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom ( - f)) = ( dom f) & ( rng ( - f)) c= RAT by Def5, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      :: original: -

      redefine

      func - f -> PartFunc of C, INT ;

      coherence

      proof

        ( dom ( - f)) = ( dom f) & ( rng ( - f)) c= INT by Def5, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      cluster ( - f) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      cluster ( - f) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      cluster ( - f) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      cluster ( - f) -> total;

      coherence ;

    end

    registration

      let f be complex-valued FinSequence;

      cluster ( - f) -> FinSequence-like;

      coherence ;

    end

    begin

    definition

      let f be complex-valued Function;

      deffunc F( object) = ((f . $1) " );

      :: VALUED_1:def7

      func f " -> complex-valued Function means

      : Def7: ( dom it ) = ( dom f) & for c be object st c in ( dom it ) holds (it . c) = ((f . c) " );

      existence

      proof

        consider g be Function such that

         A1: ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        g is complex-valued

        proof

          let x be object;

          assume x in ( dom g);

          then (g . x) = ((f . x) " ) by A1;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let h,g be complex-valued Function such that

         A2: ( dom h) = ( dom f) and

         A3: for c be object st c in ( dom h) holds (h . c) = F(c) and

         A4: ( dom g) = ( dom f) and

         A5: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A6: x in ( dom h);

          

          hence (h . x) = F(x) by A3

          .= (g . x) by A2, A4, A5, A6;

        end;

        hence thesis by A2, A4;

      end;

      involutiveness

      proof

        let r,h be complex-valued Function;

        assume that

         A7: ( dom r) = ( dom h) and

         A8: for c be object st c in ( dom r) holds (r . c) = ((h . c) " );

        thus ( dom r) = ( dom h) by A7;

        let c be object;

        assume

         A9: c in ( dom h);

        

        thus (h . c) = (((h . c) " ) " )

        .= ((r . c) " ) by A7, A8, A9;

      end;

    end

    theorem :: VALUED_1:10

    

     Th10: for f be complex-valued Function holds for c be object holds ((f " ) . c) = ((f . c) " )

    proof

      let f be complex-valued Function;

      let c be object;

      

       A1: ( dom (f " )) = ( dom f) by Def7;

      per cases ;

        suppose c in ( dom f);

        hence thesis by A1, Def7;

      end;

        suppose

         A2: not c in ( dom f);

        

        hence ((f " ) . c) = ( 0 qua Complex " ) by A1, FUNCT_1:def 2

        .= ((f . c) " ) by A2, FUNCT_1:def 2;

      end;

    end;

    registration

      let f be real-valued Function;

      cluster (f " ) -> real-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom (f " ));

        then ((f " ) . x) = ((f . x) " ) by Def7;

        hence thesis;

      end;

    end

    registration

      let f be RAT -valued Function;

      cluster (f " ) -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng (f " ));

        then

        consider x be object such that

         A1: x in ( dom (f " )) and

         A2: ((f " ) . x) = y by FUNCT_1:def 3;

        ((f " ) . x) = ((f . x) " ) by A1, Def7;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      :: original: "

      redefine

      func f " -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f " )) = ( dom f) & ( rng (f " )) c= COMPLEX by Def7, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      :: original: "

      redefine

      func f " -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f " )) = ( dom f) & ( rng (f " )) c= REAL by Def7, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      :: original: "

      redefine

      func f " -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f " )) = ( dom f) & ( rng (f " )) c= RAT by Def7, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      cluster (f " ) -> total;

      coherence

      proof

        ( dom (f " )) = ( dom f) by Def7

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      cluster (f " ) -> total;

      coherence

      proof

        ( dom (f " )) = ( dom f) by Def7

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      cluster (f " ) -> total;

      coherence

      proof

        ( dom (f " )) = ( dom f) by Def7

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let f be complex-valued FinSequence;

      cluster (f " ) -> FinSequence-like;

      coherence

      proof

        ( dom (f " )) = ( dom f) by Def7;

        hence thesis by Lm1;

      end;

    end

    begin

    definition

      let f be complex-valued Function;

      :: VALUED_1:def8

      func f ^2 -> Function equals (f (#) f);

      coherence ;

    end

    theorem :: VALUED_1:11

    

     Th11: for f be complex-valued Function holds ( dom (f ^2 )) = ( dom f) & for c be object holds ((f ^2 ) . c) = ((f . c) ^2 )

    proof

      let f be complex-valued Function;

      

      thus

       A1: ( dom (f ^2 )) = (( dom f) /\ ( dom f)) by Def4

      .= ( dom f);

      let c be object;

      per cases ;

        suppose c in ( dom f);

        hence thesis by A1, Def4;

      end;

        suppose

         A2: not c in ( dom f);

        

        hence ((f ^2 ) . c) = ( 0 qua Complex ^2 ) by A1, FUNCT_1:def 2

        .= ((f . c) ^2 ) by A2, FUNCT_1:def 2;

      end;

    end;

    registration

      let f be complex-valued Function;

      cluster (f ^2 ) -> complex-valued;

      coherence ;

    end

    registration

      let f be real-valued Function;

      cluster (f ^2 ) -> real-valued;

      coherence ;

    end

    registration

      let f be RAT -valued Function;

      cluster (f ^2 ) -> RAT -valued;

      coherence ;

    end

    registration

      let f be INT -valued Function;

      cluster (f ^2 ) -> INT -valued;

      coherence ;

    end

    registration

      let f be natural-valued Function;

      cluster (f ^2 ) -> natural-valued;

      coherence ;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      :: original: ^2

      redefine

      func f ^2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) & ( rng (f ^2 )) c= COMPLEX by Th11, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      :: original: ^2

      redefine

      func f ^2 -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) & ( rng (f ^2 )) c= REAL by Th11, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      :: original: ^2

      redefine

      func f ^2 -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) & ( rng (f ^2 )) c= RAT by Th11, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      :: original: ^2

      redefine

      func f ^2 -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) & ( rng (f ^2 )) c= INT by Th11, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be natural-membered set;

      let f be PartFunc of C, D;

      :: original: ^2

      redefine

      func f ^2 -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) & ( rng (f ^2 )) c= NAT by Th11, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      cluster (f ^2 ) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be real-membered non empty set;

      let f be Function of C, D;

      cluster (f ^2 ) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      cluster (f ^2 ) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      cluster (f ^2 ) -> total;

      coherence ;

    end

    registration

      let C be set;

      let D be natural-membered non empty set;

      let f be Function of C, D;

      cluster (f ^2 ) -> total;

      coherence ;

    end

    registration

      let f be complex-valued FinSequence;

      cluster (f ^2 ) -> FinSequence-like;

      coherence ;

    end

    begin

    definition

      let f1,f2 be complex-valued Function;

      :: VALUED_1:def9

      func f1 - f2 -> Function equals (f1 + ( - f2));

      coherence ;

    end

    registration

      let f1,f2 be complex-valued Function;

      cluster (f1 - f2) -> complex-valued;

      coherence ;

    end

    registration

      let f1,f2 be real-valued Function;

      cluster (f1 - f2) -> real-valued;

      coherence ;

    end

    registration

      let f1,f2 be RAT -valued Function;

      cluster (f1 - f2) -> RAT -valued;

      coherence ;

    end

    registration

      let f1,f2 be INT -valued Function;

      cluster (f1 - f2) -> INT -valued;

      coherence ;

    end

    theorem :: VALUED_1:12

    

     Th12: for f1,f2 be complex-valued Function holds ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2))

    proof

      let f1,f2 be complex-valued Function;

      

      thus ( dom (f1 - f2)) = (( dom f1) /\ ( dom ( - f2))) by Def1

      .= (( dom f1) /\ ( dom f2)) by Def5;

    end;

    theorem :: VALUED_1:13

    for f1,f2 be complex-valued Function holds for c be object st c in ( dom (f1 - f2)) holds ((f1 - f2) . c) = ((f1 . c) - (f2 . c))

    proof

      let f1,f2 be complex-valued Function;

      let c be object;

      assume c in ( dom (f1 - f2));

      

      hence ((f1 - f2) . c) = ((f1 . c) + (( - f2) . c)) by Def1

      .= ((f1 . c) - (f2 . c)) by Th8;

    end;

    theorem :: VALUED_1:14

    for f1,f2 be complex-valued Function, f be Function st ( dom f) = ( dom (f1 - f2)) & for c be object st c in ( dom f) holds (f . c) = ((f1 . c) - (f2 . c)) holds f = (f1 - f2)

    proof

      let f1,f2 be complex-valued Function, f be Function such that

       A1: ( dom f) = ( dom (f1 - f2)) and

       A2: for c be object st c in ( dom f) holds (f . c) = ((f1 . c) - (f2 . c));

      thus ( dom f) = ( dom (f1 - f2)) by A1;

      let c be object;

      assume

       A3: c in ( dom f);

      

      hence (f . c) = ((f1 . c) - (f2 . c)) by A2

      .= ((f1 . c) + (( - f2) . c)) by Th8

      .= ((f1 - f2) . c) by A1, A3, Def1;

    end;

    definition

      let C be set;

      let D1,D2 be complex-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: -

      redefine

      func f1 - f2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 - f2)) c= COMPLEX by Th12, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be real-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: -

      redefine

      func f1 - f2 -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 - f2)) c= REAL by Th12, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be rational-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: -

      redefine

      func f1 - f2 -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 - f2)) c= RAT by Th12, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be integer-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: -

      redefine

      func f1 - f2 -> PartFunc of C, INT ;

      coherence

      proof

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 - f2)) c= INT by Th12, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    

     Lm3: for C be set, D1,D2 be complex-membered non empty set, f1 be Function of C, D1, f2 be Function of C, D2 holds ( dom (f1 - f2)) = C

    proof

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      

      thus ( dom (f1 - f2)) = (( dom f1) /\ ( dom ( - f2))) by Def1

      .= (C /\ ( dom ( - f2))) by FUNCT_2:def 1

      .= (C /\ C) by FUNCT_2:def 1

      .= C;

    end;

    registration

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 - f2) -> total;

      coherence by Lm3, PARTFUN1:def 2;

    end

    registration

      let C be set;

      let D1,D2 be real-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 - f2) -> total;

      coherence by Lm3, PARTFUN1:def 2;

    end

    registration

      let C be set;

      let D1,D2 be rational-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 - f2) -> total;

      coherence by Lm3, PARTFUN1:def 2;

    end

    registration

      let C be set;

      let D1,D2 be integer-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 - f2) -> total;

      coherence by Lm3, PARTFUN1:def 2;

    end

    theorem :: VALUED_1:15

    for C be set, D1,D2 be complex-membered non empty set holds for f1 be Function of C, D1, f2 be Function of C, D2 holds for c be Element of C holds ((f1 - f2) . c) = ((f1 . c) - (f2 . c))

    proof

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1, f2 be Function of C, D2;

      let c be Element of C;

      

       A1: ( dom (f1 - f2)) = C by FUNCT_2:def 1;

      per cases ;

        suppose C is non empty;

        

        hence ((f1 - f2) . c) = ((f1 . c) + (( - f2) . c)) by A1, Def1

        .= ((f1 . c) - (f2 . c)) by Th8;

      end;

        suppose

         A2: C is empty;

        then (f2 . c) = 0 ;

        hence thesis by A2;

      end;

    end;

    registration

      let f1,f2 be complex-valued FinSequence;

      cluster (f1 - f2) -> FinSequence-like;

      coherence ;

    end

    begin

    definition

      let f1,f2 be complex-valued Function;

      :: VALUED_1:def10

      func f1 /" f2 -> Function equals (f1 (#) (f2 " ));

      coherence ;

    end

    theorem :: VALUED_1:16

    

     Th16: for f1,f2 be complex-valued Function holds ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2))

    proof

      let f1,f2 be complex-valued Function;

      

      thus ( dom (f1 /" f2)) = (( dom f1) /\ ( dom (f2 " ))) by Def4

      .= (( dom f1) /\ ( dom f2)) by Def7;

    end;

    theorem :: VALUED_1:17

    for f1,f2 be complex-valued Function holds for c be object holds ((f1 /" f2) . c) = ((f1 . c) / (f2 . c))

    proof

      let f1,f2 be complex-valued Function;

      let c be object;

      

       A1: ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2)) by Th16;

      per cases ;

        suppose c in ( dom (f1 /" f2));

        

        hence ((f1 /" f2) . c) = ((f1 . c) * ((f2 " ) . c)) by Def4

        .= ((f1 . c) / (f2 . c)) by Th10;

      end;

        suppose

         A2: not c in ( dom (f1 /" f2));

        then not c in ( dom f1) or not c in ( dom f2) by A1, XBOOLE_0:def 4;

        then

         A3: (f1 . c) = 0 or (f2 . c) = 0 by FUNCT_1:def 2;

        

        thus ((f1 /" f2) . c) = ( 0 / 0 ) by A2, FUNCT_1:def 2

        .= ((f1 . c) / (f2 . c)) by A3;

      end;

    end;

    registration

      let f1,f2 be complex-valued Function;

      cluster (f1 /" f2) -> complex-valued;

      coherence ;

    end

    registration

      let f1,f2 be real-valued Function;

      cluster (f1 /" f2) -> real-valued;

      coherence ;

    end

    registration

      let f1,f2 be RAT -valued Function;

      cluster (f1 /" f2) -> RAT -valued;

      coherence ;

    end

    definition

      let C be set;

      let D1,D2 be complex-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: /"

      redefine

      func f1 /" f2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 /" f2)) c= COMPLEX by Th16, VALUED_0:def 1;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be real-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: /"

      redefine

      func f1 /" f2 -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 /" f2)) c= REAL by Th16, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D1,D2 be rational-membered set;

      let f1 be PartFunc of C, D1;

      let f2 be PartFunc of C, D2;

      :: original: /"

      redefine

      func f1 /" f2 -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2)) & ( rng (f1 /" f2)) c= RAT by Th16, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    

     Lm4: for C be set, D1,D2 be complex-membered non empty set holds for f1 be Function of C, D1, f2 be Function of C, D2 holds ( dom (f1 /" f2)) = C

    proof

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1, f2 be Function of C, D2;

      

      thus ( dom (f1 /" f2)) = (( dom f1) /\ ( dom f2)) by Th16

      .= (C /\ ( dom f2)) by FUNCT_2:def 1

      .= (C /\ C) by FUNCT_2:def 1

      .= C;

    end;

    registration

      let C be set;

      let D1,D2 be complex-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 /" f2) -> total;

      coherence by Lm4, PARTFUN1:def 2;

    end

    registration

      let C be set;

      let D1,D2 be real-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 /" f2) -> total;

      coherence by Lm4, PARTFUN1:def 2;

    end

    registration

      let C be set;

      let D1,D2 be rational-membered non empty set;

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      cluster (f1 /" f2) -> total;

      coherence by Lm4, PARTFUN1:def 2;

    end

    registration

      let f1,f2 be complex-valued FinSequence;

      cluster (f1 /" f2) -> FinSequence-like;

      coherence ;

    end

    begin

    definition

      let f be complex-valued Function;

      deffunc F( object) = |.(f . $1).|;

      :: VALUED_1:def11

      func |.f.| -> real-valued Function means

      : Def11: ( dom it ) = ( dom f) & for c be object st c in ( dom it ) holds (it . c) = |.(f . c).|;

      existence

      proof

        consider g be Function such that

         A1: ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        g is real-valued

        proof

          let x be object;

          assume x in ( dom g);

          then (g . x) = |.(f . x).| by A1;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let h,g be real-valued Function such that

         A2: ( dom h) = ( dom f) and

         A3: for c be object st c in ( dom h) holds (h . c) = F(c) and

         A4: ( dom g) = ( dom f) and

         A5: for c be object st c in ( dom g) holds (g . c) = F(c);

        now

          let x be object;

          assume

           A6: x in ( dom h);

          

          hence (h . x) = F(x) by A3

          .= (g . x) by A2, A4, A5, A6;

        end;

        hence thesis by A2, A4;

      end;

      projectivity

      proof

        let r be real-valued Function;

        let h be complex-valued Function;

        assume that ( dom r) = ( dom h) and

         A7: for c be object st c in ( dom r) holds (r . c) = |.(h . c).|;

        thus ( dom r) = ( dom r);

        let c be object;

        assume

         A8: c in ( dom r);

        

        hence (r . c) = |. |.(h . c).|.| by A7

        .= |.(r . c).| by A7, A8;

      end;

    end

    notation

      let f be complex-valued Function;

      synonym abs f for |.f.|;

    end

    theorem :: VALUED_1:18

    for f be complex-valued Function holds for c be object holds ( |.f.| . c) = |.(f . c).|

    proof

      let f be complex-valued Function;

      let c be object;

      

       A1: ( dom |.f.|) = ( dom f) by Def11;

      per cases ;

        suppose c in ( dom f);

        hence thesis by A1, Def11;

      end;

        suppose

         A2: not c in ( dom f);

        

        hence ( |.f.| . c) = |. 0 qua Complex.| by A1, COMPLEX1: 44, FUNCT_1:def 2

        .= |.(f . c).| by A2, FUNCT_1:def 2;

      end;

    end;

    registration

      let f be RAT -valued Function;

      cluster |.f.| -> RAT -valued;

      coherence

      proof

        let y be object;

        assume y in ( rng |.f.|);

        then

        consider x be object such that

         A1: x in ( dom |.f.|) and

         A2: ( |.f.| . x) = y by FUNCT_1:def 3;

        ( |.f.| . x) = |.(f . x).| by A1, Def11;

        hence thesis by A2, RAT_1:def 2;

      end;

    end

    registration

      let f be INT -valued Function;

      cluster |.f.| -> natural-valued;

      coherence

      proof

        let x be object;

         |.(f . x).| is natural;

        hence thesis by Def11;

      end;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      :: original: |.

      redefine

      func |.f.| -> PartFunc of C, REAL ;

      coherence

      proof

        ( dom |.f.|) = ( dom f) & ( rng |.f.|) c= REAL by Def11, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be complex-membered set;

      let f be PartFunc of C, D;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of C, REAL ;

      coherence

      proof

        ( abs f) = |.f.|;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      :: original: |.

      redefine

      func |.f.| -> PartFunc of C, RAT ;

      coherence

      proof

        ( dom |.f.|) = ( dom f) & ( rng |.f.|) c= RAT by Def11, RELAT_1:def 19;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be rational-membered set;

      let f be PartFunc of C, D;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of C, RAT ;

      coherence

      proof

        ( abs f) = |.f.|;

        hence thesis;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      :: original: |.

      redefine

      func |.f.| -> PartFunc of C, NAT ;

      coherence

      proof

        ( dom |.f.|) = ( dom f) & ( rng |.f.|) c= NAT by Def11, VALUED_0:def 6;

        hence thesis by RELSET_1: 4;

      end;

    end

    definition

      let C be set;

      let D be integer-membered set;

      let f be PartFunc of C, D;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of C, NAT ;

      coherence

      proof

        ( abs f) = |.f.|;

        hence thesis;

      end;

    end

    registration

      let C be set;

      let D be complex-membered non empty set;

      let f be Function of C, D;

      cluster |.f.| -> total;

      coherence

      proof

        ( dom |.f.|) = ( dom f) by Def11

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be rational-membered non empty set;

      let f be Function of C, D;

      cluster |.f.| -> total;

      coherence

      proof

        ( dom |.f.|) = ( dom f) by Def11

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let C be set;

      let D be integer-membered non empty set;

      let f be Function of C, D;

      cluster |.f.| -> total;

      coherence

      proof

        ( dom |.f.|) = ( dom f) by Def11

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let f be complex-valued FinSequence;

      cluster |.f.| -> FinSequence-like;

      coherence

      proof

        ( dom ( abs f)) = ( dom f) by Def11;

        hence thesis by Lm1;

      end;

    end

    theorem :: VALUED_1:19

    for f,g be FinSequence, h be Function st ( dom h) = (( dom f) /\ ( dom g)) holds h is FinSequence by Lm2;

    begin

    reserve m,j,p,q,n,l for Element of NAT ;

    definition

      let p be Function, k be Nat;

      :: VALUED_1:def12

      func Shift (p,k) -> Function means

      : Def12: ( dom it ) = { (m + k) where m be Nat : m in ( dom p) } & for m be Nat st m in ( dom p) holds (it . (m + k)) = (p . m);

      existence

      proof

        defpred P[ object, object] means ex m be Nat st $1 = (m + k) & $2 = (p . m);

        set A = { (m + k) where m be Nat : m in ( dom p) };

        

         A1: for e be object st e in A holds ex u be object st P[e, u]

        proof

          let e be object;

          assume e in A;

          then

          consider m be Nat such that

           A2: e = (m + k) and m in ( dom p);

          take (p . m);

          thus thesis by A2;

        end;

        consider f be Function such that

         A3: ( dom f) = A and

         A4: for e be object st e in A holds P[e, (f . e)] from CLASSES1:sch 1( A1);

        take f;

        thus ( dom f) = { (m + k) where m be Nat : m in ( dom p) } by A3;

        let m be Nat;

        assume m in ( dom p);

        then (m + k) in A;

        then ex j be Nat st (m + k) = (j + k) & (f . (m + k)) = (p . j) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function such that

         A5: ( dom IT1) = { (m + k) where m be Nat : m in ( dom p) } and

         A6: for m be Nat st m in ( dom p) holds (IT1 . (m + k)) = (p . m) and

         A7: ( dom IT2) = { (m + k) where m be Nat : m in ( dom p) } and

         A8: for m be Nat st m in ( dom p) holds (IT2 . (m + k)) = (p . m);

        for x be object st x in ( dom IT1) holds (IT1 . x) = (IT2 . x)

        proof

          let x be object;

          assume x in ( dom IT1);

          then

          consider m be Nat such that

           A9: x = (m + k) & m in ( dom p) by A5;

          

          thus (IT1 . x) = (p . m) by A6, A9

          .= (IT2 . x) by A8, A9;

        end;

        hence thesis by A5, A7;

      end;

    end

    registration

      let p be Function, k be Nat;

      cluster ( Shift (p,k)) -> NAT -defined;

      coherence

      proof

        

         A1: ( dom ( Shift (p,k))) = { (m + k) where m be Nat : m in ( dom p) } by Def12;

        ( Shift (p,k)) is NAT -defined

        proof

          let x be object;

          assume x in ( dom ( Shift (p,k)));

          then ex m be Nat st x = (m + k) & m in ( dom p) by A1;

          hence thesis by ORDINAL1:def 12;

        end;

        hence thesis;

      end;

    end

    theorem :: VALUED_1:20

    for P,Q be Function, k be Nat st P c= Q holds ( Shift (P,k)) c= ( Shift (Q,k))

    proof

      let P,Q be Function;

      let k be Nat;

      assume

       A1: P c= Q;

      then

       A2: ( dom P) c= ( dom Q) by GRFUNC_1: 2;

      

       A3: ( dom ( Shift (P,k))) = { (m + k) where m be Nat : m in ( dom P) } by Def12;

      

       A4: ( dom ( Shift (Q,k))) = { (m + k) where m be Nat : m in ( dom Q) } by Def12;

       A5:

      now

        let x be object;

        assume x in ( dom ( Shift (P,k)));

        then ex m1 be Nat st x = (m1 + k) & m1 in ( dom P) by A3;

        hence x in ( dom ( Shift (Q,k))) by A2, A4;

      end;

      now

        let x be object;

        assume x in ( dom ( Shift (P,k)));

        then

        consider m1 be Nat such that

         A6: x = (m1 + k) and

         A7: m1 in ( dom P) by A3;

        

        thus (( Shift (P,k)) . x) = (( Shift (P,k)) . (m1 + k)) by A6

        .= (P . m1) by A7, Def12

        .= (Q . m1) by A1, A7, GRFUNC_1: 2

        .= (( Shift (Q,k)) . (m1 + k)) by A2, A7, Def12

        .= (( Shift (Q,k)) . x) by A6;

      end;

      hence thesis by A5, GRFUNC_1: 2, TARSKI:def 3;

    end;

    theorem :: VALUED_1:21

    for n,m be Nat holds for I be Function holds ( Shift (( Shift (I,m)),n)) = ( Shift (I,(m + n)))

    proof

      let n,m be Nat;

      let I be Function;

      set A = { (l + m) where l be Nat : l in ( dom I) };

      

       A1: ( dom ( Shift (I,m))) = A by Def12;

       A2:

      now

        let l be Nat;

        assume

         A3: l in ( dom I);

        then

         A4: (l + m) in ( dom ( Shift (I,m))) by A1;

        

        thus (( Shift (( Shift (I,m)),n)) . (l + (m + n))) = (( Shift (( Shift (I,m)),n)) . ((l + m) + n))

        .= (( Shift (I,m)) . (l + m)) by A4, Def12

        .= (I . l) by A3, Def12;

      end;

      { (p + n) where p be Nat : p in A } = { (q + (m + n)) where q be Nat : q in ( dom I) }

      proof

        thus { (p + n) where p be Nat : p in A } c= { (q + (m + n)) where q be Nat : q in ( dom I) }

        proof

          let x be object;

          assume x in { (p + n) where p be Nat : p in A };

          then

          consider p be Nat such that

           A5: x = (p + n) and

           A6: p in A;

          consider l be Nat such that

           A7: p = (l + m) and

           A8: l in ( dom I) by A6;

          x = (l + (m + n)) by A5, A7;

          hence thesis by A8;

        end;

        let x be object;

        assume x in { (q + (m + n)) where q be Nat : q in ( dom I) };

        then

        consider q be Nat such that

         A9: x = (q + (m + n)) & q in ( dom I);

        x = ((q + m) + n) & (q + m) in A by A9;

        hence thesis;

      end;

      then ( dom ( Shift (( Shift (I,m)),n))) = { (l + (m + n)) where l be Nat : l in ( dom I) } by A1, Def12;

      hence thesis by A2, Def12;

    end;

    theorem :: VALUED_1:22

    for s,f be Function holds for n be Nat holds ( Shift ((f * s),n)) = (f * ( Shift (s,n)))

    proof

      let s,f be Function;

      let n be Nat;

      

       A1: ( dom (f * s)) c= ( dom s) by RELAT_1: 25;

      

       A2: ( dom ( Shift (s,n))) = { (m + n) where m be Nat : m in ( dom s) } by Def12;

      now

        let e be object;

        thus e in { (m + n) where m be Nat : m in ( dom (f * s)) } implies e in ( dom ( Shift (s,n))) & (( Shift (s,n)) . e) in ( dom f)

        proof

          assume e in { (m + n) where m be Nat : m in ( dom (f * s)) };

          then

          consider m be Nat such that

           A3: e = (m + n) and

           A4: m in ( dom (f * s));

          thus e in ( dom ( Shift (s,n))) by A2, A1, A3, A4;

          (( Shift (s,n)) . e) = (s . m) by A1, A3, A4, Def12;

          hence thesis by A4, FUNCT_1: 11;

        end;

        assume e in ( dom ( Shift (s,n)));

        then

        consider m0 be Nat such that

         A5: e = (m0 + n) and

         A6: m0 in ( dom s) by A2;

        assume (( Shift (s,n)) . e) in ( dom f);

        then (s . m0) in ( dom f) by A5, A6, Def12;

        then m0 in ( dom (f * s)) by A6, FUNCT_1: 11;

        hence e in { (m + n) where m be Nat : m in ( dom (f * s)) } by A5;

      end;

      then (( Shift (s,n)) " ( dom f)) = { (m + n) where m be Nat : m in ( dom (f * s)) } by FUNCT_1:def 7;

      then

       A7: ( dom (f * ( Shift (s,n)))) = { (m + n) where m be Nat : m in ( dom (f * s)) } by RELAT_1: 147;

      now

        let m be Nat;

        assume

         A8: m in ( dom (f * s));

        then (m + n) in ( dom ( Shift (s,n))) by A2, A1;

        

        hence ((f * ( Shift (s,n))) . (m + n)) = (f . (( Shift (s,n)) . (m + n))) by FUNCT_1: 13

        .= (f . (s . m)) by A1, A8, Def12

        .= ((f * s) . m) by A8, FUNCT_1: 12;

      end;

      hence thesis by A7, Def12;

    end;

    theorem :: VALUED_1:23

    for I,J be Function, n be Nat holds ( Shift ((I +* J),n)) = (( Shift (I,n)) +* ( Shift (J,n)))

    proof

      let I,J be Function, n be Nat;

      

       A1: ( dom ( Shift (J,n))) = { (m + n) where m be Nat : m in ( dom J) } by Def12;

       A2:

      now

        let m be Nat such that

         A3: m in ( dom (I +* J));

        per cases ;

          suppose

           A4: m in ( dom J);

          then (m + n) in ( dom ( Shift (J,n))) by A1;

          

          hence ((( Shift (I,n)) +* ( Shift (J,n))) . (m + n)) = (( Shift (J,n)) . (m + n)) by FUNCT_4: 13

          .= (J . m) by A4, Def12

          .= ((I +* J) . m) by A4, FUNCT_4: 13;

        end;

          suppose

           A5: not m in ( dom J);

          m in (( dom I) \/ ( dom J)) by A3, FUNCT_4:def 1;

          then

           A6: m in ( dom I) by A5, XBOOLE_0:def 3;

           not ex l be Nat st (m + n) = (l + n) & l in ( dom J) by A5;

          then not (m + n) in ( dom ( Shift (J,n))) by A1;

          

          hence ((( Shift (I,n)) +* ( Shift (J,n))) . (m + n)) = (( Shift (I,n)) . (m + n)) by FUNCT_4: 11

          .= (I . m) by A6, Def12

          .= ((I +* J) . m) by A5, FUNCT_4: 11;

        end;

      end;

      

       A7: ( dom ( Shift (I,n))) = { (m + n) where m be Nat : m in ( dom I) } by Def12;

      

       A8: (( dom ( Shift (I,n))) \/ ( dom ( Shift (J,n)))) = { (m + n) where m be Nat : m in (( dom I) \/ ( dom J)) }

      proof

        hereby

          let x be object;

          assume x in (( dom ( Shift (I,n))) \/ ( dom ( Shift (J,n))));

          then x in ( dom ( Shift (I,n))) or x in ( dom ( Shift (J,n))) by XBOOLE_0:def 3;

          then

          consider m be Nat such that

           A9: x = (m + n) & m in ( dom J) or x = (m + n) & m in ( dom I) by A1, A7;

          m in (( dom I) \/ ( dom J)) by A9, XBOOLE_0:def 3;

          hence x in { (l + n) where l be Nat : l in (( dom I) \/ ( dom J)) } by A9;

        end;

        let x be object;

        assume x in { (m + n) where m be Nat : m in (( dom I) \/ ( dom J)) };

        then

        consider m be Nat such that

         A10: x = (m + n) and

         A11: m in (( dom I) \/ ( dom J));

        m in ( dom I) or m in ( dom J) by A11, XBOOLE_0:def 3;

        then x in ( dom ( Shift (I,n))) or x in ( dom ( Shift (J,n))) by A1, A7, A10;

        hence thesis by XBOOLE_0:def 3;

      end;

      ( dom (I +* J)) = (( dom I) \/ ( dom J)) by FUNCT_4:def 1;

      then ( dom (( Shift (I,n)) +* ( Shift (J,n)))) = { (m + n) where m be Nat : m in ( dom (I +* J)) } by A8, FUNCT_4:def 1;

      hence thesis by A2, Def12;

    end;

    theorem :: VALUED_1:24

    

     Th24: for p be Function, k,il be Nat st il in ( dom p) holds (il + k) in ( dom ( Shift (p,k)))

    proof

      let p be Function, k,il be Nat such that

       A1: il in ( dom p);

      ( dom ( Shift (p,k))) = { (loc + k) where loc be Nat : loc in ( dom p) } by Def12;

      hence thesis by A1;

    end;

    theorem :: VALUED_1:25

    

     Th25: for p be Function, k be Nat holds ( rng ( Shift (p,k))) c= ( rng p)

    proof

      let p be Function, k be Nat;

      let y be object;

      assume y in ( rng ( Shift (p,k)));

      then

      consider x be object such that

       A1: x in ( dom ( Shift (p,k))) and

       A2: y = (( Shift (p,k)) . x) by FUNCT_1:def 3;

      x in { (m + k) where m be Nat : m in ( dom p) } by A1, Def12;

      then

      consider m be Nat such that

       A3: x = (m + k) and

       A4: m in ( dom p);

      (p . m) = (( Shift (p,k)) . x) by A3, A4, Def12;

      hence thesis by A2, A4, FUNCT_1:def 3;

    end;

    theorem :: VALUED_1:26

    for p be Function st ( dom p) c= NAT holds for k be Nat holds ( rng ( Shift (p,k))) = ( rng p)

    proof

      let p be Function such that

       A1: ( dom p) c= NAT ;

      let k be Nat;

      thus ( rng ( Shift (p,k))) c= ( rng p) by Th25;

      let y be object;

      assume y in ( rng p);

      then

      consider x be object such that

       A2: x in ( dom p) and

       A3: y = (p . x) by FUNCT_1:def 3;

      reconsider x as Element of NAT by A1, A2;

      (x + k) in ( dom ( Shift (p,k))) & (( Shift (p,k)) . (x + k)) = y by A2, A3, Def12, Th24;

      hence thesis by FUNCT_1:def 3;

    end;

    registration

      let p be finite Function, k be Nat;

      cluster ( Shift (p,k)) -> finite;

      coherence

      proof

        deffunc F( Nat) = ($1 + k);

        

         A1: ( dom p) is finite;

        

         A2: { F(w) where w be Element of NAT : w in ( dom p) } is finite from FRAENKEL:sch 21( A1);

        ( dom ( Shift (p,k))) c= { F(w) where w be Element of NAT : w in ( dom p) }

        proof

          let e be object;

          assume e in ( dom ( Shift (p,k)));

          then e in { F(i) where i be Nat : i in ( dom p) } by Def12;

          then

          consider i be Nat such that

           A3: e = F(i) & i in ( dom p);

          reconsider i as Element of NAT by ORDINAL1:def 12;

          e = F(i) & i in ( dom p) by A3;

          hence e in { F(w) where w be Element of NAT : w in ( dom p) };

        end;

        hence thesis by A2, FINSET_1: 10;

      end;

    end

    reserve e1,e2 for ExtReal;

    definition

      let X be non empty ext-real-membered set, s be sequence of X;

      :: original: increasing

      redefine

      :: VALUED_1:def13

      attr s is increasing means for n be Nat holds (s . n) < (s . (n + 1));

      compatibility

      proof

        thus s is increasing implies for n be Nat holds (s . n) < (s . (n + 1))

        proof

          assume

           A1: s is increasing;

          let n be Nat;

          

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

          ( dom s) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

          hence thesis by A1, A2;

        end;

        assume

         A3: for n be Nat holds (s . n) < (s . (n + 1));

        let e1, e2;

        assume e1 in ( dom s) & e2 in ( dom s);

        then

        reconsider m = e1, n = e2 as Nat;

        defpred P[ Nat] means m < $1 implies (s . m) < (s . $1);

        

         A4: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat such that

           A5: P[j];

          assume m < (j + 1);

          then m <= j by NAT_1: 13;

          then (s . m) < (s . j) or m = j by A5, XXREAL_0: 1;

          hence thesis by A3, XXREAL_0: 2;

        end;

        assume

         A6: e1 < e2;

        

         A7: P[ 0 ];

        for j be Nat holds P[j] from NAT_1:sch 2( A7, A4);

        then (s . m) < (s . n) by A6;

        hence thesis;

      end;

      :: original: decreasing

      redefine

      :: VALUED_1:def14

      attr s is decreasing means for n be Nat holds (s . n) > (s . (n + 1));

      compatibility

      proof

        thus s is decreasing implies for n be Nat holds (s . n) > (s . (n + 1))

        proof

          assume

           A8: s is decreasing;

          let n be Nat;

          

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

          ( dom s) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

          hence thesis by A8, A9;

        end;

        assume

         A10: for n be Nat holds (s . n) > (s . (n + 1));

        let e1, e2;

        assume e1 in ( dom s) & e2 in ( dom s);

        then

        reconsider m = e1, n = e2 as Nat;

        defpred P[ Nat] means m < $1 implies (s . m) > (s . $1);

        

         A11: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat such that

           A12: P[j];

          assume m < (j + 1);

          then m <= j by NAT_1: 13;

          then (s . m) > (s . j) or m = j by A12, XXREAL_0: 1;

          hence thesis by A10, XXREAL_0: 2;

        end;

        assume

         A13: e1 < e2;

        

         A14: P[ 0 ];

        for j be Nat holds P[j] from NAT_1:sch 2( A14, A11);

        then (s . m) > (s . n) by A13;

        hence thesis;

      end;

      :: original: non-decreasing

      redefine

      :: VALUED_1:def15

      attr s is non-decreasing means for n be Nat holds (s . n) <= (s . (n + 1));

      compatibility

      proof

        thus s is non-decreasing implies for n be Nat holds (s . n) <= (s . (n + 1))

        proof

          assume

           A15: s is non-decreasing;

          let n be Nat;

          

           A16: n < (n + 1) by NAT_1: 13;

          ( dom s) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

          hence thesis by A15, A16;

        end;

        assume

         A17: for n be Nat holds (s . n) <= (s . (n + 1));

        let e1, e2;

        assume e1 in ( dom s) & e2 in ( dom s);

        then

        reconsider m = e1, n = e2 as Nat;

        defpred P[ Nat] means m <= $1 implies (s . m) <= (s . $1);

        

         A18: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat such that

           A19: P[j];

          assume m <= (j + 1);

          then

           A20: m < (j + 1) or m = (j + 1) by XXREAL_0: 1;

          (s . j) <= (s . (j + 1)) by A17;

          hence thesis by A19, A20, NAT_1: 13, XXREAL_0: 2;

        end;

        assume

         A21: e1 <= e2;

        

         A22: P[ 0 ];

        for j be Nat holds P[j] from NAT_1:sch 2( A22, A18);

        then (s . m) <= (s . n) by A21;

        hence thesis;

      end;

      :: original: non-increasing

      redefine

      :: VALUED_1:def16

      attr s is non-increasing means for n be Nat holds (s . n) >= (s . (n + 1));

      compatibility

      proof

        thus s is non-increasing implies for n be Nat holds (s . n) >= (s . (n + 1))

        proof

          assume

           A23: s is non-increasing;

          let n be Nat;

          

           A24: n < (n + 1) by NAT_1: 13;

          ( dom s) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

          hence thesis by A23, A24;

        end;

        assume

         A25: for n be Nat holds (s . n) >= (s . (n + 1));

        let e1, e2;

        assume e1 in ( dom s) & e2 in ( dom s);

        then

        reconsider m = e1, n = e2 as Nat;

        defpred P[ Nat] means m <= $1 implies (s . m) >= (s . $1);

        

         A26: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat such that

           A27: P[j];

          assume m <= (j + 1);

          then

           A28: m < (j + 1) or m = (j + 1) by XXREAL_0: 1;

          (s . j) >= (s . (j + 1)) by A25;

          hence thesis by A27, A28, NAT_1: 13, XXREAL_0: 2;

        end;

        assume

         A29: e1 <= e2;

        

         A30: P[ 0 ];

        for j be Nat holds P[j] from NAT_1:sch 2( A30, A26);

        then (s . m) >= (s . n) by A29;

        hence thesis;

      end;

    end

    scheme :: VALUED_1:sch1

    SubSeqChoice { X() -> non empty set , S() -> sequence of X() , P[ set] } :

ex S1 be subsequence of S() st for n be Element of NAT holds P[(S1 . n)]

      provided

       A1: for n be Element of NAT holds ex m be Element of NAT st n <= m & P[(S() . m)];

      defpred P1[ set, set, set] means $3 in NAT & (for m,k be Element of NAT st m = $2 & k = $3 holds m < k & P[(S() . k)]);

      consider n0 be Element of NAT such that 0 <= n0 and

       A2: P[(S() . n0)] by A1;

      

       A3: for n be Nat holds for x be set holds ex y be set st P1[n, x, y]

      proof

        let n be Nat, x be set;

        per cases ;

          suppose x in NAT ;

          then

          reconsider mx = x as Element of NAT ;

          consider my be Element of NAT such that

           A4: (mx + 1) <= my & P[(S() . my)] by A1;

          take my;

          thus my in NAT ;

          thus thesis by A4, NAT_1: 13;

        end;

          suppose

           A5: not x in NAT ;

          take 0 ;

          set y = 0 ;

          thus y in NAT ;

          let m,k be Element of NAT ;

          assume that

           A6: m = x and k = y;

          thus thesis by A5, A6;

        end;

      end;

      consider g be Function such that

       A7: ( dom g) = NAT and

       A8: (g . 0 ) = n0 and

       A9: for n be Nat holds P1[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A3);

      ( rng g) c= NAT

      proof

        defpred P[ Nat] means (g . $1) in NAT ;

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A10: x in ( dom g) and

         A11: (g . x) = y by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A7, A10;

        

         A12: for k be Nat holds P[k] implies P[(k + 1)] by A9;

        

         A13: P[ 0 ] by A8;

        for k be Nat holds P[k] from NAT_1:sch 2( A13, A12);

        then (g . n) in NAT ;

        hence thesis by A11;

      end;

      then

      reconsider g as sequence of NAT by A7, FUNCT_2: 2;

      g is increasing by A9;

      then

      reconsider g as increasing sequence of NAT ;

      reconsider S1 = (S() * g) as sequence of X();

      

       A14: ( dom S1) = NAT by FUNCT_2:def 1;

      reconsider S1 as subsequence of S();

      take S1;

      thus for n be Element of NAT holds P[(S1 . n)]

      proof

        let n be Element of NAT ;

        per cases ;

          suppose n = 0 ;

          hence thesis by A2, A8, A14, FUNCT_1: 12;

        end;

          suppose n <> 0 ;

          then n >= ( 0 qua Nat + 1) by NAT_1: 13;

          then

          reconsider n9 = (n - 1) as Element of NAT by INT_1: 5;

          reconsider k = (g . (n9 + 1)) as Element of NAT ;

          for m,k be Element of NAT st m = (g . n9) & k = (g . (n9 + 1)) holds P[(S() . k)] by A9;

          then P[(S() . k)];

          hence thesis by A14, FUNCT_1: 12;

        end;

      end;

    end;

    theorem :: VALUED_1:27

    for k be Nat holds for F be NAT -defined Function holds (( dom F),( dom ( Shift (F,k)))) are_equipotent

    proof

      let k be Nat;

      let F be NAT -defined Function;

      defpred P[ object, object] means ex il be Element of NAT st $1 = il & $2 = (k + il);

      

       A1: for e be object st e in ( dom F) holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in ( dom F);

        then

        reconsider e as Element of NAT ;

        take (k + e), e;

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = ( dom F) and

       A3: for x be object st x in ( dom F) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      take f;

      hereby

        let x1,x2 be object such that

         A4: x1 in ( dom f) and

         A5: x2 in ( dom f) and

         A6: (f . x1) = (f . x2);

        consider i1 be Element of NAT such that

         A7: x1 = i1 and

         A8: (f . x1) = (k + i1) by A2, A3, A4;

        consider i2 be Element of NAT such that

         A9: x2 = i2 and

         A10: (f . x2) = (k + i2) by A2, A3, A5;

        thus x1 = x2 by A7, A6, A8, A10, A9;

      end;

      thus ( dom f) = ( dom F) by A2;

      

       A11: ( dom ( Shift (F,k))) = { (m + k) where m be Nat : m in ( dom F) } by Def12;

      hereby

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A12: x in ( dom f) and

         A13: (f . x) = y by FUNCT_1:def 3;

        consider il be Element of NAT such that

         A14: x = il and

         A15: (f . x) = (k + il) by A2, A3, A12;

        thus y in ( dom ( Shift (F,k))) by A2, A11, A12, A13, A14, A15;

      end;

      let y be object;

      assume y in ( dom ( Shift (F,k)));

      then

      consider m be Nat such that

       A16: y = (m + k) and

       A17: m in ( dom F) by A11;

      consider il be Element of NAT such that

       A18: m = il and

       A19: (f . m) = (k + il) by A3, A17;

      thus thesis by A2, A16, A17, A18, A19, FUNCT_1:def 3;

    end;

    registration

      let F be NAT -defined Function;

      reduce ( Shift (F, 0 )) to F;

      reducibility

      proof

        

         A1: ( dom F) = { (m + 0 qua Nat) where m be Nat : m in ( dom F) }

        proof

          hereby

            let a be object;

            assume

             A2: a in ( dom F);

            then

            reconsider l = a as Element of NAT ;

            a = (l qua Nat + 0 qua Complex);

            hence a in { (m + 0 qua Nat) where m be Nat : m in ( dom F) } by A2;

          end;

          let a be object;

          assume a in { (m + 0 qua Complex) where m be Nat : m in ( dom F) };

          then ex m be Nat st a = (m + 0 qua Complex) & m in ( dom F);

          hence thesis;

        end;

        for m be Nat st m in ( dom F) holds (F . (m + 0 qua Complex)) = (F . m);

        hence thesis by A1, Def12;

      end;

    end

    registration

      let X be non empty set;

      let F be X -valued Function, k be Nat;

      cluster ( Shift (F,k)) -> X -valued;

      coherence

      proof

        

         A1: ( dom ( Shift (F,k))) = { (m + k) where m be Nat : m in ( dom F) } by Def12;

        thus ( rng ( Shift (F,k))) c= X

        proof

          let x be object;

          assume x in ( rng ( Shift (F,k)));

          then

          consider y be object such that

           A2: y in ( dom ( Shift (F,k))) and

           A3: x = (( Shift (F,k)) . y) by FUNCT_1:def 3;

          consider m be Nat such that

           A4: y = (m + k) and

           A5: m in ( dom F) by A2, A1;

          (( Shift (F,k)) . (m + k)) = (F . m) by A5, Def12

          .= (F /. m) by A5, PARTFUN1:def 6;

          hence x in X by A3, A4;

        end;

      end;

    end

    registration

      cluster non empty NAT -defined for Function;

      existence

      proof

        take ( id NAT );

        thus thesis;

      end;

    end

    registration

      let F be empty Function, k be Nat;

      cluster ( Shift (F,k)) -> empty;

      coherence

      proof

        

         A1: ( dom ( Shift (F,k))) = { (m + k) where m be Nat : m in ( dom F) } by Def12;

        assume ( Shift (F,k)) is non empty;

        then

        reconsider f = ( Shift (F,k)) as non empty Function;

        ( dom f) is non empty;

        then

        consider a be object such that

         A2: a in ( dom ( Shift (F,k)));

        ex m be Nat st a = (m + k) & m in ( dom F) by A1, A2;

        hence thesis;

      end;

    end

    registration

      let F be non empty NAT -defined Function, k be Nat;

      cluster ( Shift (F,k)) -> non empty;

      coherence

      proof

        

         A1: ( dom ( Shift (F,k))) = { (m + k) where m be Nat : m in ( dom F) } by Def12;

        consider a be object such that

         A2: a in ( dom F) by XBOOLE_0:def 1;

        reconsider a as Element of NAT by A2;

        consider m be Nat such that

         A3: a = m;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        (m + k) in ( dom ( Shift (F,k))) by A1, A2, A3;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: VALUED_1:29

    for F be Function, k be Nat st k > 0 holds not 0 in ( dom ( Shift (F,k)))

    proof

      let F be Function, k be Nat such that

       A1: k > 0 and

       A2: 0 in ( dom ( Shift (F,k)));

      ( dom ( Shift (F,k))) = { (m + k) where m be Nat : m in ( dom F) } by Def12;

      then ex m be Nat st 0 = (m + k) & m in ( dom F) by A2;

      hence contradiction by A1;

    end;

    registration

      cluster NAT -defined finite non empty for Function;

      existence

      proof

        take f = ( 0 .--> 0 );

        thus ( dom f) c= NAT by ZFMISC_1: 31;

        thus thesis;

      end;

    end

    registration

      let F be NAT -defined Relation;

      cluster ( dom F) -> natural-membered;

      coherence ;

    end

    definition

      let F be non empty NAT -defined finite Function;

      :: VALUED_1:def17

      func LastLoc F -> Element of NAT equals ( max ( dom F));

      coherence by ORDINAL1:def 12;

    end

    definition

      let F be non empty NAT -defined finite Function;

      :: VALUED_1:def18

      func CutLastLoc F -> Function equals (F \ (( LastLoc F) .--> (F . ( LastLoc F))));

      coherence ;

    end

    registration

      let F be non empty NAT -defined finite Function;

      cluster ( CutLastLoc F) -> NAT -defined finite;

      coherence ;

    end

    theorem :: VALUED_1:30

    for F be non empty NAT -defined finite Function holds ( LastLoc F) in ( dom F) by XXREAL_2:def 8;

    theorem :: VALUED_1:31

    for F,G be non empty NAT -defined finite Function st F c= G holds ( LastLoc F) <= ( LastLoc G) by RELAT_1: 11, XXREAL_2: 59;

    theorem :: VALUED_1:32

    for F be non empty NAT -defined finite Function, l be Element of NAT st l in ( dom F) holds l <= ( LastLoc F) by XXREAL_2:def 8;

    definition

      let F be non empty NAT -defined Function;

      :: VALUED_1:def19

      func FirstLoc F -> Element of NAT equals ( min ( dom F));

      coherence by ORDINAL1:def 12;

    end

    theorem :: VALUED_1:33

    for F be non empty NAT -defined finite Function holds ( FirstLoc F) in ( dom F) by XXREAL_2:def 7;

    theorem :: VALUED_1:34

    for F,G be non empty NAT -defined finite Function st F c= G holds ( FirstLoc G) <= ( FirstLoc F) by RELAT_1: 11, XXREAL_2: 60;

    theorem :: VALUED_1:35

    for l1 be Element of NAT holds for F be non empty NAT -defined finite Function st l1 in ( dom F) holds ( FirstLoc F) <= l1 by XXREAL_2:def 7;

    theorem :: VALUED_1:36

    

     Th35: for F be non empty NAT -defined finite Function holds ( dom ( CutLastLoc F)) = (( dom F) \ {( LastLoc F)})

    proof

      let F be non empty NAT -defined finite Function;

      

       A1: ( dom (( LastLoc F) .--> (F . ( LastLoc F)))) = {( LastLoc F)};

      reconsider R = { [( LastLoc F), (F . ( LastLoc F))]} as Relation;

      

       A2: R = (( LastLoc F) .--> (F . ( LastLoc F))) by FUNCT_4: 82;

      then

       A3: ( dom R) = {( LastLoc F)};

      thus ( dom ( CutLastLoc F)) c= (( dom F) \ {( LastLoc F)})

      proof

        let x be object;

        assume x in ( dom ( CutLastLoc F));

        then

        consider y be object such that

         A4: [x, y] in (F \ R) by A2, XTUPLE_0:def 12;

        

         A5: not [x, y] in R by A4, XBOOLE_0:def 5;

        

         A6: x in ( dom F) by A4, XTUPLE_0:def 12;

        per cases by A5, TARSKI:def 1;

          suppose x <> ( LastLoc F);

          then not x in ( dom R) by A3, TARSKI:def 1;

          hence thesis by A2, A6, XBOOLE_0:def 5;

        end;

          suppose

           A7: y <> (F . ( LastLoc F));

          now

            assume x in ( dom R);

            then x = ( LastLoc F) by A3, TARSKI:def 1;

            hence contradiction by A4, A7, FUNCT_1: 1;

          end;

          hence thesis by A2, A6, XBOOLE_0:def 5;

        end;

      end;

      thus thesis by A1, XTUPLE_0: 25;

    end;

    theorem :: VALUED_1:37

    for F be non empty NAT -defined finite Function holds ( dom F) = (( dom ( CutLastLoc F)) \/ {( LastLoc F)})

    proof

      let F be non empty NAT -defined finite Function;

      ( LastLoc F) in ( dom F) by XXREAL_2:def 8;

      then

       A1: {( LastLoc F)} c= ( dom F) by ZFMISC_1: 31;

      ( dom ( CutLastLoc F)) = (( dom F) \ {( LastLoc F)}) by Th35;

      hence thesis by A1, XBOOLE_1: 45;

    end;

    registration

      cluster 1 -element NAT -defined finite for Function;

      existence

      proof

        take ( 0 .--> 0 );

        thus thesis;

      end;

    end

    registration

      let F be 1 -element NAT -defined finite Function;

      cluster ( CutLastLoc F) -> empty;

      coherence

      proof

        ( LastLoc F) in ( dom F) by XXREAL_2:def 8;

        then

         A1: [( LastLoc F), (F . ( LastLoc F))] in F by FUNCT_1:def 2;

        assume not thesis;

        then

        consider a be object such that

         A2: a in ( CutLastLoc F);

        

         A3: a = [( LastLoc F), (F . ( LastLoc F))] by A1, A2, ZFMISC_1:def 10;

         not a in (( LastLoc F) .--> (F . ( LastLoc F))) by A2, XBOOLE_0:def 5;

        then not a in { [( LastLoc F), (F . ( LastLoc F))]} by FUNCT_4: 82;

        hence thesis by A3, TARSKI:def 1;

      end;

    end

    theorem :: VALUED_1:38

    

     Th37: for F be non empty NAT -defined finite Function holds ( card ( CutLastLoc F)) = (( card F) - 1)

    proof

      let F be non empty NAT -defined finite Function;

      (( LastLoc F) .--> (F . ( LastLoc F))) c= F

      proof

        let a,b be object;

        assume [a, b] in (( LastLoc F) .--> (F . ( LastLoc F)));

        then [a, b] in { [( LastLoc F), (F . ( LastLoc F))]} by FUNCT_4: 82;

        then

         A1: [a, b] = [( LastLoc F), (F . ( LastLoc F))] by TARSKI:def 1;

        ( LastLoc F) in ( dom F) by XXREAL_2:def 8;

        hence thesis by A1, FUNCT_1:def 2;

      end;

      

      hence ( card ( CutLastLoc F)) = (( card F) - ( card (( LastLoc F) .--> (F . ( LastLoc F))))) by CARD_2: 44

      .= (( card F) - ( card { [( LastLoc F), (F . ( LastLoc F))]})) by FUNCT_4: 82

      .= (( card F) - 1) by CARD_1: 30;

    end;

    begin

    registration

      let X be set, f be X -defined complex-valued Function;

      cluster ( - f) -> X -defined;

      coherence

      proof

        

         A1: ( dom ( - f)) = ( dom f) by Def5;

        thus ( dom ( - f)) c= X by A1;

      end;

      cluster (f " ) -> X -defined;

      coherence

      proof

        

         A2: ( dom (f " )) = ( dom f) by Def7;

        thus ( dom (f " )) c= X by A2;

      end;

      cluster (f ^2 ) -> X -defined;

      coherence

      proof

        

         A3: ( dom (f ^2 )) = ( dom f) by Th11;

        thus ( dom (f ^2 )) c= X by A3;

      end;

      cluster |.f.| -> X -defined;

      coherence

      proof

        

         A4: ( dom |.f.|) = ( dom f) by Def11;

        thus ( dom |.f.|) c= X by A4;

      end;

    end

    registration

      let X be set;

      cluster total for X -defined natural-valued Function;

      existence

      proof

        take the total PartFunc of X, NAT ;

        thus thesis;

      end;

    end

    registration

      let X be set, f be totalX -defined complex-valued Function;

      cluster ( - f) -> total;

      coherence

      proof

        

         A1: ( dom ( - f)) = ( dom f) by Def5;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A1, PARTFUN1:def 2;

      end;

      cluster (f " ) -> total;

      coherence

      proof

        

         A2: ( dom (f " )) = ( dom f) by Def7;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A2, PARTFUN1:def 2;

      end;

      cluster (f ^2 ) -> total;

      coherence

      proof

        

         A3: ( dom (f ^2 )) = ( dom f) by Th11;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A3, PARTFUN1:def 2;

      end;

      cluster |.f.| -> total;

      coherence

      proof

        

         A4: ( dom |.f.|) = ( dom f) by Def11;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A4, PARTFUN1:def 2;

      end;

    end

    registration

      let X be set, f be X -defined complex-valued Function, r be Complex;

      cluster (r + f) -> X -defined;

      coherence

      proof

        

         A1: ( dom (r + f)) = ( dom f) by Def2;

        thus ( dom (r + f)) c= X by A1;

      end;

      cluster (f - r) -> X -defined;

      coherence ;

      cluster (r (#) f) -> X -defined;

      coherence

      proof

        

         A2: ( dom (r (#) f)) = ( dom f) by Def5;

        thus ( dom (r (#) f)) c= X by A2;

      end;

    end

    registration

      let X be set, f be totalX -defined complex-valued Function, r be Complex;

      cluster (r + f) -> total;

      coherence

      proof

        

         A1: ( dom (r + f)) = ( dom f) by Def2;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A1, PARTFUN1:def 2;

      end;

      cluster (f - r) -> total;

      coherence ;

      cluster (r (#) f) -> total;

      coherence

      proof

        

         A2: ( dom (r (#) f)) = ( dom f) by Def5;

        ( dom f) = X by PARTFUN1:def 2;

        hence thesis by A2, PARTFUN1:def 2;

      end;

    end

    registration

      let X be set, f1 be complex-valued Function;

      let f2 be X -defined complex-valued Function;

      cluster (f1 + f2) -> X -defined;

      coherence

      proof

        

         A1: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by Def1;

        thus ( dom (f1 + f2)) c= X by A1;

      end;

      cluster (f1 - f2) -> X -defined;

      coherence ;

      cluster (f1 (#) f2) -> X -defined;

      coherence

      proof

        

         A2: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def4;

        thus ( dom (f1 (#) f2)) c= X by A2;

      end;

      cluster (f1 /" f2) -> X -defined;

      coherence ;

    end

    registration

      let X be set;

      let f1,f2 be totalX -defined complex-valued Function;

      cluster (f1 + f2) -> total;

      coherence

      proof

        

         A1: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by Def1;

        ( dom f1) = X & ( dom f2) = X by PARTFUN1:def 2;

        hence thesis by A1, PARTFUN1:def 2;

      end;

      cluster (f1 - f2) -> total;

      coherence ;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        

         A2: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def4;

        ( dom f1) = X & ( dom f2) = X by PARTFUN1:def 2;

        hence thesis by A2, PARTFUN1:def 2;

      end;

      cluster (f1 /" f2) -> total;

      coherence ;

    end

    registration

      let X be non empty set;

      let F be X -valued non empty NAT -defined finite Function;

      cluster ( CutLastLoc F) -> X -valued;

      coherence ;

    end

    theorem :: VALUED_1:39

    for f be Function holds for i,n be Nat st i in ( dom ( Shift (f,n))) holds ex j be Nat st j in ( dom f) & i = (j + n)

    proof

      let f be Function;

      let i,n be Nat;

      

       A1: ( dom ( Shift (f,n))) = { (m + n) where m be Nat : m in ( dom f) } by Def12;

      assume i in ( dom ( Shift (f,n)));

      then ex m be Nat st i = (m + n) & m in ( dom f) by A1;

      hence ex j be Nat st j in ( dom f) & i = (j + n);

    end;

    registration

      let p be FinSubsequence;

      let i be Nat;

      cluster ( Shift (p,i)) -> FinSubsequence-like;

      coherence

      proof

        set X = { (k + i) where k be Nat : k in ( dom p) }, f = ( Shift (p,i));

        consider K be Nat such that

         A1: ( dom p) c= ( Seg K) by FINSEQ_1:def 12;

        

         A2: ( dom f) = X by Def12;

        X c= ( Seg (i + K))

        proof

          let x be object;

          assume x in X;

          then

          consider k be Nat such that

           A3: x = (k + i) and

           A4: k in ( dom p);

          

           A5: (i + k) >= k by NAT_1: 11;

          

           A6: k >= 1 by A1, A4, FINSEQ_1: 1;

          

           A7: k <= K by A1, A4, FINSEQ_1: 1;

          (i + k) >= 1 by A5, A6, XXREAL_0: 2;

          hence thesis by A3, A7, FINSEQ_1: 1, XREAL_1: 6;

        end;

        hence f is FinSubsequence-like by A2;

      end;

    end

    reserve i for Nat,

k,k1,k2,j1 for Element of NAT ,

x,x1,x2,y for set;

    theorem :: VALUED_1:40

    

     Th39: for p be FinSequence holds ( dom ( Shift (p,i))) = { j1 where j1 be Nat : (i + 1) <= j1 & j1 <= (i + ( len p)) }

    proof

      let p be FinSequence;

      

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

      .= { k where k be Nat : 1 <= k & k <= ( len p) };

      set X = { j1 where j1 be Nat : (i + 1) <= j1 & j1 <= (i + ( len p)) };

      

       A2: ( dom ( Shift (p,i))) = { (k1 + i) where k1 be Nat : k1 in ( dom p) } by Def12;

      thus ( dom ( Shift (p,i))) c= X

      proof

        let x be object;

        assume x in ( dom ( Shift (p,i)));

        then

        consider k1 be Nat such that

         A3: x = (k1 + i) and

         A4: k1 in ( dom p) by A2;

        consider k be Nat such that

         A5: k1 = k and

         A6: 1 <= k and

         A7: k <= ( len p) by A1, A4;

        

         A8: (i + 1) <= (i + k) by A6, XREAL_1: 7;

        (i + k) <= (i + ( len p)) by A7, XREAL_1: 7;

        hence thesis by A3, A5, A8;

      end;

      let x be object;

      assume x in X;

      then

      consider j1 be Nat such that

       A9: x = j1 and

       A10: (i + 1) <= j1 and

       A11: j1 <= (i + ( len p));

      (i + 0 qua Nat) <= (i + 1) by XREAL_1: 7;

      then

      consider k2 be Nat such that

       A12: j1 = (i + k2) by A10, NAT_1: 10, XXREAL_0: 2;

      

       A13: 1 <= k2 by A10, A12, XREAL_1: 6;

      k2 <= ( len p) by A11, A12, XREAL_1: 6;

      then k2 in ( dom p) by A1, A13;

      hence thesis by A2, A9, A12;

    end;

    theorem :: VALUED_1:41

    

     Th40: for q be FinSubsequence holds ex ss be FinSubsequence st ( dom ss) = ( dom q) & ( rng ss) = ( dom ( Shift (q,i))) & (for k st k in ( dom q) holds (ss . k) = (i + k)) & ss is one-to-one

    proof

      let q be FinSubsequence;

      consider n be Nat such that

       A1: ( dom q) c= ( Seg n) by FINSEQ_1:def 12;

      defpred P[ object, object] means ex k st k = $1 & $2 = (i + k);

      

       A2: for x be object st x in ( dom q) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( dom q);

        then

        reconsider x as Element of NAT ;

        take (i + x);

        thus thesis;

      end;

      consider f be Function such that

       A3: ( dom f) = ( dom q) and

       A4: for x be object st x in ( dom q) holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      reconsider ss = f as FinSubsequence by A1, A3, FINSEQ_1:def 12;

      

       A5: ( dom ( Shift (q,i))) = { (k + i) where k be Nat : k in ( dom q) } by Def12;

      

       A6: ( rng ss) = ( dom ( Shift (q,i)))

      proof

        thus ( rng ss) c= ( dom ( Shift (q,i)))

        proof

          let y be object;

          assume y in ( rng ss);

          then

          consider x be object such that

           A7: x in ( dom ss) and

           A8: y = (ss . x) by FUNCT_1:def 3;

          ex k1 st (k1 = x) & ((ss . x) = (i + k1)) by A3, A4, A7;

          hence thesis by A3, A5, A7, A8;

        end;

        let y be object;

        assume y in ( dom ( Shift (q,i)));

        then

        consider k2 be Nat such that

         A9: y = (k2 + i) and

         A10: k2 in ( dom q) by A5;

        ex k3 be Element of NAT st (k3 = k2) & ((ss . k2) = (i + k3)) by A4, A10;

        hence thesis by A3, A9, A10, FUNCT_1:def 3;

      end;

      

       A11: for k st k in ( dom q) holds (ss . k) = (i + k)

      proof

        let k;

        assume k in ( dom q);

        then ex k1 st (k1 = k) & ((ss . k) = (i + k1)) by A4;

        hence thesis;

      end;

      for x1,x2 be object st x1 in ( dom ss) & x2 in ( dom ss) & (ss . x1) = (ss . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A12: x1 in ( dom ss) and

         A13: x2 in ( dom ss) and

         A14: (ss . x1) = (ss . x2);

        

         A15: ex k1 st (k1 = x1) & ((ss . x1) = (i + k1)) by A3, A4, A12;

        ex k2 st (k2 = x2) & ((ss . x2) = (i + k2)) by A3, A4, A13;

        hence thesis by A14, A15;

      end;

      then ss is one-to-one;

      hence thesis by A3, A6, A11;

    end;

    

     Lm5: for p be FinSequence holds ex fs be FinSequence st ( dom fs) = ( dom p) & ( rng fs) = ( dom ( Shift (p,i))) & (for k st k in ( dom p) holds (fs . k) = (i + k)) & fs is one-to-one

    proof

      let p be FinSequence;

      consider ss be FinSubsequence such that

       A1: ( dom ss) = ( dom p) and

       A2: ( rng ss) = ( dom ( Shift (p,i))) and

       A3: for k st k in ( dom p) holds (ss . k) = (i + k) and

       A4: ss is one-to-one by Th40;

      ( dom ss) = ( Seg ( len p)) by A1, FINSEQ_1:def 3;

      then

      reconsider fs = ss as FinSequence by FINSEQ_1:def 2;

      ( dom fs) = ( dom p) by A1;

      hence thesis by A2, A3, A4;

    end;

    theorem :: VALUED_1:42

    

     Th41: for q be FinSubsequence holds ( card q) = ( card ( Shift (q,i)))

    proof

      let q be FinSubsequence;

      ex ss be FinSubsequence st (( dom ss) = ( dom q)) & (( rng ss) = ( dom ( Shift (q,i)))) & (for k st k in ( dom q) holds (ss . k) = (i + k)) & (ss is one-to-one) by Th40;

      then

       A1: (( dom q),( dom ( Shift (q,i)))) are_equipotent ;

      

       A2: ( card ( dom q)) = ( card q) by CARD_1: 62;

      ( card ( dom ( Shift (q,i)))) = ( card ( Shift (q,i))) by CARD_1: 62;

      hence thesis by A1, A2, CARD_1: 5;

    end;

    theorem :: VALUED_1:43

    

     Th42: for p be FinSequence holds ( dom p) = ( dom ( Seq ( Shift (p,i))))

    proof

      let p be FinSequence;

      

       A1: ( rng ( Sgm ( dom ( Shift (p,i))))) = ( dom ( Shift (p,i))) by FINSEQ_1: 50;

      

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

      

       A3: ( dom ( Sgm ( dom ( Shift (p,i))))) = ( Seg ( len ( Sgm ( dom ( Shift (p,i)))))) by FINSEQ_1:def 3;

      ex k be Nat st (( dom ( Shift (p,i))) c= ( Seg k)) by FINSEQ_1:def 12;

      then

       A4: ( len ( Sgm ( dom ( Shift (p,i))))) = ( card ( dom ( Shift (p,i)))) by FINSEQ_3: 39;

      ( card ( dom ( Shift (p,i)))) = ( card ( Shift (p,i))) by CARD_1: 62;

      then ( card ( dom ( Shift (p,i)))) = ( len p) by Th41;

      hence thesis by A1, A2, A3, A4, RELAT_1: 27;

    end;

    theorem :: VALUED_1:44

    

     Th43: for p be FinSequence st k in ( dom p) holds (( Sgm ( dom ( Shift (p,i)))) . k) = (i + k)

    proof

      let p be FinSequence;

      assume

       A1: k in ( dom p);

      consider fs be FinSequence such that

       A2: ( dom fs) = ( dom p) and

       A3: ( rng fs) = ( dom ( Shift (p,i))) and

       A4: for j st j in ( dom p) holds (fs . j) = (i + j) and fs is one-to-one by Lm5;

      

       A5: ex l be Nat st (( dom ( Shift (p,i))) c= ( Seg l)) by FINSEQ_1:def 12;

      reconsider fs as FinSequence of NAT by A3, FINSEQ_1:def 4;

      for n,m,k1,k2 be Nat st 1 <= n & n < m & m <= ( len fs) & k1 = (fs . n) & k2 = (fs . m) holds k1 < k2

      proof

        let n,m,k1,k2 be Nat;

        assume that

         A6: 1 <= n and

         A7: n < m and

         A8: m <= ( len fs) and

         A9: k1 = (fs . n) and

         A10: k2 = (fs . m);

        reconsider n, m as Element of NAT by ORDINAL1:def 12;

        

         A11: ( dom fs) = ( Seg ( len fs)) by FINSEQ_1:def 3

        .= { n1 where n1 be Nat : 1 <= n1 & n1 <= ( len fs) };

        (n + 1) <= m by A7, INT_1: 7;

        then (n + 1) <= ( len fs) by A8, XXREAL_0: 2;

        then

         A12: n <= (( len fs) - 1) by XREAL_1: 19;

        (( len fs) + 0 qua Nat) <= (( len fs) + 1) by XREAL_1: 7;

        then (( len fs) - 1) <= ( len fs) by XREAL_1: 20;

        then n <= ( len fs) by A12, XXREAL_0: 2;

        then

         A13: n in ( dom p) by A2, A6, A11;

        1 <= m by A6, A7, XXREAL_0: 2;

        then

         A14: m in ( dom p) by A2, A8, A11;

        

         A15: k1 = (i + n) by A4, A9, A13;

        k2 = (i + m) by A4, A10, A14;

        hence thesis by A7, A15, XREAL_1: 8;

      end;

      then fs = ( Sgm ( dom ( Shift (p,i)))) by A3, A5, FINSEQ_1:def 13;

      hence thesis by A1, A4;

    end;

    theorem :: VALUED_1:45

    

     Th44: for p be FinSequence st k in ( dom p) holds (( Seq ( Shift (p,i))) . k) = (p . k)

    proof

      let p be FinSequence;

      assume

       A1: k in ( dom p);

      then

       A2: k in ( dom ( Seq ( Shift (p,i)))) by Th42;

      ((( Shift (p,i)) * ( Sgm ( dom ( Shift (p,i))))) . k) = (( Shift (p,i)) . (( Sgm ( dom ( Shift (p,i)))) . k)) by A2, FUNCT_1: 12

      .= (( Shift (p,i)) . (i + k)) by A1, Th43;

      hence thesis by A1, Def12;

    end;

    theorem :: VALUED_1:46

    for p be FinSequence holds ( Seq ( Shift (p,i))) = p

    proof

      let p be FinSequence;

      

       A1: ( dom ( Seq ( Shift (p,i)))) = ( dom p) by Th42;

      for x be object holds x in ( dom p) implies (( Seq ( Shift (p,i))) . x) = (p . x) by Th44;

      hence thesis by A1;

    end;

    reserve p1,p2 for FinSequence;

    

     Lm6: for j,k,l be Nat st 1 <= j & j <= l or (l + 1) <= j & j <= (l + k) holds 1 <= j & j <= (l + k)

    proof

      let j,k,l be Nat;

      assume that

       A1: 1 <= j & j <= l or (l + 1) <= j & j <= (l + k);

      per cases by A1;

        suppose

         A2: 1 <= j & j <= l;

        (l + 0 qua Nat) <= (l + k) by XREAL_1: 7;

        hence thesis by A2, XXREAL_0: 2;

      end;

        suppose

         A3: (l + 1) <= j & j <= (l + k);

        ( 0 qua Nat + 1) <= (l + 1) by XREAL_1: 7;

        hence thesis by A3, XXREAL_0: 2;

      end;

    end;

    theorem :: VALUED_1:47

    

     Th46: ( dom (p1 \/ ( Shift (p2,( len p1))))) = ( Seg (( len p1) + ( len p2)))

    proof

      

       A1: ( dom (p1 \/ ( Shift (p2,( len p1))))) = (( dom p1) \/ ( dom ( Shift (p2,( len p1))))) by XTUPLE_0: 23;

      

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

      .= { k where k be Nat : 1 <= k & k <= ( len p1) };

      

       A3: ( dom ( Shift (p2,( len p1)))) = { k1 where k1 be Nat : (( len p1) + 1) <= k1 & k1 <= (( len p1) + ( len p2)) } by Th39;

      thus ( dom (p1 \/ ( Shift (p2,( len p1))))) c= ( Seg (( len p1) + ( len p2)))

      proof

        let x be object;

        assume x in ( dom (p1 \/ ( Shift (p2,( len p1)))));

        then

         A4: x in ( dom p1) or x in ( dom ( Shift (p2,( len p1)))) by A1, XBOOLE_0:def 3;

        then

         A5: ex k3 be Nat st x = k3 & 1 <= k3 & k3 <= ( len p1) or x = k3 & (( len p1) + 1) <= k3 & k3 <= (( len p1) + ( len p2)) by A2, A3;

        reconsider x as Nat by A4;

        

         A6: 1 <= x by A5, Lm6;

        x <= (( len p1) + ( len p2)) by A5, Lm6;

        hence thesis by A6;

      end;

      let x be object;

      assume x in ( Seg (( len p1) + ( len p2)));

      then

      consider j be Nat such that

       A7: x = j and

       A8: 1 <= j and

       A9: j <= (( len p1) + ( len p2));

      reconsider i0 = ( len p1) as Integer;

      1 <= j & j <= i0 or (i0 + 1) <= j & j <= (i0 + ( len p2)) by A8, A9, INT_1: 7;

      then x in ( dom p1) or x in ( dom ( Shift (p2,( len p1)))) by A2, A3, A7;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: VALUED_1:48

    

     Th47: for p1 be FinSequence, p2 be FinSubsequence st ( len p1) <= i holds ( dom p1) misses ( dom ( Shift (p2,i)))

    proof

      let p1 be FinSequence, p2 be FinSubsequence;

      assume

       A1: ( len p1) <= i;

      

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

      .= { k where k be Nat : 1 <= k & k <= ( len p1) };

      

       A3: ( dom ( Shift (p2,i))) = { (k + i) where k be Nat : k in ( dom p2) } by Def12;

       not ex x be object st x in (( dom p1) /\ ( dom ( Shift (p2,i))))

      proof

        given x be object such that

         A4: x in (( dom p1) /\ ( dom ( Shift (p2,i))));

        

         A5: x in ( dom p1) by A4, XBOOLE_0:def 4;

        

         A6: x in ( dom ( Shift (p2,i))) by A4, XBOOLE_0:def 4;

        

         A7: ex k1 be Nat st (x = k1) & (1 <= k1) & (k1 <= ( len p1)) by A2, A5;

        consider k2 be Nat such that

         A8: x = (k2 + i) and

         A9: k2 in ( dom p2) by A3, A6;

        consider n be Nat such that

         A10: ( dom p2) c= ( Seg n) by FINSEQ_1:def 12;

        

         A11: k2 in ( Seg n) by A9, A10;

        

         A12: ex m be Nat st k2 = m & 1 <= m & m <= n by A11;

        reconsider x as Element of NAT by A4;

        (( len p1) + k2) <= (i + k2) by A1, XREAL_1: 7;

        then ((( len p1) + k2) - k2) < (x - 0 ) by A8, A12, XREAL_1: 15;

        hence contradiction by A7;

      end;

      hence (( dom p1) /\ ( dom ( Shift (p2,i)))) = {} by XBOOLE_0:def 1;

    end;

    theorem :: VALUED_1:49

    for p1,p2 be FinSequence holds (p1 ^ p2) = (p1 \/ ( Shift (p2,( len p1))))

    proof

      let p1, p2;

      

       A1: ( dom (p1 \/ ( Shift (p2,( len p1))))) = ( Seg (( len p1) + ( len p2))) by Th46;

      ( dom p1) misses ( dom ( Shift (p2,( len p1)))) by Th47;

      then

      reconsider p = (p1 \/ ( Shift (p2,( len p1)))) as FinSequence by A1, FINSEQ_1:def 2, GRFUNC_1: 13;

      

       A2: ( dom p) = ( Seg (( len p1) + ( len p2))) by Th46;

      

       A3: for k be Nat st k in ( dom p1) holds (p . k) = (p1 . k)

      proof

        let k be Nat;

        assume k in ( dom p1);

        then [k, (p1 . k)] in p1 by FUNCT_1:def 2;

        then [k, (p1 . k)] in p by XBOOLE_0:def 3;

        hence thesis by FUNCT_1: 1;

      end;

      for k be Nat st k in ( dom p2) holds (p . (( len p1) + k)) = (p2 . k)

      proof

        let k be Nat;

        assume

         A4: k in ( dom p2);

        ( dom ( Shift (p2,( len p1)))) = { (j + ( len p1)) where j be Nat : j in ( dom p2) } by Def12;

        then (( len p1) + k) in ( dom ( Shift (p2,( len p1)))) by A4;

        then [(( len p1) + k), (( Shift (p2,( len p1))) . (( len p1) + k))] in ( Shift (p2,( len p1))) by FUNCT_1:def 2;

        then [(( len p1) + k), (( Shift (p2,( len p1))) . (( len p1) + k))] in p by XBOOLE_0:def 3;

        then (p . (( len p1) + k)) = (( Shift (p2,( len p1))) . (( len p1) + k)) by FUNCT_1: 1;

        hence thesis by A4, Def12;

      end;

      hence thesis by A2, A3, FINSEQ_1:def 7;

    end;

    theorem :: VALUED_1:50

    for p1 be FinSequence, p2 be FinSubsequence st i >= ( len p1) holds p1 misses ( Shift (p2,i))

    proof

      let p1 be FinSequence, p2 be FinSubsequence;

      assume i >= ( len p1);

      then ( dom p1) misses ( dom ( Shift (p2,i))) by Th47;

      hence thesis by RELAT_1: 179;

    end;

    theorem :: VALUED_1:51

    for F be total NAT -defined Function, p be NAT -defined Function, n be Element of NAT st ( Shift (p,n)) c= F holds for i be Element of NAT st i in ( dom p) holds (F . (n + i)) = (p . i)

    proof

      let F be total NAT -defined Function, p be NAT -defined Function, n be Element of NAT such that

       A1: ( Shift (p,n)) c= F;

      let i be Element of NAT ;

      assume

       A2: i in ( dom p);

      then (n + i) in ( dom ( Shift (p,n))) by Th24;

      

      hence (F . (n + i)) = (( Shift (p,n)) . (n + i)) by A1, GRFUNC_1: 2

      .= (p . i) by A2, Def12;

    end;

    theorem :: VALUED_1:52

    

     Th51: for p,q be FinSubsequence st q c= p holds ( Shift (q,i)) c= ( Shift (p,i))

    proof

      let p,q be FinSubsequence;

      assume

       A1: q c= p;

      

       A2: ( dom ( Shift (q,i))) = { (k + i) where k be Nat : k in ( dom q) } by Def12;

      

       A3: ( dom ( Shift (p,i))) = { (k + i) where k be Nat : k in ( dom p) } by Def12;

      let x,y be object;

      assume

       A4: [x, y] in ( Shift (q,i));

      then

       A5: x in ( dom ( Shift (q,i))) by FUNCT_1: 1;

      

       A6: y = (( Shift (q,i)) . x) by A4, FUNCT_1: 1;

      consider k be Nat such that

       A7: x = (k + i) and

       A8: k in ( dom q) by A2, A5;

      

       A9: ( dom q) c= ( dom p) by A1, GRFUNC_1: 2;

      then

       A10: x in ( dom ( Shift (p,i))) by A3, A7, A8;

      y = (q . k) by A6, A7, A8, Def12

      .= (p . k) by A1, A8, GRFUNC_1: 2

      .= (( Shift (p,i)) . x) by A7, A8, A9, Def12;

      hence thesis by A10, FUNCT_1: 1;

    end;

    theorem :: VALUED_1:53

    for p1,p2 be FinSequence holds ( Shift (p2,( len p1))) c= (p1 ^ p2)

    proof

      let p1,p2 be FinSequence;

      

       A1: ( dom ( Shift (p2,( len p1)))) = { (k + ( len p1)) where k be Nat : k in ( dom p2) } by Def12;

      

       A2: ( dom ( Shift (p2,( len p1)))) = { k where k be Nat : (( len p1) + 1) <= k & k <= (( len p1) + ( len p2)) } by Th39;

      

       A3: ( dom (p1 ^ p2)) = ( Seg (( len p1) + ( len p2))) by FINSEQ_1:def 7

      .= { k where k be Nat : 1 <= k & k <= (( len p1) + ( len p2)) };

      let x,y be object;

      assume

       A4: [x, y] in ( Shift (p2,( len p1)));

      then

       A5: x in ( dom ( Shift (p2,( len p1)))) by FUNCT_1: 1;

      

       A6: y = (( Shift (p2,( len p1))) . x) by A4, FUNCT_1: 1;

      consider k be Nat such that

       A7: x = k and

       A8: (( len p1) + 1) <= k and

       A9: k <= (( len p1) + ( len p2)) by A2, A5;

      1 <= (( len p1) + 1) by INT_1: 6;

      then 1 <= k by A8, XXREAL_0: 2;

      then

       A10: x in ( dom (p1 ^ p2)) by A3, A7, A9;

      consider j be Nat such that

       A11: x = (j + ( len p1)) and

       A12: j in ( dom p2) by A1, A5;

      y = (p2 . j) by A6, A11, A12, Def12

      .= ((p1 ^ p2) . x) by A11, A12, FINSEQ_1:def 7;

      hence thesis by A10, FUNCT_1: 1;

    end;

    reserve q,q1,q2,q3,q4 for FinSubsequence,

p1,p2 for FinSequence;

    theorem :: VALUED_1:54

    

     Th53: ( dom q1) misses ( dom q2) implies ( dom ( Shift (q1,i))) misses ( dom ( Shift (q2,i)))

    proof

      assume

       A1: ( dom q1) misses ( dom q2);

      

       A2: ( dom ( Shift (q1,i))) = { (k + i) where k be Nat : k in ( dom q1) } by Def12;

      

       A3: ( dom ( Shift (q2,i))) = { (k + i) where k be Nat : k in ( dom q2) } by Def12;

      now

        given x be object such that

         A4: x in (( dom ( Shift (q1,i))) /\ ( dom ( Shift (q2,i))));

        

         A5: x in ( dom ( Shift (q1,i))) by A4, XBOOLE_0:def 4;

        

         A6: x in ( dom ( Shift (q2,i))) by A4, XBOOLE_0:def 4;

        

         A7: ex k1 be Nat st (x = (k1 + i)) & (k1 in ( dom q1)) by A2, A5;

        consider k2 be Nat such that

         A8: x = (k2 + i) and

         A9: k2 in ( dom q2) by A3, A6;

        k2 in (( dom q1) /\ ( dom q2)) by A7, A8, A9, XBOOLE_0:def 4;

        hence contradiction by A1;

      end;

      hence (( dom ( Shift (q1,i))) /\ ( dom ( Shift (q2,i)))) = {} by XBOOLE_0:def 1;

    end;

    theorem :: VALUED_1:55

    for q,q1,q2 be FinSubsequence st q = (q1 \/ q2) & q1 misses q2 holds (( Shift (q1,i)) \/ ( Shift (q2,i))) = ( Shift (q,i))

    proof

      let q,q1,q2 be FinSubsequence such that

       A1: q = (q1 \/ q2) and

       A2: q1 misses q2;

      

       A3: ( dom ( Shift (q,i))) = { (k + i) where k be Nat : k in ( dom q) } by Def12;

      

       A4: ( dom ( Shift (q1,i))) = { (k + i) where k be Nat : k in ( dom q1) } by Def12;

      

       A5: ( dom ( Shift (q2,i))) = { (k + i) where k be Nat : k in ( dom q2) } by Def12;

      

       A6: q1 c= q by A1, XBOOLE_1: 7;

      

       A7: q2 c= q by A1, XBOOLE_1: 7;

      

       A8: ( Shift (q1,i)) c= ( Shift (q,i)) by A1, Th51, XBOOLE_1: 7;

      

       A9: ( Shift (q2,i)) c= ( Shift (q,i)) by A1, Th51, XBOOLE_1: 7;

      ( dom q1) misses ( dom q2) by A2, A6, A7, FUNCT_1: 112;

      then ( dom ( Shift (q1,i))) misses ( dom ( Shift (q2,i))) by Th53;

      then

      reconsider q3 = (( Shift (q1,i)) \/ ( Shift (q2,i))) as Function by GRFUNC_1: 13;

      let x,y be object;

      thus [x, y] in (( Shift (q1,i)) \/ ( Shift (q2,i))) implies [x, y] in ( Shift (q,i))

      proof

        assume

         A10: [x, y] in (( Shift (q1,i)) \/ ( Shift (q2,i)));

        then x in ( dom q3) by FUNCT_1: 1;

        then

         A11: x in (( dom ( Shift (q1,i))) \/ ( dom ( Shift (q2,i)))) by XTUPLE_0: 23;

         A12:

        now

          assume

           A13: x in ( dom ( Shift (q1,i)));

          

           A14: ( dom ( Shift (q1,i))) c= ( dom ( Shift (q,i))) by A8, GRFUNC_1: 2;

          (( Shift (q1,i)) . x) = (( Shift (q,i)) . x) by A8, A13, GRFUNC_1: 2;

          then [x, (( Shift (q,i)) . x)] in ( Shift (q1,i)) by A13, FUNCT_1:def 2;

          then [x, (( Shift (q,i)) . x)] in q3 by XBOOLE_0:def 3;

          hence x in ( dom ( Shift (q,i))) & y = (( Shift (q,i)) . x) by A10, A13, A14, FUNCT_1:def 1;

        end;

        now

          assume

           A15: x in ( dom ( Shift (q2,i)));

          

           A16: ( dom ( Shift (q2,i))) c= ( dom ( Shift (q,i))) by A9, GRFUNC_1: 2;

          (( Shift (q2,i)) . x) = (( Shift (q,i)) . x) by A9, A15, GRFUNC_1: 2;

          then [x, (( Shift (q,i)) . x)] in ( Shift (q2,i)) by A15, FUNCT_1:def 2;

          then [x, (( Shift (q,i)) . x)] in q3 by XBOOLE_0:def 3;

          hence x in ( dom ( Shift (q,i))) & y = (( Shift (q,i)) . x) by A10, A15, A16, FUNCT_1:def 1;

        end;

        hence thesis by A11, A12, FUNCT_1: 1, XBOOLE_0:def 3;

      end;

      assume

       A17: [x, y] in ( Shift (q,i));

      then

       A18: x in ( dom ( Shift (q,i))) by FUNCT_1: 1;

      

       A19: y = (( Shift (q,i)) . x) by A17, FUNCT_1: 1;

      consider k be Nat such that

       A20: x = (k + i) and

       A21: k in ( dom q) by A3, A18;

      ( dom q) = (( dom q1) \/ ( dom q2)) by A1, XTUPLE_0: 23;

      then

       A22: k in ( dom q1) or k in ( dom q2) by A21, XBOOLE_0:def 3;

      then x in ( dom ( Shift (q1,i))) or x in ( dom ( Shift (q2,i))) by A4, A5, A20;

      then x in (( dom ( Shift (q1,i))) \/ ( dom ( Shift (q2,i)))) by XBOOLE_0:def 3;

      then

       A23: x in ( dom q3) by XTUPLE_0: 23;

       A24:

      now

        assume

         A25: x in ( dom ( Shift (q1,i)));

        then

         A26: ex k1 be Nat st (x = (k1 + i)) & (k1 in ( dom q1)) by A4;

        

        thus y = (q . k) by A19, A20, A21, Def12

        .= (q1 . k) by A1, A20, A26, GRFUNC_1: 15

        .= (( Shift (q1,i)) . x) by A20, A26, Def12

        .= (q3 . x) by A25, GRFUNC_1: 15;

      end;

      now

        assume

         A27: x in ( dom ( Shift (q2,i)));

        then

         A28: ex k2 be Nat st (x = (k2 + i)) & (k2 in ( dom q2)) by A5;

        

        thus y = (q . k) by A19, A20, A21, Def12

        .= (q2 . k) by A1, A20, A28, GRFUNC_1: 15

        .= (( Shift (q2,i)) . x) by A20, A28, Def12

        .= (q3 . x) by A27, GRFUNC_1: 15;

      end;

      hence thesis by A4, A5, A20, A22, A23, A24, FUNCT_1: 1;

    end;

    theorem :: VALUED_1:56

    

     Th55: for q be FinSubsequence holds ( dom ( Seq q)) = ( dom ( Seq ( Shift (q,i))))

    proof

      let q be FinSubsequence;

      

       A1: ( len ( Seq q)) = ( card q) by FINSEQ_3: 158;

      

       A2: ( len ( Seq ( Shift (q,i)))) = ( card ( Shift (q,i))) by FINSEQ_3: 158;

      

      thus ( dom ( Seq q)) = ( Seg ( len ( Seq q))) by FINSEQ_1:def 3

      .= ( dom ( Seq ( Shift (q,i)))) by Th41, A1, A2, FINSEQ_1:def 3;

    end;

    reserve l1 for Nat,

j2 for Element of NAT ;

    theorem :: VALUED_1:57

    

     Th56: for q be FinSubsequence st k in ( dom ( Seq q)) holds ex j st j = (( Sgm ( dom q)) . k) & (( Sgm ( dom ( Shift (q,i)))) . k) = (i + j)

    proof

      let q be FinSubsequence such that

       A1: k in ( dom ( Seq q));

      consider ss be FinSubsequence such that

       A2: ( dom ss) = ( dom q) and

       A3: ( rng ss) = ( dom ( Shift (q,i))) and

       A4: for l st l in ( dom q) holds (ss . l) = (i + l) and ss is one-to-one by Th40;

      

       A5: ( rng ( Seq ss)) = ( dom ( Shift (q,i))) by A3, FINSEQ_1: 101;

      

       A6: ( rng ( Sgm ( dom q))) = ( dom q) by FINSEQ_1: 50;

      

       A7: ( dom ( Seq q)) = ( dom (q * ( Sgm ( dom q))))

      .= ( dom ( Sgm ( dom q))) by A6, RELAT_1: 27;

      

       A8: for l1 st l1 in ( dom ( Seq q)) holds ex j1 st j1 = (( Sgm ( dom q)) . l1) & (( Seq ss) . l1) = (i + j1)

      proof

        let l1 such that

         A9: l1 in ( dom ( Seq q));

        

         A10: (( Sgm ( dom q)) . l1) in ( rng ( Sgm ( dom q))) by A7, A9, FUNCT_1:def 3;

        then

         A11: (( Sgm ( dom q)) . l1) in ( dom q) by FINSEQ_1: 50;

        reconsider j1 = (( Sgm ( dom q)) . l1) as Element of NAT by A10;

        (( Seq ss) . l1) = ((ss * ( Sgm ( dom ss))) . l1)

        .= (ss . j1) by A2, A7, A9, FUNCT_1: 13

        .= (i + j1) by A4, A11;

        hence thesis;

      end;

      

       A12: ( rng ss) = ( rng ( Sgm ( dom ( Shift (q,i))))) by A3, FINSEQ_1: 50;

      ( rng ( Sgm ( dom ( Shift (q,i))))) c= NAT ;

      then ( rng ( Seq ss)) c= NAT by A12, FINSEQ_1: 101;

      then

      reconsider fs = ( Seq ss) as FinSequence of NAT by FINSEQ_1:def 4;

      

       A13: ex l2 be Nat st (( dom ( Shift (q,i))) c= ( Seg l2)) by FINSEQ_1:def 12;

      

       A14: ( dom ( Seq ss)) = ( dom (ss * ( Sgm ( dom ss))))

      .= ( dom ( Sgm ( dom q))) by A2, A6, RELAT_1: 27;

      for n,m,k1,k2 be Nat st 1 <= n & n < m & m <= ( len fs) & k1 = (fs . n) & k2 = (fs . m) holds k1 < k2

      proof

        let n,m,k1,k2 be Nat;

        assume that

         A15: 1 <= n and

         A16: n < m and

         A17: m <= ( len fs) and

         A18: k1 = (fs . n) and

         A19: k2 = (fs . m);

        reconsider n, m as Element of NAT by ORDINAL1:def 12;

        

         A20: ( dom fs) = ( Seg ( len fs)) by FINSEQ_1:def 3

        .= { l3 where l3 be Nat : 1 <= l3 & l3 <= ( len fs) };

        (n + 1) <= m by A16, INT_1: 7;

        then (n + 1) <= ( len fs) by A17, XXREAL_0: 2;

        then

         A21: n <= (( len fs) - 1) by XREAL_1: 19;

        (( len fs) + 0 qua Nat) <= (( len fs) + 1) by XREAL_1: 7;

        then (( len fs) - 1) <= ( len fs) by XREAL_1: 20;

        then n <= ( len fs) by A21, XXREAL_0: 2;

        then

         A22: n in ( dom ( Seq q)) by A7, A14, A15, A20;

        1 <= m by A15, A16, XXREAL_0: 2;

        then

         A23: m in ( dom ( Seq q)) by A7, A14, A17, A20;

        consider j2 be Element of NAT such that

         A24: j2 = (( Sgm ( dom q)) . n) and

         A25: (fs . n) = (i + j2) by A8, A22;

        consider j3 be Element of NAT such that

         A26: j3 = (( Sgm ( dom q)) . m) and

         A27: (fs . m) = (i + j3) by A8, A23;

        

         A28: ex l3 be Nat st (( dom q) c= ( Seg l3)) by FINSEQ_1:def 12;

        ( dom ( Seq ss)) = ( Seg ( len fs)) by FINSEQ_1:def 3;

        then ( len fs) = ( len ( Sgm ( dom q))) by A14, FINSEQ_1:def 3;

        then j2 < j3 by A15, A16, A17, A24, A26, A28, FINSEQ_1:def 13;

        hence thesis by A18, A19, A25, A27, XREAL_1: 8;

      end;

      then fs = ( Sgm ( dom ( Shift (q,i)))) by A5, A13, FINSEQ_1:def 13;

      hence thesis by A1, A8;

    end;

    theorem :: VALUED_1:58

    

     Th57: for q be FinSubsequence st k in ( dom ( Seq q)) holds (( Seq ( Shift (q,i))) . k) = (( Seq q) . k)

    proof

      let q be FinSubsequence;

      assume

       A1: k in ( dom ( Seq q));

      then

      consider j such that

       A2: j = (( Sgm ( dom q)) . k) and

       A3: (( Sgm ( dom ( Shift (q,i)))) . k) = (i + j) by Th56;

      

       A4: ( rng ( Sgm ( dom q))) = ( dom q) by FINSEQ_1: 50;

      

       A5: ( dom ( Seq q)) = ( dom ( Seq ( Shift (q,i)))) by Th55

      .= ( dom (( Shift (q,i)) * ( Sgm ( dom ( Shift (q,i))))));

      

       A6: ( dom ( Seq q)) = ( dom (q * ( Sgm ( dom q))))

      .= ( dom ( Sgm ( dom q))) by A4, RELAT_1: 27;

      then j in ( rng ( Sgm ( dom q))) by A1, A2, FUNCT_1:def 3;

      then

       A7: j in ( dom q) by FINSEQ_1: 50;

      (( Seq ( Shift (q,i))) . k) = ((( Shift (q,i)) * ( Sgm ( dom ( Shift (q,i))))) . k)

      .= (( Shift (q,i)) . (( Sgm ( dom ( Shift (q,i)))) . k)) by A1, A5, FUNCT_1: 12

      .= (q . j) by A3, A7, Def12

      .= ((q * ( Sgm ( dom q))) . k) by A1, A2, A6, FUNCT_1: 13

      .= (( Seq q) . k);

      hence thesis;

    end;

    theorem :: VALUED_1:59

    for q be FinSubsequence holds ( Seq q) = ( Seq ( Shift (q,i)))

    proof

      let q be FinSubsequence;

      

       A1: ( dom ( Seq q)) = ( dom ( Seq ( Shift (q,i)))) by Th55;

      for x be object holds x in ( dom ( Seq q)) implies (( Seq ( Shift (q,i))) . x) = (( Seq q) . x) by Th57;

      hence thesis by A1;

    end;

    theorem :: VALUED_1:60

    

     Th59: for q be FinSubsequence st ( dom q) c= ( Seg k) holds ( dom ( Shift (q,i))) c= ( Seg (i + k))

    proof

      let q be FinSubsequence;

      assume

       A1: ( dom q) c= ( Seg k);

      

       A2: ( dom ( Shift (q,i))) = { (j + i) where j be Nat : j in ( dom q) } by Def12;

      let x be object;

      assume x in ( dom ( Shift (q,i)));

      then

      consider j1 be Nat such that

       A3: x = (j1 + i) and

       A4: j1 in ( dom q) by A2;

      j1 in ( Seg k) by A1, A4;

      then

       A5: ex j2 be Nat st (j1 = j2) & (1 <= j2) & (j2 <= k);

      

       A6: ( 0 qua Nat + 1) <= (i + j1) by A5, XREAL_1: 7;

      (i + j1) <= (i + k) by A5, XREAL_1: 7;

      hence thesis by A3, A6;

    end;

    theorem :: VALUED_1:61

    

     Th60: for p be FinSequence, q1,q2 be FinSubsequence st q1 c= p holds ex ss be FinSubsequence st ss = (q1 \/ ( Shift (q2,( len p))))

    proof

      let p be FinSequence, q1,q2 be FinSubsequence;

      assume q1 c= p;

      then

       A1: ( dom q1) c= ( dom p) by GRFUNC_1: 2;

      ( dom p) misses ( dom ( Shift (q2,( len p)))) by Th47;

      then

      reconsider ss = (q1 \/ ( Shift (q2,( len p)))) as Function by A1, GRFUNC_1: 13, XBOOLE_1: 63;

      

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

      consider k be Nat such that

       A3: ( dom q2) c= ( Seg k) by FINSEQ_1:def 12;

      k in NAT by ORDINAL1:def 12;

      then

       A4: ( dom ( Shift (q2,( len p)))) c= ( Seg (( len p) + k)) by A3, Th59;

      (( len p) + 0 qua Nat) <= (( len p) + k) by XREAL_1: 7;

      then ( Seg ( len p)) c= ( Seg (( len p) + k)) by FINSEQ_1: 5;

      then ( dom q1) c= ( Seg (( len p) + k)) by A1, A2;

      then (( dom q1) \/ ( dom ( Shift (q2,( len p))))) c= ( Seg (( len p) + k)) by A4, XBOOLE_1: 8;

      then ( dom (q1 \/ ( Shift (q2,( len p))))) c= ( Seg (( len p) + k)) by XTUPLE_0: 23;

      then

      reconsider ss as FinSubsequence by FINSEQ_1:def 12;

      take ss;

      thus thesis;

    end;

    

     Lm7: for p,q be FinSubsequence st q c= p holds ( dom ( Shift (q,i))) c= ( dom ( Shift (p,i)))

    proof

      let p,q be FinSubsequence;

      assume

       A1: q c= p;

      

       A2: ( dom ( Shift (q,i))) = { (k + i) where k be Nat : k in ( dom q) } by Def12;

      

       A3: ( dom ( Shift (p,i))) = { (k + i) where k be Nat : k in ( dom p) } by Def12;

      

       A4: ( dom q) c= ( dom p) by A1, GRFUNC_1: 2;

      let x be object;

      assume x in ( dom ( Shift (q,i)));

      then ex k1 be Nat st (x = (k1 + i)) & (k1 in ( dom q)) by A2;

      hence thesis by A3, A4;

    end;

    

     Lm8: for p1,p2 be FinSequence, q1,q2 be FinSubsequence st q1 c= p1 & q2 c= p2 holds ( Sgm (( dom q1) \/ ( dom ( Shift (q2,( len p1)))))) = (( Sgm ( dom q1)) ^ ( Sgm ( dom ( Shift (q2,( len p1))))))

    proof

      let p1,p2 be FinSequence, q1,q2 be FinSubsequence;

      assume that

       A1: q1 c= p1 and

       A2: q2 c= p2;

      

       A3: ex k1 be Nat st (( dom q1) c= ( Seg k1)) by FINSEQ_1:def 12;

      

       A4: ex k2 be Nat st (( dom ( Shift (q2,( len p1)))) c= ( Seg k2)) by FINSEQ_1:def 12;

      for m,n be Nat st m in ( dom q1) & n in ( dom ( Shift (q2,( len p1)))) holds m < n

      proof

        let m,n be Nat such that

         A5: m in ( dom q1) and

         A6: n in ( dom ( Shift (q2,( len p1))));

        

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

        .= { k where k be Nat : 1 <= k & k <= ( len p1) };

        

         A8: ( dom ( Shift (p2,( len p1)))) = { k where k be Nat : (( len p1) + 1) <= k & k <= (( len p1) + ( len p2)) } by Th39;

        

         A9: ( dom q1) c= ( dom p1) by A1, GRFUNC_1: 2;

        

         A10: ( dom ( Shift (q2,( len p1)))) c= ( dom ( Shift (p2,( len p1)))) by A2, Lm7;

        

         A11: m in ( dom p1) by A5, A9;

        

         A12: n in ( dom ( Shift (p2,( len p1)))) by A6, A10;

        consider k3 be Nat such that

         A13: k3 = m and 1 <= k3 and

         A14: k3 <= ( len p1) by A7, A11;

        consider k4 be Nat such that

         A15: k4 = n and

         A16: (( len p1) + 1) <= k4 and k4 <= (( len p1) + ( len p2)) by A8, A12;

        ( len p1) < (( len p1) + 1) by XREAL_1: 29;

        then k3 <= (( len p1) + 1) by A14, XXREAL_0: 2;

        then

         A17: k3 <= k4 by A16, XXREAL_0: 2;

        k3 <> k4 by A5, A6, A9, A13, A15, Th47, XBOOLE_0: 3;

        hence thesis by A13, A15, A17, XXREAL_0: 1;

      end;

      hence thesis by A3, A4, FINSEQ_3: 42;

    end;

    theorem :: VALUED_1:62

    

     Th61: for p1,p2 be FinSequence, q1,q2 be FinSubsequence st q1 c= p1 & q2 c= p2 holds ex ss be FinSubsequence st ss = (q1 \/ ( Shift (q2,( len p1)))) & ( dom ( Seq ss)) = ( Seg (( len ( Seq q1)) + ( len ( Seq q2))))

    proof

      let p1,p2 be FinSequence, q1,q2 be FinSubsequence;

      assume that

       A1: q1 c= p1 and

       A2: q2 c= p2;

      consider ss be FinSubsequence such that

       A3: ss = (q1 \/ ( Shift (q2,( len p1)))) by A1, Th60;

      

       A4: ex k1 be Nat st (( dom q1) c= ( Seg k1)) by FINSEQ_1:def 12;

      

       A5: ex k2 be Nat st (( dom ( Shift (q2,( len p1)))) c= ( Seg k2)) by FINSEQ_1:def 12;

      

       A6: ( rng ( Sgm ( dom ss))) = ( dom ss) by FINSEQ_1: 50;

      

       A7: ( dom ( Seq ss)) = ( dom ( Sgm ( dom ss))) by A6, RELAT_1: 27

      .= ( dom ( Sgm (( dom q1) \/ ( dom ( Shift (q2,( len p1))))))) by A3, XTUPLE_0: 23

      .= ( dom (( Sgm ( dom q1)) ^ ( Sgm ( dom ( Shift (q2,( len p1))))))) by A1, A2, Lm8

      .= ( Seg (( len ( Sgm ( dom q1))) + ( len ( Sgm ( dom ( Shift (q2,( len p1)))))))) by FINSEQ_1:def 7;

      

       A8: ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) = ( card ( dom ( Shift (q2,( len p1))))) by A5, FINSEQ_3: 39;

      

       A9: ( len ( Sgm ( dom q1))) = ( card ( dom q1)) by A4, FINSEQ_3: 39;

      ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) = ( card ( Shift (q2,( len p1)))) by A8, CARD_1: 62;

      then

       A10: ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) = ( card q2) by Th41;

      

       A11: ( len ( Sgm ( dom q1))) = ( card q1) by A9, CARD_1: 62;

      

       A12: ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) = ( len ( Seq q2)) by A10, FINSEQ_3: 158;

      ( len ( Sgm ( dom q1))) = ( len ( Seq q1)) by A11, FINSEQ_3: 158;

      hence thesis by A3, A7, A12;

    end;

    theorem :: VALUED_1:63

    

     Th62: for p1,p2 be FinSequence, q1,q2 be FinSubsequence st q1 c= p1 & q2 c= p2 holds ex ss be FinSubsequence st ss = (q1 \/ ( Shift (q2,( len p1)))) & ( dom ( Seq ss)) = ( Seg (( len ( Seq q1)) + ( len ( Seq q2)))) & ( Seq ss) = (( Seq q1) \/ ( Shift (( Seq q2),( len ( Seq q1)))))

    proof

      let p1,p2 be FinSequence, q1,q2 be FinSubsequence;

      assume that

       A1: q1 c= p1 and

       A2: q2 c= p2;

      consider ss be FinSubsequence such that

       A3: ss = (q1 \/ ( Shift (q2,( len p1)))) and

       A4: ( dom ( Seq ss)) = ( Seg (( len ( Seq q1)) + ( len ( Seq q2)))) by A1, A2, Th61;

      

       A5: ( dom ( Seq q1)) = ( Seg ( len ( Seq q1))) by FINSEQ_1:def 3

      .= { k where k be Nat : 1 <= k & k <= ( len ( Seq q1)) };

      

       A6: ( dom ( Shift (( Seq q2),( len ( Seq q1))))) = { k where k be Nat : (( len ( Seq q1)) + 1) <= k & k <= (( len ( Seq q1)) + ( len ( Seq q2))) } by Th39;

      

       A7: ( Seg (( len ( Seq q1)) + ( len ( Seq q2)))) = (( dom ( Seq q1)) \/ ( dom ( Shift (( Seq q2),( len ( Seq q1))))))

      proof

        thus ( Seg (( len ( Seq q1)) + ( len ( Seq q2)))) c= (( dom ( Seq q1)) \/ ( dom ( Shift (( Seq q2),( len ( Seq q1))))))

        proof

          let x be object;

          assume x in ( Seg (( len ( Seq q1)) + ( len ( Seq q2))));

          then

          consider k1 be Nat such that

           A8: x = k1 and

           A9: 1 <= k1 and

           A10: k1 <= (( len ( Seq q1)) + ( len ( Seq q2)));

          

           A11: 1 <= k1 & k1 <= ( len ( Seq q1)) implies k1 in ( dom ( Seq q1)) by A5;

          (( len ( Seq q1)) + 1) <= k1 & k1 <= (( len ( Seq q1)) + ( len ( Seq q2))) implies k1 in ( dom ( Shift (( Seq q2),( len ( Seq q1))))) by A6;

          hence thesis by A8, A9, A10, A11, INT_1: 7, XBOOLE_0:def 3;

        end;

        let x be object;

        assume

         A12: x in (( dom ( Seq q1)) \/ ( dom ( Shift (( Seq q2),( len ( Seq q1))))));

         A13:

        now

          assume x in ( dom ( Seq q1));

          then

          consider k1 be Nat such that

           A14: x = k1 and

           A15: 1 <= k1 and

           A16: k1 <= ( len ( Seq q1)) by A5;

          (( len ( Seq q1)) + 0 qua Nat) <= (( len ( Seq q1)) + ( len ( Seq q2))) by XREAL_1: 7;

          then k1 <= (( len ( Seq q1)) + ( len ( Seq q2))) by A16, XXREAL_0: 2;

          hence thesis by A14, A15;

        end;

        now

          assume x in ( dom ( Shift (( Seq q2),( len ( Seq q1)))));

          then

          consider k2 be Nat such that

           A17: x = k2 and

           A18: (( len ( Seq q1)) + 1) <= k2 and

           A19: k2 <= (( len ( Seq q1)) + ( len ( Seq q2))) by A6;

          ( 0 qua Nat + 1) <= (( len ( Seq q1)) + 1) by XREAL_1: 7;

          then 1 <= k2 by A18, XXREAL_0: 2;

          hence thesis by A17, A19;

        end;

        hence thesis by A12, A13, XBOOLE_0:def 3;

      end;

      

       A20: (( dom ( Seq q1)) \/ ( dom ( Shift (( Seq q2),( len ( Seq q1)))))) = ( dom (( Seq q1) \/ ( Shift (( Seq q2),( len ( Seq q1)))))) by XTUPLE_0: 23;

      ( dom ( Seq q1)) misses ( dom ( Shift (( Seq q2),( len ( Seq q1))))) by Th47;

      then

      reconsider ss1 = (( Seq q1) \/ ( Shift (( Seq q2),( len ( Seq q1))))) as Function by GRFUNC_1: 13;

      for x be object st x in ( dom ( Seq ss)) holds (( Seq ss) . x) = (ss1 . x)

      proof

        let x be object;

        assume

         A21: x in ( dom ( Seq ss));

        

         A22: (( Seq ss) . x) = ((ss * ( Sgm ( dom ss))) . x)

        .= (ss . (( Sgm ( dom ss)) . x)) by A21, FUNCT_1: 12

        .= (ss . (( Sgm (( dom q1) \/ ( dom ( Shift (q2,( len p1)))))) . x)) by A3, XTUPLE_0: 23

        .= (ss . ((( Sgm ( dom q1)) ^ ( Sgm ( dom ( Shift (q2,( len p1)))))) . x)) by A1, A2, Lm8;

         A23:

        now

          assume

           A24: x in ( dom ( Seq q1));

          then

           A25: x in ( dom ( Sgm ( dom q1))) by FINSEQ_1: 100;

          then (( Sgm ( dom q1)) . x) in ( rng ( Sgm ( dom q1))) by FUNCT_1:def 3;

          then

           A26: (( Sgm ( dom q1)) . x) in ( dom q1) by FINSEQ_1: 50;

          (( Seq ss) . x) = (ss . (( Sgm ( dom q1)) . x)) by A22, A25, FINSEQ_1:def 7

          .= (q1 . (( Sgm ( dom q1)) . x)) by A3, A26, GRFUNC_1: 15

          .= ((q1 * ( Sgm ( dom q1))) . x) by A25, FUNCT_1: 13

          .= (( Seq q1) . x);

          hence thesis by A24, GRFUNC_1: 15;

        end;

        now

          assume

           A27: x in ( dom ( Shift (( Seq q2),( len ( Seq q1)))));

          ( dom ( Shift (( Seq q2),( len ( Seq q1))))) = { (j + ( len ( Seq q1))) where j be Nat : j in ( dom ( Seq q2)) } by Def12;

          then

          consider j be Nat such that

           A28: x = (j + ( len ( Seq q1))) and

           A29: j in ( dom ( Seq q2)) by A27;

          

           A30: (ss1 . x) = (( Shift (( Seq q2),( len ( Seq q1)))) . x) by A27, GRFUNC_1: 15

          .= (( Seq q2) . j) by A28, A29, Def12;

          

           A31: ex l1 be Nat st (( dom q1) c= ( Seg l1)) by FINSEQ_1:def 12;

          

           A32: ex l2 be Nat st (( dom ( Shift (q2,( len p1)))) c= ( Seg l2)) by FINSEQ_1:def 12;

          ( card ( dom q1)) = ( len ( Sgm ( dom q1))) by A31, FINSEQ_3: 39;

          then

           A33: ( card q1) = ( len ( Sgm ( dom q1))) by CARD_1: 62;

          

           A34: ( len ( Seq q1)) = ( card q1) by FINSEQ_3: 158;

          

           A35: ( dom ( Seq q2)) = ( Seg ( len ( Seq q2))) by FINSEQ_1:def 3;

          ( card q2) = ( len ( Seq q2)) by FINSEQ_3: 158;

          then

           A36: ( card ( Shift (q2,( len p1)))) = ( len ( Seq q2)) by Th41;

          then

           A37: ( card ( dom ( Shift (q2,( len p1))))) = ( len ( Seq q2)) by CARD_1: 62;

          

           A38: ( card ( dom ( Shift (q2,( len p1))))) = ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) by A32, FINSEQ_3: 39;

          

           A39: ( len ( Sgm ( dom ( Shift (q2,( len p1)))))) = ( len ( Seq q2)) by A32, A37, FINSEQ_3: 39;

          

           A40: ( dom ( Seq q2)) = ( dom ( Sgm ( dom ( Shift (q2,( len p1)))))) by A35, A36, A38, CARD_1: 62, FINSEQ_1:def 3;

          

           A41: j in ( dom ( Sgm ( dom ( Shift (q2,( len p1)))))) by A29, A35, A39, FINSEQ_1:def 3;

          (( Sgm ( dom ( Shift (q2,( len p1))))) . j) in ( rng ( Sgm ( dom ( Shift (q2,( len p1)))))) by A29, A40, FUNCT_1:def 3;

          then

           A42: (( Sgm ( dom ( Shift (q2,( len p1))))) . j) in ( dom ( Shift (q2,( len p1)))) by FINSEQ_1: 50;

          (( Seq ss) . x) = (ss . (( Sgm ( dom ( Shift (q2,( len p1))))) . j)) by A22, A28, A33, A34, A41, FINSEQ_1:def 7

          .= (( Shift (q2,( len p1))) . (( Sgm ( dom ( Shift (q2,( len p1))))) . j)) by A3, A42, GRFUNC_1: 15

          .= ((( Shift (q2,( len p1))) * ( Sgm ( dom ( Shift (q2,( len p1)))))) . j) by A29, A40, FUNCT_1: 13

          .= (( Seq ( Shift (q2,( len p1)))) . j)

          .= (( Seq q2) . j) by A29, Th57;

          hence thesis by A30;

        end;

        hence thesis by A4, A7, A21, A23, XBOOLE_0:def 3;

      end;

      then ( Seq ss) = ss1 by A4, A7, A20;

      hence thesis by A3, A4;

    end;

    theorem :: VALUED_1:64

    for p1,p2 be FinSequence, q1,q2 be FinSubsequence st q1 c= p1 & q2 c= p2 holds ex ss be FinSubsequence st ss = (q1 \/ ( Shift (q2,( len p1)))) & (( Seq q1) ^ ( Seq q2)) = ( Seq ss)

    proof

      let p1,p2 be FinSequence, q1,q2 be FinSubsequence;

      assume that

       A1: q1 c= p1 and

       A2: q2 c= p2;

      consider ss be FinSubsequence such that

       A3: ss = (q1 \/ ( Shift (q2,( len p1)))) and

       A4: ( dom ( Seq ss)) = ( Seg (( len ( Seq q1)) + ( len ( Seq q2)))) and

       A5: ( Seq ss) = (( Seq q1) \/ ( Shift (( Seq q2),( len ( Seq q1))))) by A1, A2, Th62;

      

       A6: for j1 be Nat st j1 in ( dom ( Seq q1)) holds (( Seq ss) . j1) = (( Seq q1) . j1) by A5, GRFUNC_1: 15;

      for j2 be Nat st j2 in ( dom ( Seq q2)) holds (( Seq ss) . (( len ( Seq q1)) + j2)) = (( Seq q2) . j2)

      proof

        let j2 be Nat;

        assume

         A7: j2 in ( dom ( Seq q2));

        ( dom ( Shift (( Seq q2),( len ( Seq q1))))) = { (k + ( len ( Seq q1))) where k be Nat : k in ( dom ( Seq q2)) } by Def12;

        then (( len ( Seq q1)) + j2) in ( dom ( Shift (( Seq q2),( len ( Seq q1))))) by A7;

        

        hence (( Seq ss) . (( len ( Seq q1)) + j2)) = (( Shift (( Seq q2),( len ( Seq q1)))) . (( len ( Seq q1)) + j2)) by A5, GRFUNC_1: 15

        .= (( Seq q2) . j2) by A7, Def12;

      end;

      then ( Seq ss) = (( Seq q1) ^ ( Seq q2)) by A4, A6, FINSEQ_1:def 7;

      hence thesis by A3;

    end;

    theorem :: VALUED_1:65

    for F be non empty NAT -defined finite Function holds ( card ( CutLastLoc F)) = (( card F) -' 1)

    proof

      let F be non empty NAT -defined finite Function;

      

       A1: ( card F) >= ( 0 + 1) by NAT_1: 13;

      

      thus ( card ( CutLastLoc F)) = (( card F) - 1) by Th37

      .= (( card F) -' 1) by A1, XREAL_1: 233;

    end;

    theorem :: VALUED_1:66

    for F,G be non empty NAT -defined finite Function st ( dom F) = ( dom G) holds ( LastLoc F) = ( LastLoc G);

    theorem :: VALUED_1:67

    for f be non empty NAT -defined finite Function holds ( Shift ((f +~ (x,y)),i)) = (( Shift (f,i)) +~ (x,y))

    proof

      let f be non empty NAT -defined finite Function;

      

       A1: ( dom f) = ( dom (f +~ (x,y))) by FUNCT_4: 99;

      

       A2: ( dom (( Shift (f,i)) +~ (x,y))) = ( dom ( Shift (f,i))) by FUNCT_4: 99

      .= { (m + i) where m be Nat : m in ( dom (f +~ (x,y))) } by A1, Def12;

      for m be Nat st m in ( dom (f +~ (x,y))) holds ((( Shift (f,i)) +~ (x,y)) . (m + i)) = ((f +~ (x,y)) . m)

      proof

        let m be Nat;

        assume m in ( dom (f +~ (x,y)));

        then

         A3: (m + i) in ( dom (( Shift (f,i)) +~ (x,y))) by A2;

        then

         A4: (m + i) in ( dom ( Shift (f,i))) by FUNCT_4: 99;

        consider mm be Nat such that

         A5: (m + i) = (mm + i) and

         A6: mm in ( dom (f +~ (x,y))) by A2, A3;

        m = mm by A5;

        then m in ( dom (f +~ (x,y))) by A6;

        then

         A7: m in ( dom f) by FUNCT_4: 99;

        then

         A8: (( Shift (f,i)) . (m + i)) = (f . m) by Def12;

        per cases ;

          suppose

           A9: (( Shift (f,i)) . (m + i)) = x;

          

          hence ((( Shift (f,i)) +~ (x,y)) . (m + i)) = y by A4, FUNCT_4: 106

          .= ((f +~ (x,y)) . m) by A7, FUNCT_4: 106, A9, A8;

        end;

          suppose

           A10: (( Shift (f,i)) . (m + i)) <> x;

          

          hence ((( Shift (f,i)) +~ (x,y)) . (m + i)) = (( Shift (f,i)) . (m + i)) by FUNCT_4: 105

          .= ((f +~ (x,y)) . m) by A10, A8, FUNCT_4: 105;

        end;

      end;

      hence ( Shift ((f +~ (x,y)),i)) = (( Shift (f,i)) +~ (x,y)) by A2, Def12;

    end;

    theorem :: VALUED_1:68

    for F,G be non empty NAT -defined finite Function st ( dom F) c= ( dom G) holds ( LastLoc F) <= ( LastLoc G) by XXREAL_2: 59;