pre_circ.miz



    begin

    scheme :: PRE_CIRC:sch1

    FraenkelFinIm { A() -> finite non empty set , F( set) -> set , P[ set] } :

{ F(x) where x be Element of A() : P[x] } is finite;

      set B = { F(x) where x be Element of A() : x in A() };

      

       A1: { F(x) where x be Element of A() : P[x] } c= B

      proof

        let a be object;

        assume a in { F(x) where x be Element of A() : P[x] };

        then ex b be Element of A() st F(b) = a & P[b];

        hence thesis;

      end;

      

       A2: A() is finite;

      B is finite from FRAENKEL:sch 21( A2);

      hence thesis by A1;

    end;

    begin

    ::$Canceled

    theorem :: PRE_CIRC:2

    for I be set, MSS be ManySortedSet of I holds ((MSS # ) . ( <*> I)) = { {} }

    proof

      let I be set, MSS be ManySortedSet of I;

      reconsider eI = ( <*> I) as Element of (I * ) by FINSEQ_1: 49;

      

      thus ((MSS # ) . ( <*> I)) = ( product (MSS * eI)) by FINSEQ_2:def 5

      .= { {} } by CARD_3: 10;

    end;

    reserve i,j,x,y for object,

f,g for Function;

    scheme :: PRE_CIRC:sch2

    MSSLambda2Part { I() -> set , P[ object], F,G( object) -> object } :

ex f be ManySortedSet of I() st for i be Element of I() st i in I() holds (P[i] implies (f . i) = F(i)) & ( not P[i] implies (f . i) = G(i));

      defpred Q[ object, object] means (P[$1] implies $2 = F($1)) & ( not P[$1] implies $2 = G($1));

       A1:

      now

        let i be object such that i in I();

        thus ex j be object st Q[i, j]

        proof

          per cases ;

            suppose

             A2: P[i];

            take F(i);

            thus thesis by A2;

          end;

            suppose

             A3: not P[i];

            take G(i);

            thus thesis by A3;

          end;

        end;

      end;

      consider f be ManySortedSet of I() such that

       A4: for i be object st i in I() holds Q[i, (f . i)] from PBOOLE:sch 3( A1);

      take f;

      thus thesis by A4;

    end;

    registration

      let I be set;

      cluster non-empty finite-yielding for ManySortedSet of I;

      existence

      proof

        reconsider f = (I --> { {} }) as Function;

        reconsider f as ManySortedSet of I;

        take f;

        thus f is non-empty;

        thus f is finite-yielding by FUNCOP_1: 7;

      end;

    end

    registration

      let I be set, M be ManySortedSet of I, A be Subset of I;

      cluster (M | A) -> total;

      coherence

      proof

        set B = (M | A);

        ( dom B) = (( dom M) /\ A) & ( dom M) = I by PARTFUN1:def 2, RELAT_1: 61;

        then ( dom B) = A by XBOOLE_1: 28;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let I be set, M be ManySortedSet of I, A be Subset of I;

      cluster (M | A) -> total;

      coherence ;

    end

    registration

      let M be non-empty Function, A be set;

      cluster (M | A) -> non-empty;

      coherence

      proof

        ( rng (M | A)) c= ( rng M) by RELAT_1: 70;

        hence not {} in ( rng (M | A)) by RELAT_1:def 9;

      end;

    end

    theorem :: PRE_CIRC:3

    

     Th2: for I be non empty set, B be non-empty ManySortedSet of I holds ( union ( rng B)) is non empty

    proof

      let I be non empty set, B be non-empty ManySortedSet of I;

      set i = the Element of I;

      i in I;

      then i in ( dom B) by PARTFUN1:def 2;

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

      hence thesis by ORDERS_1: 6;

    end;

    theorem :: PRE_CIRC:4

    

     Th3: for I be set holds ( uncurry (I --> {} )) = {}

    proof

      let I be set;

      per cases ;

        suppose I = {} ;

        hence thesis by FUNCT_5: 43;

      end;

        suppose I <> {} ;

        

        then ( rng (I --> {} )) = { {} } by FUNCOP_1: 8

        .= ( Funcs ( {} qua set, {} qua set)) by FUNCT_5: 57;

        

        then ( dom ( uncurry (I --> {} ))) = [:( dom (I --> {} )), {} :] by FUNCT_5: 26

        .= {} by ZFMISC_1: 90;

        hence thesis;

      end;

    end;

    theorem :: PRE_CIRC:5

    for I be non empty set, A be set, B be non-empty ManySortedSet of I, F be ManySortedFunction of (I --> A) qua totalI -defined Function, B holds ( dom ( commute F)) = A

    proof

      let I be non empty set, A be set, B be non-empty ManySortedSet of I, F be ManySortedFunction of (I --> A), B;

      

       A1: ( dom B) = I by PARTFUN1:def 2;

      

       A2: ( dom F) = I by PARTFUN1:def 2;

      per cases ;

        suppose

         A3: A is empty;

        ( rng F) c= { {} }

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider i be object such that

           A4: i in I & x = (F . i) by A2, FUNCT_1:def 3;

          ((I --> A) . i) = A & x is Function of ((I --> A) . i), (B . i) by A4, FUNCOP_1: 7, PBOOLE:def 15;

          then x = {} by A3;

          hence thesis by TARSKI:def 1;

        end;

        then ( rng F) = { {} } by ZFMISC_1: 33;

        then

         A5: F = (I --> {} ) by A2, FUNCOP_1: 9;

        ( commute F) = ( curry' ( uncurry F)) by FUNCT_6:def 10

        .= {} by A5, Th3, FUNCT_5: 42;

        hence thesis by A3;

      end;

        suppose

         A6: A is non empty;

        ( rng F) c= ( Funcs (A,( union ( rng B))))

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider i be object such that

           A7: i in ( dom F) and

           A8: x = (F . i) by FUNCT_1:def 3;

          ((I --> A) . i) = A by A2, A7, FUNCOP_1: 7;

          then

          reconsider x9 = x as Function of A, (B . i) by A2, A7, A8, PBOOLE:def 15;

          (B . i) in ( rng B) by A1, A2, A7, FUNCT_1:def 3;

          then ( rng x9) c= (B . i) & (B . i) c= ( union ( rng B)) by RELAT_1:def 19, ZFMISC_1: 74;

          then

           A9: ( rng x9) c= ( union ( rng B));

          ( dom x9) = A by A2, A7, FUNCT_2:def 1;

          hence thesis by A9, FUNCT_2:def 2;

        end;

        then F in ( Funcs (I,( Funcs (A,( union ( rng B)))))) by A2, FUNCT_2:def 2;

        then ( commute F) in ( Funcs (A,( Funcs (I,( union ( rng B)))))) by A6, FUNCT_6: 55;

        then

         A10: ( commute F) is Function of A, ( Funcs (I,( union ( rng B)))) by FUNCT_2: 66;

        ( union ( rng B)) is non empty by Th2;

        then ( Funcs (I,( union ( rng B)))) is non empty by FUNCT_2: 8;

        hence thesis by A10, FUNCT_2:def 1;

      end;

    end;

    scheme :: PRE_CIRC:sch3

    LambdaRecCorrD { D() -> non empty set , A() -> Element of D() , F( Nat, Element of D()) -> Element of D() } :

(ex f be sequence of D() st (f . 0 ) = A() & for i be Nat holds (f . (i + 1)) = F(i,.)) & for f1,f2 be sequence of D() st ((f1 . 0 ) = A() & for i be Nat holds (f1 . (i + 1)) = F(i,.)) & ((f2 . 0 ) = A() & for i be Nat holds (f2 . (i + 1)) = F(i,.)) holds f1 = f2;

      thus ex f be sequence of D() st (f . 0 ) = A() & for i be Nat holds (f . (i + 1)) = F(i,.) from NAT_1:sch 12;

      let f1,f2 be sequence of D() such that

       A1: (f1 . 0 ) = A() and

       A2: for i be Nat holds (f1 . (i + 1)) = F(i,.) and

       A3: (f2 . 0 ) = A() and

       A4: for i be Nat holds (f2 . (i + 1)) = F(i,.);

      thus f1 = f2 from NAT_1:sch 16( A1, A2, A3, A4);

    end;

    scheme :: PRE_CIRC:sch4

    LambdaMSFD { J() -> non empty set , I() -> Subset of J() , A,B() -> ManySortedSet of I() , F( object) -> set } :

ex f be ManySortedFunction of A(), B() st for i be Element of J() st i in I() holds (f . i) = F(i)

      provided

       A1: for i be Element of J() st i in I() holds F(i) is Function of (A() . i), (B() . i);

      consider f be ManySortedSet of I() such that

       A2: for i be object st i in I() holds (f . i) = F(i) from PBOOLE:sch 4;

      f is Function-yielding

      proof

        let i be object;

        assume i in ( dom f);

        then

         A3: i in I() by PARTFUN1:def 2;

        then F(i) is Function by A1;

        hence thesis by A2, A3;

      end;

      then

      reconsider f as ManySortedFunction of I();

      f is ManySortedFunction of A(), B()

      proof

        let i;

        assume

         A4: i in I();

        then F(i) is Function of (A() . i), (B() . i) by A1;

        hence thesis by A2, A4;

      end;

      then

      reconsider f as ManySortedFunction of A(), B();

      take f;

      thus thesis by A2;

    end;

    theorem :: PRE_CIRC:6

    for I be set, f be non-empty ManySortedSet of I, g be Function, s be Element of ( product f) st ( dom g) c= ( dom f) & for x be set st x in ( dom g) holds (g . x) in (f . x) holds (s +* g) is Element of ( product f)

    proof

      let I be set, f be non-empty ManySortedSet of I, g be Function, s be Element of ( product f);

      assume that

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

       A2: for x be set st x in ( dom g) holds (g . x) in (f . x);

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom f);

        per cases ;

          suppose

           A5: x in ( dom g);

          then ((s +* g) . x) = (g . x) by FUNCT_4: 13;

          hence ((s +* g) . x) in (f . x) by A2, A5;

        end;

          suppose

           A6: not x in ( dom g);

          

           A7: ex g9 be Function st s = g9 & ( dom g9) = ( dom f) & for x be object st x in ( dom f) holds (g9 . x) in (f . x) by CARD_3:def 5;

          ((s +* g) . x) = (s . x) by A6, FUNCT_4: 11;

          hence ((s +* g) . x) in (f . x) by A4, A7;

        end;

      end;

      ( dom (s +* g)) = (( dom s) \/ ( dom g)) & ( dom s) = ( dom f) by CARD_3: 9, FUNCT_4:def 1;

      then ( dom (s +* g)) = ( dom f) by A1, XBOOLE_1: 12;

      hence thesis by A3, CARD_3: 9;

    end;

    theorem :: PRE_CIRC:7

    for A,B be non empty set, C be non-empty ManySortedSet of A, InpFs be ManySortedFunction of (A --> B), C, b be Element of B holds ex c be ManySortedSet of A st c = (( commute InpFs) . b) & c in C

    proof

      let A,B be non empty set, C be non-empty ManySortedSet of A, InpFs be ManySortedFunction of (A --> B), C, b be Element of B;

      

       A1: ( dom InpFs) = A by PARTFUN1:def 2;

      ( dom ( uncurry InpFs)) = [:A, B:]

      proof

        thus ( dom ( uncurry InpFs)) c= [:A, B:]

        proof

          let i be object;

          assume i in ( dom ( uncurry InpFs));

          then

          consider x, g, y such that

           A2: i = [x, y] and

           A3: x in ( dom InpFs) and

           A4: g = (InpFs . x) and

           A5: y in ( dom g) by FUNCT_5:def 2;

          g is Function of ((A --> B) . x), (C . x) by A1, A3, A4, PBOOLE:def 15;

          then ( dom g) = ((A --> B) . x) by A1, A3, FUNCT_2:def 1;

          then ( dom g) = B by A1, A3, FUNCOP_1: 7;

          hence thesis by A1, A2, A3, A5, ZFMISC_1: 87;

        end;

        let i1,i2 be object;

        reconsider g = (InpFs . ( [i1, i2] `1 )) as Function;

        assume

         A6: [i1, i2] in [:A, B:];

        then

         A7: ( [i1, i2] `1 ) in ( dom InpFs) by A1, MCART_1: 10;

        g is Function of ((A --> B) . ( [i1, i2] `1 )), (C . ( [i1, i2] `1 )) by A6, MCART_1: 10, PBOOLE:def 15;

        then ( dom g) = ((A --> B) . ( [i1, i2] `1 )) by A1, A7, FUNCT_2:def 1;

        then ( dom g) = B by A6, FUNCOP_1: 7, MCART_1: 10;

        then

         A8: ( [i1, i2] `2 ) in ( dom g) by A6, MCART_1: 10;

        thus thesis by A7, A8, FUNCT_5: 38;

      end;

      then

       A9: ( commute InpFs) = ( curry' ( uncurry InpFs)) & ex g be Function st (( curry' ( uncurry InpFs)) . b) = g & ( dom g) = A & ( rng g) c= ( rng ( uncurry InpFs)) & for i st i in A holds (g . i) = (( uncurry InpFs) . (i,b)) by FUNCT_5: 32, FUNCT_6:def 10;

      then

      reconsider c = (( commute InpFs) . b) as ManySortedSet of A by PARTFUN1:def 2, RELAT_1:def 18;

      take c;

      thus c = (( commute InpFs) . b);

      let i be object;

      reconsider h = (InpFs . i) as Function;

      assume

       A10: i in A;

      then ((A --> B) . i) = B by FUNCOP_1: 7;

      then

       A11: h is Function of B, (C . i) by A10, PBOOLE:def 15;

      then

       A12: ( dom h) = B by A10, FUNCT_2:def 1;

      (c . i) = (( uncurry InpFs) . (i,b)) by A9, A10

      .= (h . b) by A1, A10, A12, FUNCT_5: 38;

      hence thesis by A10, A11, FUNCT_2: 5;

    end;

    theorem :: PRE_CIRC:8

    for n be Nat, a be set holds ( product (n |-> {a})) = {(n |-> a)}

    proof

      let n be Nat, a be set;

      now

        let i be object;

        hereby

          assume i in ( product (n |-> {a}));

          then

          consider g be Function such that

           A1: i = g and

           A2: ( dom g) = ( dom (n |-> {a})) and

           A3: for x be object st x in ( dom (n |-> {a})) holds (g . x) in ((n |-> {a}) . x) by CARD_3:def 5;

          

           A4: ( dom g) = ( Seg n) by A2;

          now

            let x be object;

            assume

             A5: x in ( dom g);

            then (g . x) in ((n |-> {a}) . x) by A2, A3;

            then (g . x) in {a} by A4, A5, FUNCOP_1: 7;

            hence (g . x) = a by TARSKI:def 1;

          end;

          hence i = (n |-> a) by A1, A4, FUNCOP_1: 11;

        end;

        assume

         A6: i = (n |-> a);

        then

        reconsider g = i as Function;

         A7:

        now

          let x be object;

          assume x in ( dom (n |-> {a}));

          then x in ( Seg n);

          then (g . x) = a & ((n |-> {a}) . x) = {a} by A6, FUNCOP_1: 7;

          hence (g . x) in ((n |-> {a}) . x) by TARSKI:def 1;

        end;

        ( dom g) = ( Seg n) by A6

        .= ( dom (n |-> {a}));

        hence i in ( product (n |-> {a})) by A7, CARD_3: 9;

      end;

      hence thesis by TARSKI:def 1;

    end;

    begin

    reserve T,T1 for finite Tree,

t,p for Element of T,

t1 for Element of T1;

    registration

      let D be non empty set;

      cluster -> finite for Element of ( FinTrees D);

      coherence

      proof

        let t be Element of ( FinTrees D);

        ( dom t) is finite;

        hence thesis by FINSET_1: 10;

      end;

    end

    registration

      let T be finite DecoratedTree;

      let t be Element of ( dom T);

      cluster (T | t) -> finite;

      coherence

      proof

        ( dom (T | t)) = (( dom T) | t) by TREES_2:def 10;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: PRE_CIRC:9

    

     Th8: ((T | p),{ t : p is_a_prefix_of t }) are_equipotent

    proof

      set X = { t : p is_a_prefix_of t };

      deffunc F( Element of (T | p)) = (p ^ $1);

      consider f be Function such that

       A1: ( dom f) = (T | p) and

       A2: for n be Element of (T | p) holds (f . n) = F(n) from FUNCT_1:sch 4;

      take f;

      thus f is one-to-one

      proof

        let x,y be object such that

         A3: x in ( dom f) & y in ( dom f) and

         A4: (f . x) = (f . y);

        reconsider m = x, n = y as Element of (T | p) by A1, A3;

        (p ^ m) = (f . n) by A2, A4

        .= (p ^ n) by A2;

        hence thesis by FINSEQ_1: 33;

      end;

      thus ( dom f) = (T | p) by A1;

      thus ( rng f) c= X

      proof

        let i be object;

        assume i in ( rng f);

        then

        consider n be object such that

         A5: n in ( dom f) and

         A6: i = (f . n) by FUNCT_1:def 3;

        reconsider n as Element of (T | p) by A1, A5;

        reconsider t = (p ^ n) as Element of T by TREES_1:def 6;

        (f . n) = (p ^ n) & p is_a_prefix_of t by A2, TREES_1: 1;

        hence thesis by A6;

      end;

      let i be object;

      assume i in X;

      then

       A7: ex t be Element of T st i = t & p is_a_prefix_of t;

      then

      consider n be FinSequence such that

       A8: i = (p ^ n) by TREES_1: 1;

      n is FinSequence of NAT by A7, A8, FINSEQ_1: 36;

      then

      reconsider n as Element of (T | p) by A7, A8, TREES_1:def 6;

      i = (f . n) by A2, A8;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    registration

      let T be finite DecoratedTree-like Function;

      let t be Element of ( dom T);

      let T1 be finite DecoratedTree;

      cluster (T with-replacement (t,T1)) -> finite;

      coherence

      proof

        ( dom (T with-replacement (t,T1))) = (( dom T) with-replacement (t,( dom T1))) by TREES_2:def 11;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: PRE_CIRC:10

    

     Th9: (T with-replacement (p,T1)) = ({ t : not p is_a_prefix_of t } \/ the set of all (p ^ t1))

    proof

      defpred P2[ set] means not contradiction;

      defpred P1[ set] means $1 = $1;

      deffunc F( FinSequence) = (p ^ $1);

      set A = { t : not p is_a_proper_prefix_of t }, B = { F(t1) : P1[t1] }, C = { t : not p is_a_prefix_of t }, D = { F(t1) : P2[t1] };

      now

        let x be object;

        hereby

          assume x in A;

          then

          consider t such that

           A1: x = t and

           A2: not p is_a_proper_prefix_of t;

           not p is_a_prefix_of t or t = p by A2;

          hence x in C or x in {p} by A1, TARSKI:def 1;

        end;

        assume x in C or x in {p};

        then x = p or ex t st t = x & not p is_a_prefix_of t by TARSKI:def 1;

        then

        consider t such that

         A3: t = x and

         A4: t = p or not p is_a_prefix_of t;

         not p is_a_proper_prefix_of t by A4;

        hence x in A by A3;

      end;

      then

       A5: A = (C \/ {p}) by XBOOLE_0:def 3;

       {} is Element of T1 & (p ^ {} ) = p by FINSEQ_1: 34, TREES_1: 22;

      then

       A6: p in D;

      

      thus (T with-replacement (p,T1)) = ((C \/ {p}) \/ D) by A5, TREES_1: 32

      .= (C \/ ( {p} \/ D)) by XBOOLE_1: 4

      .= (C \/ D) by A6, ZFMISC_1: 40;

    end;

    theorem :: PRE_CIRC:11

    

     Th10: for f be FinSequence of NAT st f in (T with-replacement (p,T1)) & p is_a_prefix_of f holds ex t1 st f = (p ^ t1)

    proof

      let f be FinSequence of NAT such that

       A1: f in (T with-replacement (p,T1)) and

       A2: p is_a_prefix_of f;

      

       A3: not f in { t : not p is_a_prefix_of t }

      proof

        assume f in { t : not p is_a_prefix_of t };

        then ex t st f = t & not p is_a_prefix_of t;

        hence contradiction by A2;

      end;

      (T with-replacement (p,T1)) = ({ t : not p is_a_prefix_of t } \/ the set of all (p ^ t1)) by Th9;

      then f in the set of all (p ^ t1) by A1, A3, XBOOLE_0:def 3;

      hence thesis;

    end;

    theorem :: PRE_CIRC:12

    

     Th11: for p be Tree-yielding FinSequence, k be Element of NAT st (k + 1) in ( dom p) holds (( tree p) | <*k*>) = (p . (k + 1))

    proof

      let p be Tree-yielding FinSequence, k be Element of NAT ;

      assume (k + 1) in ( dom p);

      then (k + 1) <= ( len p) by FINSEQ_3: 25;

      then k < ( len p) by NAT_1: 13;

      hence thesis by TREES_3: 49;

    end;

    theorem :: PRE_CIRC:13

    for q be DTree-yielding FinSequence, k be Nat st (k + 1) in ( dom q) holds <*k*> in ( tree ( doms q))

    proof

      let q be DTree-yielding FinSequence, k be Nat;

      

       A1: k < (k + 1) by XREAL_1: 29;

      

       A2: ( dom q) = ( Seg ( len q)) & ( Seg ( len ( doms q))) = ( dom ( doms q)) by FINSEQ_1:def 3;

      assume

       A3: (k + 1) in ( dom q);

      then (k + 1) <= ( len q) by FINSEQ_3: 25;

      then k < ( len q) by A1, XXREAL_0: 2;

      then

       A4: k < ( len ( doms q)) by A2, FINSEQ_1: 6, TREES_3: 37;

      ( dom ( doms q)) = ( dom q) by TREES_3: 37;

      then (( doms q) . (k + 1)) is Tree by A3, TREES_3: 22;

      then

       A5: {} in (( doms q) . (k + 1)) by TREES_1: 22;

       <*k*> = ( <*k*> ^ {} ) by FINSEQ_1: 34;

      hence thesis by A5, A4, TREES_3:def 15;

    end;

    theorem :: PRE_CIRC:14

    

     Th13: for p,q be Tree-yielding FinSequence, k be Element of NAT st ( len p) = ( len q) & (k + 1) in ( dom p) & for i be Nat st i in ( dom p) & i <> (k + 1) holds (p . i) = (q . i) holds for t be Tree st (q . (k + 1)) = t holds ( tree q) = (( tree p) with-replacement ( <*k*>,t))

    proof

      let p,q be Tree-yielding FinSequence, k be Element of NAT such that

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

       A2: (k + 1) in ( dom p) and

       A3: for i be Nat st i in ( dom p) & i <> (k + 1) holds (p . i) = (q . i);

      let t be Tree;

      set o = <*k*>;

      (k + 1) <= ( len p) by A2, FINSEQ_3: 25;

      then

       A4: k < ( len p) by NAT_1: 13;

      assume

       A5: (q . (k + 1)) = t;

       A6:

      now

        let s be FinSequence of NAT ;

        hereby

          assume

           A7: s in ( tree q);

          per cases by A7, TREES_3:def 15;

            suppose s = {} ;

            hence s in ( tree p) & not o is_a_proper_prefix_of s or ex r be FinSequence of NAT st r in t & s = (o ^ r) by TREES_1: 22;

          end;

            suppose ex n be Nat, r be FinSequence st n < ( len q) & r in (q . (n + 1)) & s = ( <*n*> ^ r);

            then

            consider n be Nat, r be FinSequence such that

             A8: n < ( len q) and

             A9: r in (q . (n + 1)) and

             A10: s = ( <*n*> ^ r);

            now

              per cases ;

                case

                 A11: n = k;

                reconsider r as FinSequence of NAT by A10, FINSEQ_1: 36;

                take r;

                thus r in t & s = (o ^ r) by A5, A9, A10, A11;

              end;

                case

                 A12: n <> k;

                1 <= (n + 1) & (n + 1) <= ( len p) by A1, A8, NAT_1: 11, NAT_1: 13;

                then (n + 1) in ( dom p) by FINSEQ_3: 25;

                then (q . (n + 1)) = (p . (n + 1)) by A3, A12, XCMPLX_1: 2;

                hence s in ( tree p) by A1, A8, A9, A10, TREES_3:def 15;

                assume o is_a_proper_prefix_of s;

                then o is_a_prefix_of s;

                then ex s1 be FinSequence st s = (o ^ s1) by TREES_1: 1;

                

                then k = (s . 1) by FINSEQ_1: 41

                .= n by A10, FINSEQ_1: 41;

                hence contradiction by A12;

              end;

            end;

            hence s in ( tree p) & not o is_a_proper_prefix_of s or ex r be FinSequence of NAT st r in t & s = (o ^ r);

          end;

        end;

        assume

         A13: s in ( tree p) & not o is_a_proper_prefix_of s or ex r be FinSequence of NAT st r in t & s = (o ^ r);

        per cases by A13;

          suppose that

           A14: s in ( tree p) and

           A15: not o is_a_proper_prefix_of s;

          now

            per cases by A14, TREES_3:def 15;

              suppose s = {} ;

              hence s in ( tree q) by TREES_1: 22;

            end;

              suppose ex n be Nat, r be FinSequence st n < ( len p) & r in (p . (n + 1)) & s = ( <*n*> ^ r);

              then

              consider n be Nat, r be FinSequence such that

               A16: n < ( len p) and

               A17: r in (p . (n + 1)) and

               A18: s = ( <*n*> ^ r);

              now

                per cases ;

                  suppose

                   A19: r = {} ;

                  1 <= (n + 1) & (n + 1) <= ( len q) by A1, A16, NAT_1: 11, NAT_1: 13;

                  then (n + 1) in ( dom q) by FINSEQ_3: 25;

                  then (q . (n + 1)) is Tree by TREES_3: 22;

                  then r in (q . (n + 1)) by A19, TREES_1: 22;

                  hence s in ( tree q) by A1, A16, A18, TREES_3:def 15;

                end;

                  suppose r <> {} ;

                  then

                   A20: n <> k by A15, A18, FINSEQ_1: 87, TREES_1: 1;

                  1 <= (n + 1) & (n + 1) <= ( len p) by A16, NAT_1: 11, NAT_1: 13;

                  then (n + 1) in ( dom p) by FINSEQ_3: 25;

                  then (q . (n + 1)) = (p . (n + 1)) by A3, A20, XCMPLX_1: 2;

                  hence s in ( tree q) by A1, A16, A17, A18, TREES_3:def 15;

                end;

              end;

              hence s in ( tree q);

            end;

          end;

          hence s in ( tree q);

        end;

          suppose ex r be FinSequence of NAT st r in t & s = (o ^ r);

          hence s in ( tree q) by A1, A4, A5, TREES_3:def 15;

        end;

      end;

      (p . (k + 1)) is Tree by A2, TREES_3: 22;

      then

       A21: {} in (p . (k + 1)) by TREES_1: 22;

      o = (o ^ {} ) by FINSEQ_1: 34;

      then o in ( tree p) by A4, A21, TREES_3:def 15;

      hence thesis by A6, TREES_1:def 9;

    end;

    theorem :: PRE_CIRC:15

    for e1,e2 be finite DecoratedTree, x be set, k be Element of NAT , p be DTree-yielding FinSequence st <*k*> in ( dom e1) & e1 = (x -tree p) holds ex q be DTree-yielding FinSequence st (e1 with-replacement ( <*k*>,e2)) = (x -tree q) & ( len q) = ( len p) & (q . (k + 1)) = e2 & for i be Nat st i in ( dom p) & i <> (k + 1) holds (q . i) = (p . i)

    proof

      let e1,e2 be finite DecoratedTree, x be set, k be Element of NAT , p be DTree-yielding FinSequence such that

       A1: <*k*> in ( dom e1) and

       A2: e1 = (x -tree p);

      consider j be Nat, T be DecoratedTree, w be Node of T such that

       A3: j < ( len p) and T = (p . (j + 1)) and

       A4: <*k*> = ( <*j*> ^ w) by A1, A2, TREES_4: 11;

      consider pp be DTree-yielding FinSequence such that

       A5: p = pp and

       A6: ( dom (x -tree p)) = ( tree ( doms pp)) by TREES_4:def 4;

      

       A7: ( dom ( doms pp)) = ( dom p) by A5, TREES_3: 37;

      deffunc F( Nat) = ( IFEQ ($1,(k + 1),e2,(p . $1)));

      set o = <*k*>;

      consider q be FinSequence such that

       A8: ( len q) = ( len p) and

       A9: for i be Nat st i in ( dom q) holds (q . i) = F(i) from FINSEQ_1:sch 2;

      

       A10: ( dom q) = ( Seg ( len p)) by A8, FINSEQ_1:def 3;

      

       A11: ( dom q) = ( dom p) by A8, FINSEQ_3: 29;

      now

        let x;

        assume

         A12: x in ( dom q);

        then

        reconsider i = x as Nat;

        

         A13: i = (k + 1) or i <> (k + 1);

        (q . i) = ( IFEQ (i,(k + 1),e2,(p . i))) by A9, A12;

        then (q . i) = e2 or (q . i) = (p . i) by A13, FUNCOP_1:def 8;

        hence (q . x) is DecoratedTree by A11, A12, TREES_3: 24;

      end;

      then

      reconsider q as DTree-yielding FinSequence by TREES_3: 24;

      consider qq be DTree-yielding FinSequence such that

       A14: q = qq and

       A15: ( dom (x -tree q)) = ( tree ( doms qq)) by TREES_4:def 4;

      

       A16: ( len ( doms pp)) = ( len p) by A5, TREES_3: 38

      .= ( len ( doms qq)) by A8, A14, TREES_3: 38;

      

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

       A18:

      now

        let i be Nat;

        assume that

         A19: i in ( dom ( doms pp)) and

         A20: i <> (k + 1);

        

         A21: (q . i) = ( IFEQ (i,(k + 1),e2,(p . i))) by A9, A10, A17, A7, A19

        .= (p . i) by A20, FUNCOP_1:def 8;

        reconsider pii = (p . i) as DecoratedTree by A7, A19, TREES_3: 24;

        

        thus (( doms pp) . i) = ( dom pii) by A5, A7, A19, FUNCT_6: 22

        .= (( doms qq) . i) by A11, A14, A7, A19, A21, FUNCT_6: 22;

      end;

      reconsider dqq = ( doms qq) as Tree-yielding FinSequence;

      take q;

       <*j*> = <*k*> by A4, FINSEQ_1: 88;

      

      then

       A22: j = ( <*k*> . 1) by FINSEQ_1:def 8

      .= k by FINSEQ_1:def 8;

      then 1 <= (k + 1) & (k + 1) <= ( len p) by A3, NAT_1: 11, NAT_1: 13;

      then

       A23: (k + 1) in ( dom p) by FINSEQ_3: 25;

      then (k + 1) in ( Seg ( len p)) by FINSEQ_1:def 3;

      

      then

       A24: (q . (k + 1)) = ( IFEQ ((k + 1),(k + 1),e2,(p . (k + 1)))) by A9, A10

      .= e2 by FUNCOP_1:def 8;

      then (( doms qq) . (k + 1)) = ( dom e2) by A11, A23, A14, FUNCT_6: 22;

      then

       A25: ( dom (x -tree q)) = (( dom e1) with-replacement (o,( dom e2))) by A2, A23, A15, A6, A16, A7, A18, Th13;

      for f be FinSequence of NAT st f in (( dom e1) with-replacement (o,( dom e2))) holds not o is_a_prefix_of f & ((x -tree q) . f) = (e1 . f) or ex r be FinSequence of NAT st r in ( dom e2) & f = (o ^ r) & ((x -tree q) . f) = (e2 . r)

      proof

        reconsider o9 = o as Element of ( dom e1) by A1;

        let f be FinSequence of NAT ;

        assume

         A26: f in (( dom e1) with-replacement (o,( dom e2)));

        per cases by A26, Th10;

          suppose

           A27: not o9 is_a_prefix_of f;

          

           A28: ((x -tree q) . f) = (e1 . f)

          proof

            per cases by A15, A25, A26, TREES_3:def 15;

              suppose

               A29: f = {} ;

              

              hence ((x -tree q) . f) = x by TREES_4:def 4

              .= (e1 . f) by A2, A29, TREES_4:def 4;

            end;

              suppose ex w be Nat, u be FinSequence st w < ( len dqq) & u in (dqq . (w + 1)) & f = ( <*w*> ^ u);

              then

              consider w be Nat, u be FinSequence such that

               A30: w < ( len ( doms q)) and

               A31: u in (( doms q) . (w + 1)) and

               A32: f = ( <*w*> ^ u) by A14;

              reconsider u as FinSequence of NAT by A32, FINSEQ_1: 36;

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

              reconsider ww = <*w*> as FinSequence of NAT ;

              

               A33: (w + 1) <> (k + 1) by A27, A32, TREES_1: 1;

              

               A34: ex pp be DTree-yielding FinSequence st p = pp & ( dom (x -tree p)) = ( tree ( doms pp)) by TREES_4:def 4;

              

               A35: w < ( len q) by A30, TREES_3: 38;

              then

               A36: ((x -tree q) | <*w*>) = (q . (w + 1)) by TREES_4:def 4;

              1 <= (w + 1) & (w + 1) <= ( len p) by A8, A35, NAT_1: 11, NAT_1: 13;

              then

               A37: (w + 1) in ( dom p) by FINSEQ_3: 25;

              then

              reconsider pw1 = (p . (w + 1)) as DecoratedTree by TREES_3: 24;

              

               A38: (q . (w + 1)) = ( IFEQ ((w + 1),(k + 1),e2,(p . (w + 1)))) by A9, A10, A17, A37

              .= (p . (w + 1)) by A33, FUNCOP_1:def 8;

              (w + 1) in ( dom ( doms p)) by A37, TREES_3: 37;

              

              then

               A39: (( dom (x -tree p)) | <*w*>) = (( doms p) . (w + 1)) by A34, Th11

              .= ( dom pw1) by A37, FUNCT_6: 22

              .= (( doms q) . (w + 1)) by A11, A37, A38, FUNCT_6: 22;

              (w + 1) in ( dom ( doms q)) by A11, A37, TREES_3: 37;

              then (( dom (x -tree q)) | <*w*>) = (( doms q) . (w + 1)) by A14, A15, Th11;

              

              hence ((x -tree q) . f) = (((x -tree q) | ww) . u) by A31, A32, TREES_2:def 10

              .= (((x -tree p) | ww) . u) by A8, A35, A36, A38, TREES_4:def 4

              .= (e1 . f) by A2, A31, A32, A39, TREES_2:def 10;

            end;

          end;

          assume o is_a_prefix_of f or ((x -tree q) . f) <> (e1 . f);

          hence thesis by A27, A28;

        end;

          suppose ex t1 be Element of ( dom e2) st f = (o9 ^ t1);

          then

          consider r be Element of ( dom e2) such that

           A40: f = (o ^ r);

          assume o is_a_prefix_of f or ((x -tree q) . f) <> (e1 . f);

          

           A41: ((x -tree q) | o) = (q . (k + 1)) by A8, A3, A22, TREES_4:def 4;

          reconsider r as FinSequence of NAT ;

          take r;

          thus

           A42: r in ( dom e2);

          thus f = (o ^ r) by A40;

          r in (( dom (x -tree q)) | o) by A1, A25, A42, TREES_1: 33;

          hence thesis by A24, A40, A41, TREES_2:def 10;

        end;

      end;

      hence (e1 with-replacement (o,e2)) = (x -tree q) by A1, A25, TREES_2:def 11;

      thus ( len q) = ( len p) by A8;

      thus (q . (k + 1)) = e2 by A24;

      let i be Nat;

      assume i in ( dom p);

      then (q . i) = ( IFEQ (i,(k + 1),e2,(p . i))) by A9, A10, A17;

      hence thesis by FUNCOP_1:def 8;

    end;

    theorem :: PRE_CIRC:16

    for T be finite Tree, p be Element of T st p <> {} holds ( card (T | p)) < ( card T)

    proof

      let T be finite Tree, p be Element of T;

      reconsider p9 = p as Element of ( NAT * ) by FINSEQ_1:def 11;

      set X = { (p9 ^ n) where n be Element of ( NAT * ) : n in (T | p) };

      

       A1: ((T | p),X) are_equipotent

      proof

        deffunc F( Element of (T | p)) = (p9 ^ $1);

        consider f be Function such that

         A2: ( dom f) = (T | p) and

         A3: for n be Element of (T | p) holds (f . n) = F(n) from FUNCT_1:sch 4;

        take f;

        thus f is one-to-one

        proof

          let x,y be object such that

           A4: x in ( dom f) & y in ( dom f) and

           A5: (f . x) = (f . y);

          reconsider m = x, n = y as Element of (T | p) by A2, A4;

          (p9 ^ m) = (f . n) by A3, A5

          .= (p9 ^ n) by A3;

          hence thesis by FINSEQ_1: 33;

        end;

        thus ( dom f) = (T | p) by A2;

        thus ( rng f) c= X

        proof

          let i be object;

          assume i in ( rng f);

          then

          consider n be object such that

           A6: n in ( dom f) and

           A7: i = (f . n) by FUNCT_1:def 3;

          (T | p) c= ( NAT * ) by TREES_1:def 3;

          then

          reconsider n as Element of ( NAT * ) by A2, A6;

          (f . n) = (p9 ^ n) by A2, A3, A6;

          hence thesis by A2, A6, A7;

        end;

        let i be object;

        assume i in X;

        then

        consider n be Element of ( NAT * ) such that

         A8: i = (p9 ^ n) and

         A9: n in (T | p);

        reconsider n as Element of (T | p) by A9;

        i = (f . n) by A3, A8;

        hence thesis by A2, FUNCT_1:def 3;

      end;

      then

      reconsider X as finite set by CARD_1: 38;

      

       A10: ( card X) = ( card (T | p)) by A1, CARD_1: 5;

      assume

       A11: p <> {} ;

      

       A12: X <> T

      proof

        assume X = T;

        then {} in X by TREES_1: 22;

        then ex n be Element of ( NAT * ) st {} = (p9 ^ n) & n in (T | p);

        hence contradiction by A11;

      end;

      X c= T

      proof

        let i be object;

        assume i in X;

        then ex n be Element of ( NAT * ) st i = (p9 ^ n) & n in (T | p);

        hence thesis by TREES_1:def 6;

      end;

      then X c< T by A12;

      hence thesis by A10, CARD_2: 48;

    end;

    theorem :: PRE_CIRC:17

    

     Th16: for T,T1 be finite Tree, p be Element of T holds (( card (T with-replacement (p,T1))) + ( card (T | p))) = (( card T) + ( card T1))

    proof

      let T, T1, p;

      defpred P1[ Element of T] means not p is_a_prefix_of $1;

      defpred P2[ Element of T] means p is_a_prefix_of $1;

      set A = { t : P1[t] };

      set B = { t : P2[t] };

      set C = the set of all (p ^ t1);

      

       A1: A is Subset of T from DOMAIN_1:sch 7;

      

       A2: B is Subset of T from DOMAIN_1:sch 7;

      

       A3: (T1,C) are_equipotent

      proof

        deffunc F( Element of T1) = (p ^ $1);

        consider f be Function such that

         A4: ( dom f) = T1 and

         A5: for n be Element of T1 holds (f . n) = F(n) from FUNCT_1:sch 4;

        take f;

        thus f is one-to-one

        proof

          let x,y be object such that

           A6: x in ( dom f) & y in ( dom f) and

           A7: (f . x) = (f . y);

          reconsider m = x, n = y as Element of T1 by A4, A6;

          (p ^ m) = (f . n) by A5, A7

          .= (p ^ n) by A5;

          hence thesis by FINSEQ_1: 33;

        end;

        thus ( dom f) = T1 by A4;

        thus ( rng f) c= C

        proof

          let i be object;

          assume i in ( rng f);

          then

          consider n be object such that

           A8: n in ( dom f) and

           A9: i = (f . n) by FUNCT_1:def 3;

          T1 c= ( NAT * ) by TREES_1:def 3;

          then

          reconsider n as Element of ( NAT * ) by A4, A8;

          (f . n) = (p ^ n) by A4, A5, A8;

          hence thesis by A4, A8, A9;

        end;

        let i be object;

        assume i in C;

        then

        consider n be Element of T1 such that

         A10: i = (p ^ n);

        i = (f . n) by A5, A10;

        hence thesis by A4, FUNCT_1:def 3;

      end;

      reconsider A, B as finite set by A1, A2;

      now

        let x be object;

        hereby

          assume x in T;

          then

          reconsider t = x as Element of T;

          p is_a_prefix_of t or not p is_a_prefix_of t;

          hence x in A or x in B;

        end;

        assume x in A or x in B;

        hence x in T by A1, A2;

      end;

      then

       A11: T = (A \/ B) by XBOOLE_0:def 3;

      

       A12: A misses C

      proof

        assume not thesis;

        then

        consider x be object such that

         A13: x in (A /\ C) by XBOOLE_0: 4;

        x in C by A13, XBOOLE_0:def 4;

        then

         A14: ex t1 st x = (p ^ t1);

        x in A by A13, XBOOLE_0:def 4;

        then ex t st x = t & not p is_a_prefix_of t;

        hence contradiction by A14, TREES_1: 1;

      end;

      

       A15: A misses B

      proof

        assume not thesis;

        then

        consider x be object such that

         A16: x in (A /\ B) by XBOOLE_0: 4;

        x in B by A16, XBOOLE_0:def 4;

        then

         A17: ex t st x = t & p is_a_prefix_of t;

        x in A by A16, XBOOLE_0:def 4;

        then ex t st x = t & not p is_a_prefix_of t;

        hence contradiction by A17;

      end;

      

       A18: (T with-replacement (p,T1)) = (A \/ C) by Th9;

      reconsider C as finite set by A3, CARD_1: 38;

      

       A19: ( card T1) = ( card C) by A3, CARD_1: 5;

      ((T | p),B) are_equipotent by Th8;

      then ( card (T | p)) = ( card B) by CARD_1: 5;

      

      hence (( card (T with-replacement (p,T1))) + ( card (T | p))) = ((( card A) + ( card C)) + ( card B)) by A18, A12, CARD_2: 40

      .= ((( card A) + ( card B)) + ( card C))

      .= (( card T) + ( card T1)) by A11, A15, A19, CARD_2: 40;

    end;

    theorem :: PRE_CIRC:18

    for T,T1 be finite DecoratedTree, p be Element of ( dom T) holds (( card (T with-replacement (p,T1))) + ( card (T | p))) = (( card T) + ( card T1))

    proof

      let T,T1 be finite DecoratedTree, p be Element of ( dom T);

      

       A1: ( card ( dom T)) = ( card T) & ( card ( dom T1)) = ( card T1) by CARD_1: 62;

      

       A2: ( card ( dom (T with-replacement (p,T1)))) = ( card (T with-replacement (p,T1))) & ( card ( dom (T | p))) = ( card (T | p)) by CARD_1: 62;

      ( dom (T with-replacement (p,T1))) = (( dom T) with-replacement (p,( dom T1))) & ( dom (T | p)) = (( dom T) | p) by TREES_2:def 10, TREES_2:def 11;

      hence thesis by A1, A2, Th16;

    end;

    registration

      let x be object;

      cluster ( root-tree x) -> finite;

      coherence

      proof

        ( root-tree x) = { [ {} , x]} by TREES_4: 6;

        hence thesis;

      end;

    end

    theorem :: PRE_CIRC:19

    for x be set holds ( card ( root-tree x)) = 1

    proof

      let x be set;

      ( root-tree x) = { [ {} , x]} by TREES_4: 6;

      hence thesis by CARD_1: 30;

    end;

    begin

    theorem :: PRE_CIRC:20

    

     Th19: for F be non empty finite set holds (( card F) - 1) = (( card F) -' 1)

    proof

      let F be non empty finite set;

      (( card F) - 1) >= 0 by NAT_1: 14, XREAL_1: 48;

      hence thesis by XREAL_0:def 2;

    end;

    theorem :: PRE_CIRC:21

    for f,g be Function holds (( dom f),( dom g)) are_equipotent iff (f,g) are_equipotent

    proof

      let f,g be Function;

      

       A1: ( card f) = ( card ( dom f)) & ( card g) = ( card ( dom g)) by CARD_1: 62;

      hereby

        assume (( dom f),( dom g)) are_equipotent ;

        then ( card ( dom f)) = ( card ( dom g)) by CARD_1: 5;

        hence (f,g) are_equipotent by A1, CARD_1: 5;

      end;

      assume (f,g) are_equipotent ;

      then ( card f) = ( card g) by CARD_1: 5;

      hence thesis by A1, CARD_1: 5;

    end;

    theorem :: PRE_CIRC:22

    for f,g be finite Function st ( dom f) misses ( dom g) holds ( card (f +* g)) = (( card f) + ( card g))

    proof

      let f,g be finite Function such that

       A1: ( dom f) misses ( dom g);

      

      thus ( card (f +* g)) = ( card ( dom (f +* g))) by CARD_1: 62

      .= ( card (( dom f) \/ ( dom g))) by FUNCT_4:def 1

      .= (( card ( dom f)) + ( card ( dom g))) by A1, CARD_2: 40

      .= (( card ( dom f)) + ( card g)) by CARD_1: 62

      .= (( card f) + ( card g)) by CARD_1: 62;

    end;

    theorem :: PRE_CIRC:23

    for n be Nat holds { k where k be Nat : k > n } is infinite

    proof

      let n be Nat;

      set X = { k where k be Nat : k > n };

      

       A1: X c= NAT

      proof

        let x be object;

        assume x in X;

        then ex k be Nat st x = k & k > n;

        hence thesis by ORDINAL1:def 12;

      end;

      (n + 1) > (n + 0 ) by XREAL_1: 8;

      then

       A2: (n + 1) in X;

      assume X is finite;

      then

      reconsider X as non empty finite Subset of NAT by A1, A2;

      set m = ( max X);

      m in X by XXREAL_2:def 8;

      then

      consider k be Nat such that

       A3: m = k and

       A4: k > n;

      (k + 1) > (k + 0 ) by XREAL_1: 8;

      then (k + 1) > n by A4, XXREAL_0: 2;

      then (m + 1) in X by A3;

      then (m + 1) <= (m + 0 ) by XXREAL_2:def 8;

      hence contradiction by XREAL_1: 8;

    end;

    theorem :: PRE_CIRC:24

    

     Th23: for D be finite set, k be Nat st ( card D) = (k + 1) holds ex x be Element of D, C be Subset of D st D = (C \/ {x}) & ( card C) = k

    proof

      let D be finite set, k be Nat;

      assume

       A1: ( card D) = (k + 1);

      then D <> {} ;

      then

      consider x be object such that

       A2: x in D by XBOOLE_0:def 1;

      reconsider C = (D \ {x}) as Subset of D;

      reconsider x as Element of D by A2;

      take x, C;

      x in {x} by TARSKI:def 1;

      then

       A3: not x in C by XBOOLE_0:def 5;

       {x} c= D by A2, ZFMISC_1: 31;

      hence D = (C \/ {x}) by XBOOLE_1: 45;

      then ( card D) = (( card C) + 1) by A3, CARD_2: 41;

      hence thesis by A1;

    end;

    theorem :: PRE_CIRC:25

    

     Th24: for D be finite set st ( card D) = 1 holds ex x be Element of D st D = {x}

    proof

      let D be finite set;

      assume ( card D) = 1;

      then ( card D) = ( 0 + 1);

      then

      consider x be Element of D, C be Subset of D such that

       A1: D = (C \/ {x}) and

       A2: ( card C) = 0 by Th23;

      take x;

      C = {} by A2;

      hence thesis by A1;

    end;

    reserve k for Nat;

    scheme :: PRE_CIRC:sch5

    MinValue { D() -> non empty finite set , F( Element of D()) -> Real } :

ex x be Element of D() st for y be Element of D() holds F(x) <= F(y);

      defpred P[ Nat] means for A be Subset of D() st ($1 + 1) = ( card A) holds ex x be Element of D() st x in A & for y be Element of D() st y in A holds F(x) <= F(y);

      

       A1: ((( card D()) -' 1) + 1) = ((( card D()) - 1) + 1) by Th19

      .= ( card D());

      

       A2: D() c= D();

      

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

      proof

        let k;

        assume

         A4: P[k];

        now

          let A be Subset of D();

          assume

           A5: ((k + 1) + 1) = ( card A);

          then

           A6: A <> {} ;

          consider x be Element of A, C be Subset of A such that

           A7: A = (C \/ {x}) and

           A8: ( card C) = (k + 1) by A5, Th23;

          x in A by A6;

          then

          reconsider x as Element of D();

          reconsider C as Subset of D() by XBOOLE_1: 1;

          consider z be Element of D() such that

           A9: z in C and

           A10: for y be Element of D() st y in C holds F(z) <= F(y) by A4, A8;

          per cases ;

            suppose

             A11: F(x) <= F(z);

            take x;

            thus x in A by A6;

            hereby

              let y be Element of D();

              assume

               A12: y in A;

              per cases by A7, A12, XBOOLE_0:def 3;

                suppose y in C;

                then F(z) <= F(y) by A10;

                hence F(x) <= F(y) by A11, XXREAL_0: 2;

              end;

                suppose y in {x};

                hence F(x) <= F(y) by TARSKI:def 1;

              end;

            end;

          end;

            suppose

             A13: F(x) > F(z);

            take z;

            thus z in A by A9;

            hereby

              let y be Element of D();

              assume

               A14: y in A;

              per cases by A7, A14, XBOOLE_0:def 3;

                suppose y in C;

                hence F(z) <= F(y) by A10;

              end;

                suppose y in {x};

                hence F(z) <= F(y) by A13, TARSKI:def 1;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A15: P[ 0 ]

      proof

        let A be Subset of D();

        assume ( 0 + 1) = ( card A);

        then

        consider x be Element of A such that

         A16: A = {x} by Th24;

        reconsider x as Element of D() by A16, ZFMISC_1: 31;

        take x;

        thus x in A by A16;

        thus thesis by A16, TARSKI:def 1;

      end;

      for k holds P[k] from NAT_1:sch 2( A15, A3);

      then ((( card D()) -' 1) + 1) = ( card D()) implies ex x be Element of D() st x in D() & for y be Element of D() st y in D() holds F(x) <= F(y) by A2;

      then

      consider x be Element of D() such that x in D() and

       A17: for y be Element of D() st y in D() holds F(x) <= F(y) by A1;

      take x;

      let y be Element of D();

      thus thesis by A17;

    end;