triang_1.miz



    begin

    reserve A,x,y,z,u for set,

m,n for Element of NAT ;

    registration

      let X be non empty set, R be Order of X;

      cluster RelStr (# X, R #) -> non empty;

      coherence ;

    end

    theorem :: TRIANG_1:1

    ( {} |_2 A) = {} ;

    theorem :: TRIANG_1:2

    for F be non empty Poset, A be Subset of F st A is finite & A <> {} & for B,C be Element of F st B in A & C in A holds B <= C or C <= B holds ex m be Element of F st m in A & for C be Element of F st C in A holds m <= C

    proof

      let F be non empty Poset;

      defpred P[ set] means $1 <> {} implies ex m be Element of F st m in $1 & for C be Element of F st C in $1 holds m <= C;

      let A be Subset of F such that

       A1: A is finite and

       A2: A <> {} and

       A3: for B,C be Element of F st B in A & C in A holds B <= C or C <= B;

       A4:

      now

        let x be Element of F, B be Subset of F such that

         A5: x in A and

         A6: B c= A and

         A7: P[B];

        reconsider x9 = x as Element of F;

        now

          per cases ;

            suppose

             A8: not ex y be Element of F st y in B & y <= x9;

            assume (B \/ {x}) <> {} ;

            take m = x9;

            x in {x} by TARSKI:def 1;

            hence m in (B \/ {x}) by XBOOLE_0:def 3;

            let C be Element of F;

            assume C in (B \/ {x});

            then

             A9: C in B or C in {x} by XBOOLE_0:def 3;

            then not C <= x9 or C = x by A8, TARSKI:def 1;

            hence m <= C by A3, A5, A6, A9, TARSKI:def 1;

          end;

            suppose

             A10: ex y be Element of F st y in B & y <= x9;

            assume (B \/ {x}) <> {} ;

            consider y be Element of F such that

             A11: y in B and

             A12: y <= x9 by A10;

            consider m be Element of F such that

             A13: m in B and

             A14: for C be Element of F st C in B holds m <= C by A7, A11;

            take m;

            thus m in (B \/ {x}) by A13, XBOOLE_0:def 3;

            let C be Element of F;

            assume C in (B \/ {x});

            then

             A15: C in B or C in {x} by XBOOLE_0:def 3;

            m <= y by A11, A14;

            then m <= x9 by A12, ORDERS_2: 3;

            hence m <= C by A14, A15, TARSKI:def 1;

          end;

        end;

        hence P[(B \/ {x})];

      end;

      

       A16: P[( {} the carrier of F)];

       P[A] from PRE_POLY:sch 2( A1, A16, A4);

      hence thesis by A2;

    end;

    registration

      let P be non empty Poset, A be non empty finite Subset of P, x be Element of P;

      cluster ( InitSegm (A,x)) -> finite;

      coherence ;

    end

    begin

    definition

      let C be non empty Poset;

      :: TRIANG_1:def1

      func symplexes (C) -> Subset of ( Fin the carrier of C) equals { A where A be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A };

      coherence

      proof

        set S = { A where A be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A };

        S c= ( Fin the carrier of C)

        proof

          let x be object;

          assume x in S;

          then ex a be Element of ( Fin the carrier of C) st x = a & the InternalRel of C linearly_orders a;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let C be non empty Poset;

      cluster ( symplexes C) -> with_non-empty_element;

      coherence

      proof

        set x = the Element of C;

        reconsider a = {x} as Element of ( Fin the carrier of C) by FINSUB_1:def 5;

        

         A1: the InternalRel of C is_connected_in a

        proof

          let k,l be object;

          assume that

           A2: k in a and

           A3: l in a and

           A4: k <> l;

          k = x by A2, TARSKI:def 1;

          hence thesis by A3, A4, TARSKI:def 1;

        end;

        

         A5: ( field the InternalRel of C) = the carrier of C by ORDERS_1: 12;

        then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def 12;

        then

         A6: the InternalRel of C is_antisymmetric_in a;

        the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def 16;

        then

         A7: the InternalRel of C is_transitive_in a;

        the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def 9;

        then the InternalRel of C is_reflexive_in a;

        then the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def 9;

        then a in { A where A be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A };

        hence thesis by SETFAM_1:def 10;

      end;

    end

    reserve C for non empty Poset;

    theorem :: TRIANG_1:3

    

     Th3: for x be Element of C holds {x} in ( symplexes C)

    proof

      let x be Element of C;

      reconsider a = {x} as Element of ( Fin the carrier of C) by FINSUB_1:def 5;

      

       A1: the InternalRel of C is_connected_in a

      proof

        let k,l be object;

        assume that

         A2: k in a and

         A3: l in a and

         A4: k <> l;

        k = x by A2, TARSKI:def 1;

        hence thesis by A3, A4, TARSKI:def 1;

      end;

      

       A5: ( field the InternalRel of C) = the carrier of C by ORDERS_1: 12;

      then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def 12;

      then

       A6: the InternalRel of C is_antisymmetric_in a;

      the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def 16;

      then

       A7: the InternalRel of C is_transitive_in a;

      the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def 9;

      then the InternalRel of C is_reflexive_in a;

      then the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def 9;

      hence thesis;

    end;

    theorem :: TRIANG_1:4

     {} in ( symplexes C)

    proof

       {} is Subset of C by SUBSET_1: 1;

      then

      reconsider a = {} as Element of ( Fin the carrier of C) by FINSUB_1:def 5;

      

       A1: the InternalRel of C is_antisymmetric_in a;

      

       A2: the InternalRel of C is_connected_in a;

      

       A3: the InternalRel of C is_transitive_in a;

      the InternalRel of C is_reflexive_in a;

      then the InternalRel of C linearly_orders a by A1, A3, A2, ORDERS_1:def 9;

      hence thesis;

    end;

    theorem :: TRIANG_1:5

    

     Th5: for x,s be set st x c= s & s in ( symplexes C) holds x in ( symplexes C)

    proof

      let x,s be set;

      assume that

       A1: x c= s and

       A2: s in ( symplexes C);

      consider s1 be Element of ( Fin the carrier of C) such that

       A3: s1 = s and

       A4: the InternalRel of C linearly_orders s1 by A2;

      s1 c= the carrier of C by FINSUB_1:def 5;

      then x c= the carrier of C by A1, A3;

      then

      reconsider x1 = x as Element of ( Fin the carrier of C) by A1, A2, FINSUB_1:def 5;

      the InternalRel of C linearly_orders x by A1, A3, A4, ORDERS_1: 38;

      then x1 in { A where A be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A };

      hence thesis;

    end;

    theorem :: TRIANG_1:6

    

     Th6: for C be non empty Poset, A be non empty Element of ( symplexes C) st ( card A) = n holds ( dom ( SgmX (the InternalRel of C,A))) = ( Seg n)

    proof

      let C be non empty Poset, A be non empty Element of ( symplexes C);

      set f = ( SgmX (the InternalRel of C,A));

      A in { A1 where A1 be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A1 };

      then

       A1: ex A1 be Element of ( Fin the carrier of C) st A1 = A & the InternalRel of C linearly_orders A1;

      assume ( card A) = n;

      then ( len f) = n by A1, PRE_POLY: 11;

      hence thesis by FINSEQ_1:def 3;

    end;

    registration

      let C be non empty Poset;

      cluster non empty for Element of ( symplexes C);

      existence

      proof

        set x = the Element of C;

         {x} in ( symplexes C) by Th3;

        hence thesis;

      end;

    end

    begin

    definition

      mode SetSequence is ManySortedSet of NAT ;

    end

    definition

      let IT be SetSequence;

      :: TRIANG_1:def2

      attr IT is lower_non-empty means

      : Def2: for n be Nat st (IT . n) is non empty holds for m be Nat st m < n holds (IT . m) is non empty;

    end

    registration

      cluster lower_non-empty for SetSequence;

      existence

      proof

        set f = ( NAT --> 1);

        reconsider f as ManySortedSet of NAT ;

        take f;

        for n be Nat st (f . n) is non empty holds for m be Nat st m < n holds (f . m) is non empty by FUNCOP_1: 7, ORDINAL1:def 12;

        hence thesis;

      end;

    end

    definition

      let X be SetSequence;

      :: TRIANG_1:def3

      func FuncsSeq X -> SetSequence means

      : Def3: for n be Nat holds (it . n) = ( Funcs ((X . (n + 1)),(X . n)));

      existence

      proof

        deffunc U( Element of NAT ) = ( Funcs ((X . ($1 + 1)),(X . $1)));

        consider f be ManySortedSet of NAT such that

         A1: for n be Element of NAT holds (f . n) = U(n) from PBOOLE:sch 5;

        reconsider f as SetSequence;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let a,b be SetSequence;

        assume that

         A2: for n be Nat holds (a . n) = ( Funcs ((X . (n + 1)),(X . n))) and

         A3: for n be Nat holds (b . n) = ( Funcs ((X . (n + 1)),(X . n)));

        let n be Element of NAT ;

        (a . n) = ( Funcs ((X . (n + 1)),(X . n))) by A2;

        hence (a . n) c= (b . n) by A3;

        (a . n) = ( Funcs ((X . (n + 1)),(X . n))) by A2;

        hence (b . n) c= (a . n) by A3;

      end;

    end

    registration

      let X be lower_non-empty SetSequence;

      let n be Nat;

      cluster (( FuncsSeq X) . n) -> non empty;

      coherence

      proof

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

        then

         A1: (X . (n + 1)) = {} or (X . n) <> {} by Def2;

        (( FuncsSeq X) . n) = ( Funcs ((X . (n + 1)),(X . n))) by Def3;

        hence thesis by A1, FUNCT_2: 8;

      end;

    end

    definition

      let n be Nat;

      let f be Element of ( Funcs (( Seg n),( Seg (n + 1))));

      :: TRIANG_1:def4

      func @ f -> FinSequence of REAL equals f;

      coherence

      proof

        consider x be Function such that

         A1: x = f and ( dom x) = ( Seg n) and ( rng x) c= ( Seg (n + 1)) by FUNCT_2:def 2;

        reconsider x as FinSequence of ( Seg (n + 1)) by A1, FINSEQ_2: 25;

        ( Seg (n + 1)) c= REAL by NUMBERS: 19;

        then x is FinSequence of REAL by FINSEQ_2: 24;

        hence thesis by A1;

      end;

    end

    definition

      :: TRIANG_1:def5

      func NatEmbSeq -> SetSequence means

      : Def5: for n be Nat holds (it . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing };

      existence

      proof

        deffunc U( Element of NAT ) = { f where f be Element of ( Funcs (( Seg $1),( Seg ($1 + 1)))) : ( @ f) is increasing };

        consider F be ManySortedSet of NAT such that

         A1: for n be Element of NAT holds (F . n) = U(n) from PBOOLE:sch 5;

        reconsider F as SetSequence;

        take F;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let a,b be SetSequence;

        assume that

         A2: for n be Nat holds (a . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing } and

         A3: for n be Nat holds (b . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing };

        let n be Element of NAT ;

        (a . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing } by A2;

        hence (a . n) c= (b . n) by A3;

        (a . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing } by A2;

        hence (b . n) c= (a . n) by A3;

      end;

    end

    registration

      let n be Nat;

      cluster ( NatEmbSeq . n) -> non empty;

      coherence

      proof

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

        then

         A1: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

        

         A2: ( rng ( id ( Seg n))) = ( Seg n);

        ( dom ( id ( Seg n))) = ( Seg n);

        then

        reconsider n1 = ( idseq n) as Element of ( Funcs (( Seg n),( Seg (n + 1)))) by A1, A2, FUNCT_2:def 2;

        ( @ n1) is increasing;

        then n1 in { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing };

        hence thesis by Def5;

      end;

    end

    registration

      let n be Nat;

      cluster -> Function-like Relation-like for Element of ( NatEmbSeq . n);

      coherence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        let x be Element of ( NatEmbSeq . n);

        

         A1: x in ( NatEmbSeq . n9);

        ( NatEmbSeq . n) = { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing } by Def5;

        then ex f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) st x = f & ( @ f) is increasing by A1;

        hence thesis;

      end;

    end

    definition

      let X be SetSequence;

      mode triangulation of X is ManySortedFunction of NatEmbSeq , ( FuncsSeq X);

    end

    definition

      struct TriangStr (# the SkeletonSeq -> SetSequence,

the FacesAssign -> ManySortedFunction of NatEmbSeq , ( FuncsSeq the SkeletonSeq) #)

       attr strict strict;

    end

    definition

      let T be TriangStr;

      :: TRIANG_1:def6

      attr T is lower_non-empty means

      : Def6: the SkeletonSeq of T is lower_non-empty;

    end

    registration

      cluster lower_non-empty strict for TriangStr;

      existence

      proof

        set Sk = ( NAT --> {} );

        reconsider Sk as ManySortedSet of NAT ;

        set A = the ManySortedFunction of NatEmbSeq , ( FuncsSeq Sk);

        take TriangStr (# Sk, A #);

        for n be Nat st (Sk . n) is non empty holds for m be Nat st m < n holds (Sk . m) is non empty by FUNCOP_1: 7, ORDINAL1:def 12;

        then Sk is lower_non-empty;

        hence thesis;

      end;

    end

    registration

      let T be lower_non-empty TriangStr;

      cluster the SkeletonSeq of T -> lower_non-empty;

      coherence by Def6;

    end

    registration

      let S be lower_non-empty SetSequence, F be ManySortedFunction of NatEmbSeq , ( FuncsSeq S);

      cluster TriangStr (# S, F #) -> lower_non-empty;

      coherence ;

    end

    begin

    definition

      let T be TriangStr;

      let n be Nat;

      mode Symplex of T,n is Element of (the SkeletonSeq of T . n);

    end

    definition

      let n be Nat;

      mode Face of n is Element of ( NatEmbSeq . n);

    end

    definition

      let T be lower_non-empty TriangStr, n be Nat, x be Symplex of T, (n + 1), f be Face of n;

      assume

       A1: (the SkeletonSeq of T . (n + 1)) <> {} ;

      :: TRIANG_1:def7

      func face (x,f) -> Symplex of T, n means

      : Def7: for F,G be Function st F = (the FacesAssign of T . n) & G = (F . f) holds it = (G . x);

      existence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        reconsider F = (the FacesAssign of T . n9) as Function of ( NatEmbSeq . n9), (( FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def 15;

        (F . f) in (( FuncsSeq the SkeletonSeq of T) . n9) by FUNCT_2: 5;

        then (F . f) in ( Funcs ((the SkeletonSeq of T . (n + 1)),(the SkeletonSeq of T . n))) by Def3;

        then

        consider G be Function such that

         A2: G = (F . f) and

         A3: ( dom G) = (the SkeletonSeq of T . (n + 1)) and

         A4: ( rng G) c= (the SkeletonSeq of T . n) by FUNCT_2:def 2;

        (G . x) in ( rng G) by A1, A3, FUNCT_1:def 3;

        then

        reconsider S = (G . x) as Symplex of T, n by A4;

        take S;

        let F1,G1 be Function;

        assume that

         A5: F1 = (the FacesAssign of T . n) and

         A6: G1 = (F1 . f);

        thus thesis by A2, A5, A6;

      end;

      uniqueness

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        let S1,S2 be Symplex of T, n;

        assume that

         A7: for F,G be Function st F = (the FacesAssign of T . n) & G = (F . f) holds S1 = (G . x) and

         A8: for F,G be Function st F = (the FacesAssign of T . n) & G = (F . f) holds S2 = (G . x);

        reconsider F = (the FacesAssign of T . n9) as Function of ( NatEmbSeq . n9), (( FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def 15;

        (F . f) in (( FuncsSeq the SkeletonSeq of T) . n9) by FUNCT_2: 5;

        then (F . f) in ( Funcs ((the SkeletonSeq of T . (n + 1)),(the SkeletonSeq of T . n))) by Def3;

        then

        consider G be Function such that

         A9: G = (F . f) and ( dom G) = (the SkeletonSeq of T . (n + 1)) and ( rng G) c= (the SkeletonSeq of T . n) by FUNCT_2:def 2;

        S1 = (G . x) by A7, A9;

        hence thesis by A8, A9;

      end;

    end

    definition

      let C be non empty Poset;

      :: TRIANG_1:def8

      func Triang C -> lower_non-empty strict TriangStr means (the SkeletonSeq of it . 0 ) = { {} } & (for n be Nat st n > 0 holds (the SkeletonSeq of it . n) = { ( SgmX (the InternalRel of C,A)) where A be non empty Element of ( symplexes C) : ( card A) = n }) & for n be Nat, f be Face of n, s be Element of (the SkeletonSeq of it . (n + 1)) st s in (the SkeletonSeq of it . (n + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds ( face (s,f)) = (( SgmX (the InternalRel of C,A)) * f);

      existence

      proof

        deffunc U( Element of NAT ) = ( IFEQ ($1, 0 , { {} },{ ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = $1 }));

        consider Sk be SetSequence such that

         A1: for n holds (Sk . n) = U(n) from PBOOLE:sch 5;

         A2:

        now

          let n be Nat;

          assume

           A3: n <> 0 ;

          n in NAT by ORDINAL1:def 12;

          

          hence (Sk . n) = ( IFEQ (n, 0 , { {} },{ ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = n })) by A1

          .= { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = n } by A3, FUNCOP_1:def 8;

        end;

        

         A4: (Sk . 0 ) = ( IFEQ ( 0 , 0 , { {} },{ ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = 0 })) by A1

        .= { {} } by FUNCOP_1:def 8;

        Sk is lower_non-empty

        proof

          defpred X[ Nat] means (Sk . $1) is non empty;

          let n be Nat;

          

           A5: for m st m < n & X[(m + 1)] holds X[m]

          proof

            let m;

            assume that m < n and

             A6: (Sk . (m + 1)) is non empty;

            consider g be object such that

             A7: g in (Sk . (m + 1)) by A6;

            (Sk . (m + 1)) = { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = (m + 1) } by A2;

            then

            consider s be non empty Element of ( symplexes C) such that g = ( SgmX (the InternalRel of C,s)) and

             A8: ( card s) = (m + 1) by A7;

            set x = the Element of s;

            reconsider sx = (s \ {x}) as finite set;

            (sx \/ {x}) = (s \/ {x}) by XBOOLE_1: 39;

            then

             A9: (sx \/ {x}) = s by XBOOLE_1: 12;

             not x in sx by ZFMISC_1: 56;

            then

             A10: (m + 1) = (( card sx) + 1) by A8, A9, CARD_2: 41;

            per cases ;

              suppose m = 0 ;

              hence thesis by A4;

            end;

              suppose

               A11: m <> 0 ;

              then

              reconsider sx as non empty Element of ( symplexes C) by A10, Th5, XBOOLE_1: 36;

              ( SgmX (the InternalRel of C,sx)) in { ( SgmX (the InternalRel of C,s1)) where s1 be non empty Element of ( symplexes C) : ( card s1) = m } by A10;

              hence thesis by A2, A11;

            end;

          end;

          assume

           A12: X[n];

          

           A13: for m be Element of NAT st m <= n holds X[m] from PRE_POLY:sch 1( A12, A5);

          let m be Nat;

          assume

           A14: m < n;

          m in NAT by ORDINAL1:def 12;

          hence thesis by A13, A14;

        end;

        then

        reconsider Sk as lower_non-empty SetSequence;

        defpred X[ object, object, object] means ex n be Nat, y be Face of n st $2 = y & $3 = n & for s be Element of (Sk . (n + 1)) st s in (Sk . (n + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds for g1 be Function st g1 = $1 holds (g1 . s) = (( SgmX (the InternalRel of C,A)) * y);

        

         A15: for i be object st i in NAT holds for x be object st x in ( NatEmbSeq . i) holds ex y be object st y in (( FuncsSeq Sk) . i) & X[y, x, i]

        proof

          let i be object;

          assume i in NAT ;

          then

          reconsider n = i as Element of NAT ;

          let x be object;

          assume

           A16: x in ( NatEmbSeq . i);

          then

          reconsider y = x as Face of n;

          reconsider y1 = y as Function;

          x in { f where f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) : ( @ f) is increasing } by A16, Def5;

          then

           A17: ex f be Element of ( Funcs (( Seg n),( Seg (n + 1)))) st f = x & ( @ f) is increasing;

          then

          consider y2 be Function such that

           A18: y2 = y1 and

           A19: ( dom y2) = ( Seg n) and

           A20: ( rng y2) c= ( Seg (n + 1)) by FUNCT_2:def 2;

          reconsider y2 as FinSequence by A19, FINSEQ_1:def 2;

          

           A21: ( len y2) = n by A19, FINSEQ_1:def 3;

          defpred X[ object, object] means ex f be Function st f = $1 & $2 = (f * y1);

          

           A22: for s be object st s in (Sk . (n + 1)) holds ex u be object st X[s, u]

          proof

            let s be object;

            assume s in (Sk . (n + 1));

            then s in { ( SgmX (the InternalRel of C,s9)) where s9 be non empty Element of ( symplexes C) : ( card s9) = (n + 1) } by A2;

            then

            consider A be non empty Element of ( symplexes C) such that

             A23: ( SgmX (the InternalRel of C,A)) = s and ( card A) = (n + 1);

            reconsider u = (( SgmX (the InternalRel of C,A)) * y) as set;

            consider f be Function such that

             A24: f = s by A23;

            take u, f;

            thus thesis by A23, A24;

          end;

          consider g be Function such that

           A25: ( dom g) = (Sk . (n + 1)) and

           A26: for s be object st s in (Sk . (n + 1)) holds X[s, (g . s)] from CLASSES1:sch 1( A22);

          reconsider y2 as FinSequence of ( Seg (n + 1)) by A20, FINSEQ_1:def 4;

          reconsider g9 = g as set;

          take g9;

          

           A27: y2 is one-to-one

          proof

            let a,b be object;

            assume that

             A28: a in ( dom y2) and

             A29: b in ( dom y2) and

             A30: (y2 . a) = (y2 . b);

            reconsider a, b as Element of NAT by A28, A29;

            now

              assume

               A31: a <> b;

              per cases by A31, XXREAL_0: 1;

                suppose a < b;

                hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def 1;

              end;

                suppose b < a;

                hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def 1;

              end;

            end;

            hence thesis;

          end;

          ( rng g) c= (Sk . n)

          proof

            reconsider F = ( symplexes C) as with_non-empty_element Subset of ( Fin the carrier of C);

            let z be object;

            assume z in ( rng g);

            then

            consider a be object such that

             A32: a in ( dom g) and

             A33: z = (g . a) by FUNCT_1:def 3;

            consider f be Function such that

             A34: f = a and

             A35: (g . a) = (f * y2) by A18, A25, A26, A32;

            per cases ;

              suppose

               A36: n = 0 ;

              then ( Seg n) = {} ;

              then ( dom (f * y1)) = {} by A18, A19, RELAT_1: 25, XBOOLE_1: 3;

              then z = {} by A18, A33, A35;

              hence thesis by A4, A36, TARSKI:def 1;

            end;

              suppose

               A37: n <> 0 ;

              f in { ( SgmX (the InternalRel of C,s1)) where s1 be non empty Element of ( symplexes C) : ( card s1) = (n + 1) } by A2, A25, A32, A34;

              then

              consider s1 be non empty Element of ( symplexes C) such that

               A38: ( SgmX (the InternalRel of C,s1)) = f and

               A39: ( card s1) = (n + 1);

              s1 in { A where A be Element of ( Fin the carrier of C) : the InternalRel of C linearly_orders A };

              then

               A40: ex s19 be Element of ( Fin the carrier of C) st s19 = s1 & the InternalRel of C linearly_orders s19;

              then ( rng f) = s1 by A38, PRE_POLY:def 2;

              then

              reconsider f as FinSequence of s1 by A38, FINSEQ_1:def 4;

              reconsider f as FinSequence of RelStr (# s1, (the InternalRel of C |_2 s1) #);

              

               A41: f is one-to-one by A38, A40, PRE_POLY: 10;

              

               A42: ( dom f) = ( Seg (n + 1)) by A38, A39, Th6;

              

               A43: f is Function of ( dom f), s1 by FINSEQ_2: 26;

              then f is Function of ( Seg (n + 1)), the carrier of C by A42, FUNCT_2: 7;

              then

              reconsider z1 = z as FinSequence of RelStr (# the carrier of C, the InternalRel of C #) by A33, A35, FINSEQ_2: 32;

              reconsider f as Function of ( Seg (n + 1)), the carrier of C by A42, A43, FUNCT_2: 7;

              

               A44: ( dom (f * y2)) = ( Seg n) by A19, A20, A42, RELAT_1: 27;

              ( rng (f * y2)) c= the carrier of C by FINSEQ_1:def 4;

              then

              reconsider r = ( rng (f * y2)) as Element of ( Fin the carrier of C) by FINSUB_1:def 5;

              ( rng (f * y2)) c= s1 by RELAT_1:def 19;

              then

              reconsider s9 = r as non empty Element of F by A37, A44, Th5, RELAT_1: 42;

              for n1,m1 be Nat st n1 in ( dom z1) & m1 in ( dom z1) & n1 < m1 holds (z1 /. n1) <> (z1 /. m1) & [(z1 /. n1), (z1 /. m1)] in the InternalRel of C

              proof

                let n1,m1 be Nat;

                assume that

                 A45: n1 in ( dom z1) and

                 A46: m1 in ( dom z1) and

                 A47: n1 < m1;

                (y2 . m1) in ( Seg (n + 1)) by A19, A33, A35, A44, A46, FINSEQ_2: 11;

                then

                reconsider ym = (y2 . m1) as Element of NAT ;

                (y2 . n1) in ( Seg (n + 1)) by A19, A33, A35, A44, A45, FINSEQ_2: 11;

                then

                reconsider yn = (y2 . n1) as Element of NAT ;

                

                 A48: yn < ym by A17, A18, A19, A33, A35, A44, A45, A46, A47, SEQM_3:def 1;

                

                 A49: ym in ( rng y2) by A19, A33, A35, A44, A46, FUNCT_1:def 3;

                then

                reconsider fm = (f . ym) as Element of RelStr (# s1, (the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2: 11;

                

                 A50: fm = (f /. ym) by A20, A42, A49, PARTFUN1:def 6;

                (z1 . m1) = fm by A33, A35, A46, FUNCT_1: 12;

                then

                reconsider zm = (z1 . m1) as Element of RelStr (# s1, (the InternalRel of C |_2 s1) #);

                

                 A51: zm = (z1 /. m1) by A46, PARTFUN1:def 6;

                

                 A52: (z1 . m1) = (f . (y2 . m1)) by A33, A35, A46, FUNCT_1: 12;

                

                 A53: (z1 . n1) = (f . (y2 . n1)) by A33, A35, A45, FUNCT_1: 12;

                

                 A54: yn in ( rng y2) by A19, A33, A35, A44, A45, FUNCT_1:def 3;

                then

                reconsider fn = (f . yn) as Element of RelStr (# s1, (the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2: 11;

                (z1 . n1) = fn by A33, A35, A45, FUNCT_1: 12;

                then

                reconsider zn = (z1 . n1) as Element of RelStr (# s1, (the InternalRel of C |_2 s1) #);

                

                 A55: zn = (z1 /. n1) by A45, PARTFUN1:def 6;

                fn = (f /. yn) by A20, A42, A54, PARTFUN1:def 6;

                hence thesis by A20, A38, A40, A42, A53, A52, A48, A54, A49, A50, A55, A51, PRE_POLY:def 2;

              end;

              then

               A56: z1 = ( SgmX (the InternalRel of C,s9)) by A33, A35, PRE_POLY: 9;

              ( len (f * y2)) = n by A20, A21, A42, FINSEQ_2: 29;

              then ( card s9) = n by A27, A41, FINSEQ_4: 62;

              then z in { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = n } by A56;

              hence thesis by A2, A37;

            end;

          end;

          then g9 in ( Funcs ((Sk . (n + 1)),(Sk . n))) by A25, FUNCT_2:def 2;

          hence g9 in (( FuncsSeq Sk) . i) by Def3;

          reconsider y = x as Face of n by A16;

          take n;

          take y;

          thus x = y & i = n;

          let s be Element of (Sk . (n + 1));

          assume s in (Sk . (n + 1));

          then

           A57: ex f be Function st f = s & (g . s) = (f * y1) by A26;

          let A be non empty Element of ( symplexes C) such that

           A58: ( SgmX (the InternalRel of C,A)) = s;

          let g1 be Function;

          assume g1 = g9;

          hence thesis by A58, A57;

        end;

        consider F be ManySortedFunction of NatEmbSeq , ( FuncsSeq Sk) such that

         A59: for i be object st i in NAT holds ex f be Function of ( NatEmbSeq . i), (( FuncsSeq Sk) . i) st f = (F . i) & for x be object st x in ( NatEmbSeq . i) holds X[(f . x), x, i] from MSSUBFAM:sch 1( A15);

        take TriangStr (# Sk, F #);

        thus (the SkeletonSeq of TriangStr (# Sk, F #) . 0 ) = { {} } by A4;

        thus for n be Nat st n > 0 holds (the SkeletonSeq of TriangStr (# Sk, F #) . n) = { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = n } by A2;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then

        consider f1 be Function of ( NatEmbSeq . n), (( FuncsSeq Sk) . n) such that

         A60: f1 = (F . n) and

         A61: for x be object st x in ( NatEmbSeq . n) holds ex m be Nat, y be Face of m st x = y & n = m & for s be Element of (Sk . (m + 1)) st s in (Sk . (m + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds for g1 be Function st g1 = (f1 . x) holds (g1 . s) = (( SgmX (the InternalRel of C,A)) * y) by A59;

        let x be Face of n;

        let s be Element of (the SkeletonSeq of TriangStr (# Sk, F #) . (n + 1));

        assume

         A62: s in (the SkeletonSeq of TriangStr (# Sk, F #) . (n + 1));

        let A be non empty Element of ( symplexes C);

        assume

         A63: ( SgmX (the InternalRel of C,A)) = s;

        

         A64: ex m be Nat, y be Face of m st x = y & n = m & for s be Element of (Sk . (m + 1)) st s in (Sk . (m + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds for g1 be Function st g1 = (f1 . x) holds (g1 . s) = (( SgmX (the InternalRel of C,A)) * y) by A61;

        (f1 . x) in (( FuncsSeq Sk) . n);

        then (f1 . x) in ( Funcs ((Sk . (n + 1)),(Sk . n))) by Def3;

        then

        consider G be Function such that

         A65: (f1 . x) = G and ( dom G) = (Sk . (n + 1)) and ( rng G) c= (Sk . n) by FUNCT_2:def 2;

        ( face (s,x)) = (G . s) by A60, A62, A65, Def7;

        hence thesis by A62, A63, A64, A65;

      end;

      uniqueness

      proof

        let T1,T2 be lower_non-empty strict TriangStr such that

         A66: (the SkeletonSeq of T1 . 0 ) = { {} } and

         A67: for n be Nat st n > 0 holds (the SkeletonSeq of T1 . n) = { ( SgmX (the InternalRel of C,A)) where A be non empty Element of ( symplexes C) : ( card A) = n } and

         A68: for n be Nat, f be Face of n, s be Element of (the SkeletonSeq of T1 . (n + 1)) st s in (the SkeletonSeq of T1 . (n + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds ( face (s,f)) = (( SgmX (the InternalRel of C,A)) * f) and

         A69: (the SkeletonSeq of T2 . 0 ) = { {} } and

         A70: for n be Nat st n > 0 holds (the SkeletonSeq of T2 . n) = { ( SgmX (the InternalRel of C,A)) where A be non empty Element of ( symplexes C) : ( card A) = n } and

         A71: for n be Nat, f be Face of n, s be Element of (the SkeletonSeq of T2 . (n + 1)) st s in (the SkeletonSeq of T2 . (n + 1)) holds for A be non empty Element of ( symplexes C) st ( SgmX (the InternalRel of C,A)) = s holds ( face (s,f)) = (( SgmX (the InternalRel of C,A)) * f);

        

         A72: for x be object st x in NAT holds (the SkeletonSeq of T1 . x) = (the SkeletonSeq of T2 . x)

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Element of NAT ;

          now

            per cases ;

              suppose n = 0 ;

              hence (the SkeletonSeq of T1 . n) = (the SkeletonSeq of T2 . n) by A66, A69;

            end;

              suppose

               A73: n <> 0 ;

              then (the SkeletonSeq of T1 . n) = { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = n } by A67;

              hence (the SkeletonSeq of T1 . n) = (the SkeletonSeq of T2 . n) by A70, A73;

            end;

          end;

          hence thesis;

        end;

        then

         A74: the SkeletonSeq of T1 = the SkeletonSeq of T2;

        now

          let i be object;

          assume i in NAT ;

          then

          reconsider n = i as Element of NAT ;

          reconsider F1n = (the FacesAssign of T1 . n), F2n = (the FacesAssign of T2 . n) as Function of ( NatEmbSeq . n), (( FuncsSeq the SkeletonSeq of T1) . n) by A74, PBOOLE:def 15;

          

           A75: ( dom F2n) = ( NatEmbSeq . n) by FUNCT_2:def 1;

           A76:

          now

            let x be object;

            assume x in ( NatEmbSeq . n);

            then

            reconsider x1 = x as Face of n;

            (F1n . x1) in (( FuncsSeq the SkeletonSeq of T1) . n);

            then (F1n . x1) in ( Funcs ((the SkeletonSeq of T1 . (n + 1)),(the SkeletonSeq of T1 . n))) by Def3;

            then

            consider F1nx be Function such that

             A77: F1nx = (F1n . x1) and

             A78: ( dom F1nx) = (the SkeletonSeq of T1 . (n + 1)) and ( rng F1nx) c= (the SkeletonSeq of T1 . n) by FUNCT_2:def 2;

            (F2n . x1) in (( FuncsSeq the SkeletonSeq of T1) . n);

            then (F2n . x1) in ( Funcs ((the SkeletonSeq of T1 . (n + 1)),(the SkeletonSeq of T1 . n))) by Def3;

            then

            consider F2nx be Function such that

             A79: F2nx = (F2n . x1) and

             A80: ( dom F2nx) = (the SkeletonSeq of T1 . (n + 1)) and ( rng F2nx) c= (the SkeletonSeq of T1 . n) by FUNCT_2:def 2;

            now

              let y be object;

              assume

               A81: y in (the SkeletonSeq of T1 . (n + 1));

              then

              reconsider y1 = y as Symplex of T1, (n + 1);

              

               A82: (F1nx . y1) = ( face (y1,x1)) by A77, A81, Def7;

              reconsider y2 = y as Symplex of T2, (n + 1) by A72, A81;

              

               A83: (F2nx . y2) = ( face (y2,x1)) by A74, A79, A81, Def7;

              y1 in { ( SgmX (the InternalRel of C,s)) where s be non empty Element of ( symplexes C) : ( card s) = (n + 1) } by A67, A81;

              then

              consider A be non empty Element of ( symplexes C) such that

               A84: ( SgmX (the InternalRel of C,A)) = y1 and ( card A) = (n + 1);

              ( face (y1,x1)) = (( SgmX (the InternalRel of C,A)) * x1) by A68, A81, A84;

              hence (F1nx . y) = (F2nx . y) by A71, A74, A81, A82, A83, A84;

            end;

            hence (F1n . x) = (F2n . x) by A77, A78, A79, A80, FUNCT_1: 2;

          end;

          ( dom F1n) = ( NatEmbSeq . n) by FUNCT_2:def 1;

          hence (the FacesAssign of T1 . i) = (the FacesAssign of T2 . i) by A75, A76, FUNCT_1: 2;

        end;

        hence thesis by A74, PBOOLE: 3;

      end;

    end