nomin_2.miz



    begin

    reserve a,b,c,v,v1,x,y for object;

    reserve V,A for set;

    reserve d for TypeSCNominativeData of V, A;

    theorem :: NOMIN_2:1

    

     Th1: {a, b, c} c= A iff a in A & b in A & c in A

    proof

      set X = {a, b, c};

      a in X & b in X & c in X by ENUMSET1:def 1;

      hence {a, b, c} c= A implies a in A & b in A & c in A;

      assume

       A1: a in A & b in A & c in A;

      let x;

      thus thesis by A1, ENUMSET1:def 1;

    end;

    registration

      let a,b,c,d,e,f be object;

      cluster { [a, b], [c, d], [e, f]} -> Relation-like;

      coherence

      proof

        let x;

        assume x in { [a, b], [c, d], [e, f]};

        then x = [a, b] or x = [c, d] or x = [e, f] by ENUMSET1:def 1;

        hence thesis;

      end;

    end

    theorem :: NOMIN_2:2

    

     Th2: for a,b,c,d,e,f be object holds ( dom { [a, b], [c, d], [e, f]}) = {a, c, e}

    proof

      let a,b,c,d,e,f be object;

      

       A1: ( dom { [a, b], [c, d]}) = {a, c} by RELAT_1: 10;

      

       A2: ( dom { [e, f]}) = {e} by RELAT_1: 9;

       { [a, b], [c, d], [e, f]} = ( { [a, b], [c, d]} \/ { [e, f]}) by ENUMSET1: 3;

      

      hence ( dom { [a, b], [c, d], [e, f]}) = (( dom { [a, b], [c, d]}) \/ ( dom { [e, f]})) by XTUPLE_0: 23

      .= {a, c, e} by A1, A2, ENUMSET1: 3;

    end;

    theorem :: NOMIN_2:3

    

     Th3: for a,b,c,d,e,f be object holds ( rng { [a, b], [c, d], [e, f]}) = {b, d, f}

    proof

      let a,b,c,d,e,f be object;

      

       A1: ( rng { [a, b], [c, d]}) = {b, d} by RELAT_1: 10;

      

       A2: ( rng { [e, f]}) = {f} by RELAT_1: 9;

       { [a, b], [c, d], [e, f]} = ( { [a, b], [c, d]} \/ { [e, f]}) by ENUMSET1: 3;

      

      hence ( rng { [a, b], [c, d], [e, f]}) = (( rng { [a, b], [c, d]}) \/ ( rng { [e, f]})) by XTUPLE_0: 27

      .= {b, d, f} by A1, A2, ENUMSET1: 3;

    end;

    registration

      let V;

      cluster one-to-oneV -valued for FinSequence;

      existence

      proof

        per cases ;

          suppose V is empty;

          take ( <*> V);

          thus thesis;

        end;

          suppose V is non empty;

          then

          reconsider V as non empty set;

          take <* the Element of V*>;

          thus thesis;

        end;

      end;

    end

    theorem :: NOMIN_2:4

    

     Th4: ( dom <*a, b, c*>) = {1, 2, 3}

    proof

      

      thus ( dom <*a, b, c*>) = ( Seg ( len <*a, b, c*>)) by FINSEQ_1:def 3

      .= {1, 2, 3} by FINSEQ_1: 45, FINSEQ_3: 1;

    end;

    registration

      let V, A;

      cluster ( NDSS (V,A)) -> non with_non-empty_elements;

      coherence by NOMIN_1: 6;

      cluster ( ND (V,A)) -> non with_non-empty_elements;

      coherence by NOMIN_1: 38;

    end

    theorem :: NOMIN_2:5

    

     Th5: v in V implies { [v, d]} is NonatomicND of V, A

    proof

      assume v in V;

      

      then ( naming (V,A,v,d)) = (v .--> d) by NOMIN_1:def 13

      .= { [v, d]} by ZFMISC_1: 29;

      hence thesis;

    end;

    theorem :: NOMIN_2:6

    

     Th6: for D be finite Function st ( dom D) c= V & ( rng D) c= ( ND (V,A)) holds D is NonatomicND of V, A

    proof

      let D be finite Function such that

       A1: ( dom D) c= V and

       A2: ( rng D) c= ( ND (V,A));

      defpred P[ set] means $1 is NonatomicND of V, A;

      

       A3: D is finite;

      

       A4: P[ {} ] by NOMIN_1: 30;

      

       A5: for x,B be set st x in D & B c= D & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A6: x in D and

         A7: B c= D;

        assume P[B];

        then

        reconsider B as NonatomicND of V, A;

        consider a, b such that

         A8: x = [a, b] by A6, RELAT_1:def 1;

        

         A9: a in ( dom D) by A6, A8, XTUPLE_0:def 12;

        b in ( rng D) by A6, A8, XTUPLE_0:def 13;

        then b is TypeSCNominativeData of V, A by A2, NOMIN_1: 39;

        then

         A10: { [a, b]} is NonatomicND of V, A by A1, A9, Th5;

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

        then (B \/ { [a, b]}) is Function by A7, A8, GRFUNC_1: 14;

        hence thesis by A8, A10, NOMIN_1: 36, PARTFUN1: 51;

      end;

       P[D] from FINSET_1:sch 2( A3, A4, A5);

      hence thesis;

    end;

    theorem :: NOMIN_2:7

    for d1,d2 be TypeSCNominativeData of V, A holds d2 c= ( global_overlapping (V,A,d1,d2))

    proof

      let d1,d2 be TypeSCNominativeData of V, A;

      per cases ;

        suppose not d1 in A & not d2 in A;

        then ex f1,f2 be Function st f1 = d1 & f2 = d2 & ( global_overlapping (V,A,d1,d2)) = (f2 \/ (f1 | (( dom f1) \ ( dom f2)))) by NOMIN_1:def 16;

        hence thesis by XBOOLE_1: 7;

      end;

        suppose d1 in A or d2 in A;

        hence thesis by NOMIN_1:def 16;

      end;

    end;

    theorem :: NOMIN_2:8

    for d be NonatomicND of V, A holds d is TypeSCNominativeData of V, A;

    theorem :: NOMIN_2:9

    

     Th9: for d1,d2 be NonatomicND of V, A holds ( global_overlapping (V,A,d1,d2)) is NonatomicND of V, A

    proof

      let d1,d2 be NonatomicND of V, A;

      per cases ;

        suppose not d1 in A & not d2 in A;

        then

         A1: ( global_overlapping (V,A,d1,d2)) = (d2 \/ (d1 | (( dom d1) \ ( dom d2)))) by NOMIN_1: 64;

        (d1 | (( dom d1) \ ( dom d2))) is NonatomicND of V, A by NOMIN_1: 32, RELAT_1: 59;

        hence thesis by A1, NOMIN_1: 36, PARTFUN1: 51;

      end;

        suppose d1 in A or d2 in A;

        hence thesis by NOMIN_1:def 16;

      end;

    end;

    registration

      let V, A;

      let d1,d2 be NonatomicND of V, A;

      cluster ( global_overlapping (V,A,d1,d2)) -> Function-like Relation-like;

      coherence by Th9;

    end

    registration

      let V, A, v;

      let d1 be NonatomicND of V, A;

      let d2 be object;

      cluster ( local_overlapping (V,A,d1,d2,v)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: NOMIN_2:10

    

     Th10: v in V implies for d1,d2 be TypeSCNominativeData of V, A holds for L be Function st L = ( local_overlapping (V,A,d1,d2,v)) holds (L . v) = d2

    proof

      assume

       A1: v in V;

      let d1,d2 be TypeSCNominativeData of V, A;

      let L be Function such that

       A2: L = ( local_overlapping (V,A,d1,d2,v));

      

       A4: ( naming (V,A,v,d2)) = (v .--> d2) by A1, NOMIN_1:def 13;

      

       A6: v in {v} by TARSKI:def 1;

      

       A7: ((v .--> d2) . v) = d2 by FUNCOP_1: 72;

      per cases ;

        suppose not d1 in A & not ( naming (V,A,v,d2)) in A;

        then

        consider f1,f2 be Function such that f1 = d1 and

         A8: f2 = ( naming (V,A,v,d2)) and

         A9: L = (f2 \/ (f1 | (( dom f1) \ ( dom f2)))) by A2, NOMIN_1:def 16;

        

        thus (L . v) = (f2 . v) by A4, A6, A8, A9, GRFUNC_1: 15

        .= d2 by A8, A4, A6, FUNCOP_1: 7;

      end;

        suppose d1 in A or ( naming (V,A,v,d2)) in A;

        hence thesis by A4, A7, A2, NOMIN_1:def 16;

      end;

    end;

    theorem :: NOMIN_2:11

    for d1 be NonatomicND of V, A, z be Element of V holds V is non empty & v in ( dom d1) & d = (( denaming (V,A,v)) . d1) implies (( local_overlapping (V,A,d1,d,z)) . z) = (d1 . v)

    proof

      let d1 be NonatomicND of V, A, z be Element of V;

      assume

       A1: V is non empty;

      set Dj = ( denaming (V,A,v));

      assume that

       A2: v in ( dom d1) and

       A3: d = (Dj . d1);

      ( dom Dj) = { d where d be NonatomicND of V, A : v in ( dom d) } by NOMIN_1:def 18;

      then

       A4: d1 in ( dom Dj) by A2;

      

      thus (( local_overlapping (V,A,d1,d,z)) . z) = (Dj . d1) by A1, A3, Th10

      .= ( denaming (v,d1)) by A4, NOMIN_1:def 18

      .= (d1 . v) by A2, NOMIN_1:def 12;

    end;

    theorem :: NOMIN_2:12

    v in V & v <> v1 implies for d1 be NonatomicND of V, A holds for d2 be TypeSCNominativeData of V, A st v1 in ( dom d1) & not d1 in A & not ( naming (V,A,v,d2)) in A holds (( local_overlapping (V,A,d1,d2,v)) . v1) = (d1 . v1)

    proof

      assume that

       A1: v in V and

       A2: v <> v1;

      let d1 be NonatomicND of V, A;

      let d2 be TypeSCNominativeData of V, A such that

       A4: v1 in ( dom d1) and

       A5: not d1 in A & not ( naming (V,A,v,d2)) in A;

      

       A7: ( naming (V,A,v,d2)) = (v .--> d2) by A1, NOMIN_1:def 13;

      consider f1,f2 be Function such that

       A10: f1 = d1 and

       A11: f2 = ( naming (V,A,v,d2)) and

       A12: ( local_overlapping (V,A,d1,d2,v)) = (f2 \/ (f1 | (( dom f1) \ ( dom f2)))) by A5, NOMIN_1:def 16;

       not v1 in {v} by A2, TARSKI:def 1;

      then v1 in (( dom f1) \ ( dom f2)) by A4, A7, A10, A11, XBOOLE_0:def 5;

      then

       A13: v1 in ( dom (f1 | (( dom f1) \ ( dom f2)))) by RELAT_1: 57;

      

      hence (( local_overlapping (V,A,d1,d2,v)) . v1) = ((f1 | (( dom f1) \ ( dom f2))) . v1) by A12, GRFUNC_1: 15

      .= (d1 . v1) by A10, A13, FUNCT_1: 47;

    end;

    theorem :: NOMIN_2:13

    

     Th12: for d1 be NonatomicND of V, A holds for d2 be TypeSCNominativeData of V, A st v in V & not v in ( dom d1) & not d1 in A & not ( naming (V,A,v,d2)) in A holds ( dom ( local_overlapping (V,A,d1,d2,v))) = ( {v} \/ ( dom d1))

    proof

      let d1 be NonatomicND of V, A;

      let d2 be TypeSCNominativeData of V, A such that

       A1: v in V and

       A2: not v in ( dom d1) and

       A3: not d1 in A & not ( naming (V,A,v,d2)) in A;

      set n = ( naming (V,A,v,d2));

      

       A4: n = (v .--> d2) by A1, NOMIN_1:def 13;

      

       A5: ( dom (d1 | (( dom d1) \ ( dom n)))) = ( dom d1)

      proof

        thus ( dom (d1 | (( dom d1) \ ( dom n)))) c= ( dom d1) by RELAT_1: 60;

        ( dom d1) c= (( dom d1) \ ( dom n)) by A2, A4, ZFMISC_1: 34;

        hence thesis by RELAT_1: 62;

      end;

      ( local_overlapping (V,A,d1,d2,v)) = (n \/ (d1 | (( dom d1) \ ( dom n)))) by A3, NOMIN_1: 64;

      hence thesis by A4, A5, XTUPLE_0: 23;

    end;

    theorem :: NOMIN_2:14

    

     Th13: for d1 be NonatomicND of V, A holds for d2 be TypeSCNominativeData of V, A st v in V & v in ( dom d1) & not d1 in A & not ( naming (V,A,v,d2)) in A holds ( dom ( local_overlapping (V,A,d1,d2,v))) = ( dom d1)

    proof

      let d1 be NonatomicND of V, A;

      let d2 be TypeSCNominativeData of V, A such that

       A1: v in V and

       A2: v in ( dom d1) and

       A3: not d1 in A & not ( naming (V,A,v,d2)) in A;

      set n = ( naming (V,A,v,d2));

      

       A4: n = (v .--> d2) by A1, NOMIN_1:def 13;

      

       A5: (( dom n) \/ ( dom (d1 | (( dom d1) \ ( dom n))))) = ( dom d1)

      proof

        

         A6: ( dom n) c= ( dom d1) by A2, A4, ZFMISC_1: 31;

        ( dom (d1 | (( dom d1) \ ( dom n)))) c= ( dom d1) by RELAT_1: 60;

        hence (( dom n) \/ ( dom (d1 | (( dom d1) \ ( dom n))))) c= ( dom d1) by A6, XBOOLE_1: 8;

        let x be object;

        assume

         A7: x in ( dom d1);

        per cases ;

          suppose x = v;

          then x in ( dom n) by A4, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose x <> v;

          then not x in ( dom n) by A4, TARSKI:def 1;

          then x in (( dom d1) \ ( dom n)) by A7, XBOOLE_0:def 5;

          then x in ( dom (d1 | (( dom d1) \ ( dom n)))) by RELAT_1: 57;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ( local_overlapping (V,A,d1,d2,v)) = (n \/ (d1 | (( dom d1) \ ( dom n)))) by A3, NOMIN_1: 64;

      hence thesis by A5, XTUPLE_0: 23;

    end;

    theorem :: NOMIN_2:15

    

     Th14: for d1 be NonatomicND of V, A holds for d2 be TypeSCNominativeData of V, A st v in V & not d1 in A & not ( naming (V,A,v,d2)) in A holds ( dom ( local_overlapping (V,A,d1,d2,v))) = ( {v} \/ ( dom d1))

    proof

      let d1 be NonatomicND of V, A;

      let d2 be TypeSCNominativeData of V, A such that

       A1: v in V & not d1 in A & not ( naming (V,A,v,d2)) in A;

      per cases ;

        suppose

         A2: v in ( dom d1);

        then ( dom ( local_overlapping (V,A,d1,d2,v))) = ( dom d1) by A1, Th13;

        hence thesis by A2, ZFMISC_1: 40;

      end;

        suppose not v in ( dom d1);

        hence thesis by A1, Th12;

      end;

    end;

    definition

      let V, A;

      mode SCPartialNominativePredicate of V,A is PartialPredicate of ( ND (V,A));

    end

    reserve p,q,r for SCPartialNominativePredicate of V, A;

    theorem :: NOMIN_2:16

    

     Th15: ( dom ( PP_or (p,q))) = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE }

    proof

      set X = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE };

      set Y = { d where d be Element of ( ND (V,A)) : d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE };

      X = Y

      proof

        thus X c= Y

        proof

          let x;

          assume x in X;

          then ex d be TypeSCNominativeData of V, A st d = x & (d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE );

          hence thesis;

        end;

        let x;

        assume x in Y;

        then

        consider d be Element of ( ND (V,A)) such that

         A1: d = x & (d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE );

        d is TypeSCNominativeData of V, A by NOMIN_1: 39;

        hence thesis by A1;

      end;

      hence thesis by PARTPR_1:def 4;

    end;

    theorem :: NOMIN_2:17

    ( dom ( PP_and (p,q))) = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = FALSE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = TRUE }

    proof

      set F = ( PP_and (p,q));

      set P = ( PP_not p);

      set Q = ( PP_not q);

      set D = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = FALSE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = TRUE };

      

       A1: ( dom F) = ( dom ( PP_or (P,Q))) by PARTPR_1:def 2;

      

       A2: ( dom ( PP_or (P,Q))) = { d where d be TypeSCNominativeData of V, A : d in ( dom P) & (P . d) = TRUE or d in ( dom Q) & (Q . d) = TRUE or d in ( dom P) & (P . d) = FALSE & d in ( dom Q) & (Q . d) = FALSE } by Th15;

      

       A3: ( dom P) = ( dom p) by PARTPR_1:def 2;

      

       A4: ( dom Q) = ( dom q) by PARTPR_1:def 2;

      thus ( dom F) c= D

      proof

        let x;

        assume x in ( dom F);

        then

        consider d be TypeSCNominativeData of V, A such that

         A5: x = d and

         A6: d in ( dom P) & (P . d) = TRUE or d in ( dom Q) & (Q . d) = TRUE or d in ( dom P) & (P . d) = FALSE & d in ( dom Q) & (Q . d) = FALSE by A1, A2;

        per cases by A6;

          suppose that

           A7: d in ( dom P) and

           A8: (P . d) = TRUE ;

          (p . d) = FALSE by A3, A7, A8, PARTPR_1: 5;

          hence thesis by A3, A5, A7;

        end;

          suppose that

           A9: d in ( dom Q) and

           A10: (Q . d) = TRUE ;

          (q . d) = FALSE by A4, A9, A10, PARTPR_1: 5;

          hence thesis by A4, A5, A9;

        end;

          suppose that

           A11: d in ( dom P) & d in ( dom Q) and

           A12: (P . d) = FALSE & (Q . d) = FALSE ;

          (p . d) = TRUE & (q . d) = TRUE by A3, A4, A11, A12, PARTPR_1: 4;

          hence thesis by A3, A4, A5, A11;

        end;

      end;

      let x;

      assume x in D;

      then

      consider d be TypeSCNominativeData of V, A such that

       A13: x = d and

       A14: d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = FALSE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = TRUE ;

      per cases by A14;

        suppose that

         A15: d in ( dom p) and

         A16: (p . d) = FALSE ;

        (P . d) = TRUE by A15, A16, PARTPR_1:def 2;

        hence thesis by A1, A2, A3, A13, A15;

      end;

        suppose that

         A17: d in ( dom q) and

         A18: (q . d) = FALSE ;

        (Q . d) = TRUE by A17, A18, PARTPR_1:def 2;

        hence thesis by A1, A2, A4, A13, A17;

      end;

        suppose that

         A19: d in ( dom p) & d in ( dom q) and

         A20: (p . d) = TRUE & (q . d) = TRUE ;

        (P . d) = FALSE & (Q . d) = FALSE by A19, A20, PARTPR_1:def 2;

        hence thesis by A1, A2, A3, A4, A13, A19;

      end;

    end;

    theorem :: NOMIN_2:18

    ( dom ( PP_imp (p,q))) = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = FALSE }

    proof

      set F = ( PP_imp (p,q));

      set P = ( PP_not p);

      set D = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = FALSE };

      

       A1: ( dom F) = { d where d be Element of ( ND (V,A)) : d in ( dom P) & (P . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom P) & (P . d) = FALSE & d in ( dom q) & (q . d) = FALSE } by PARTPR_1:def 4;

      

       A2: ( dom P) = ( dom p) by PARTPR_1:def 2;

      thus ( dom F) c= D

      proof

        let x;

        assume x in ( dom F);

        then

        consider d be Element of ( ND (V,A)) such that

         A3: x = d and

         A4: d in ( dom P) & (P . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom P) & (P . d) = FALSE & d in ( dom q) & (q . d) = FALSE by A1;

        reconsider d as TypeSCNominativeData of V, A by NOMIN_1: 39;

        per cases by A4;

          suppose that

           A5: d in ( dom P) and

           A6: (P . d) = TRUE ;

          (p . d) = FALSE by A2, A5, A6, PARTPR_1: 5;

          hence thesis by A2, A3, A5;

        end;

          suppose d in ( dom q) & (q . d) = TRUE ;

          hence thesis by A3;

        end;

          suppose that

           A7: d in ( dom P) & d in ( dom q) and

           A8: (P . d) = FALSE and

           A9: (q . d) = FALSE ;

          (p . d) = TRUE by A2, A7, A8, PARTPR_1: 4;

          hence thesis by A2, A3, A7, A9;

        end;

      end;

      let x;

      assume x in D;

      then

      consider d be TypeSCNominativeData of V, A such that

       A10: x = d and

       A11: d in ( dom p) & (p . d) = FALSE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = TRUE & d in ( dom q) & (q . d) = FALSE ;

      per cases by A11;

        suppose that

         A12: d in ( dom p) and

         A13: (p . d) = FALSE ;

        (P . d) = TRUE by A12, A13, PARTPR_1:def 2;

        hence thesis by A1, A2, A10, A12;

      end;

        suppose d in ( dom q) & (q . d) = TRUE ;

        hence thesis by A1, A10;

      end;

        suppose that

         A14: d in ( dom p) and

         A15: d in ( dom q) and

         A16: (p . d) = TRUE and

         A17: (q . d) = FALSE ;

        (P . d) = FALSE by A14, A16, PARTPR_1:def 2;

        hence thesis by A1, A2, A10, A14, A15, A17;

      end;

    end;

    definition

      let V, A, v;

      defpred D1[ object, Function] means ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,$1,d1,v)) in ( dom $2) & ($2 . ( local_overlapping (V,A,$1,d1,v))) = TRUE ;

      defpred D2[ object, Function] means for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,$1,d1,v)) in ( dom $2) & ($2 . ( local_overlapping (V,A,$1,d1,v))) = FALSE ;

      deffunc D( Function) = { d where d be TypeSCNominativeData of V, A : D1[d, $1] or D2[d, $1] };

      :: NOMIN_2:def1

      func SCexists (V,A,v) -> Function of ( Pr ( ND (V,A))), ( Pr ( ND (V,A))) means

      : Def1: for p be SCPartialNominativePredicate of V, A holds ( dom (it . p)) = { d where d be TypeSCNominativeData of V, A : (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = FALSE ) } & for d be TypeSCNominativeData of V, A holds ((ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = TRUE ) implies ((it . p) . d) = TRUE ) & ((for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = FALSE ) implies ((it . p) . d) = FALSE );

      existence

      proof

        defpred P[ object, object] means for p be SCPartialNominativePredicate of V, A st p = $1 holds for f be Function st f = $2 holds ( dom f) = D(p) & for d be TypeSCNominativeData of V, A holds ( D1[d, p] implies (f . d) = TRUE ) & ( D2[d, p] implies (f . d) = FALSE );

        

         A1: for x be object st x in ( Pr ( ND (V,A))) holds ex y be object st y in ( Pr ( ND (V,A))) & P[x, y]

        proof

          let x;

          assume x in ( Pr ( ND (V,A)));

          then

          reconsider X = x as PartFunc of ( ND (V,A)), BOOLEAN by PARTFUN1: 46;

          defpred Q[ object, object] means for d be TypeSCNominativeData of V, A st d = $1 holds ( D1[d, X] implies $2 = TRUE ) & ( D2[d, X] implies $2 = FALSE );

          

           A2: for a be object st a in D(X) holds ex b be object st b in BOOLEAN & Q[a, b]

          proof

            let a be object;

            assume a in D(X);

            then

            consider d be TypeSCNominativeData of V, A such that

             A3: a = d and

             A4: D1[d, X] or D2[d, X];

            per cases by A4;

              suppose

               A5: D1[d, X];

              take TRUE ;

              thus thesis by A3, A5;

            end;

              suppose

               A6: D2[d, X];

              take FALSE ;

              thus thesis by A3, A6;

            end;

          end;

          consider g be Function such that

           A7: ( dom g) = D(X) and

           A8: ( rng g) c= BOOLEAN and

           A9: for x be object st x in D(X) holds Q[x, (g . x)] from FUNCT_1:sch 6( A2);

          take g;

           D(X) c= ( ND (V,A))

          proof

            let x;

            assume x in D(X);

            then ex d be TypeSCNominativeData of V, A st d = x & ( D1[d, X] or D2[d, X]);

            hence thesis;

          end;

          then g is PartFunc of ( ND (V,A)), BOOLEAN by A7, A8, RELSET_1: 4;

          hence g in ( Pr ( ND (V,A))) by PARTFUN1: 45;

          let p be SCPartialNominativePredicate of V, A such that

           A10: p = x;

          let f be Function such that

           A11: f = g;

          thus ( dom f) = D(p) by A7, A10, A11;

          let d be TypeSCNominativeData of V, A;

          hereby

            assume

             A12: D1[d, p];

            then d in D(X) by A10;

            hence (f . d) = TRUE by A9, A10, A11, A12;

          end;

          assume

           A13: D2[d, p];

          then d in D(X) by A10;

          hence thesis by A9, A10, A11, A13;

        end;

        consider F be Function of ( Pr ( ND (V,A))), ( Pr ( ND (V,A))) such that

         A14: for x be object st x in ( Pr ( ND (V,A))) holds P[x, (F . x)] from FUNCT_2:sch 1( A1);

        take F;

        let p be SCPartialNominativePredicate of V, A;

        p in ( Pr ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by A14;

      end;

      uniqueness

      proof

        let f,g be Function of ( Pr ( ND (V,A))), ( Pr ( ND (V,A))) such that

         A15: for p be SCPartialNominativePredicate of V, A holds ( dom (f . p)) = D(p) & for d be TypeSCNominativeData of V, A holds ( D1[d, p] implies ((f . p) . d) = TRUE ) & ( D2[d, p] implies ((f . p) . d) = FALSE ) and

         A16: for p be SCPartialNominativePredicate of V, A holds ( dom (g . p)) = D(p) & for d be TypeSCNominativeData of V, A holds ( D1[d, p] implies ((g . p) . d) = TRUE ) & ( D2[d, p] implies ((g . p) . d) = FALSE );

        let x be Element of ( Pr ( ND (V,A)));

        reconsider p = x as SCPartialNominativePredicate of V, A by PARTFUN1: 46;

        

         A17: ( dom (f . x)) = D(p) by A15;

        hence ( dom (f . x)) = ( dom (g . x)) by A16;

        let a be object;

        assume a in ( dom (f . x));

        then

        consider d be TypeSCNominativeData of V, A such that

         A18: a = d and

         A19: D1[d, p] or D2[d, p] by A17;

        per cases by A19;

          suppose

           A20: D1[d, p];

          

          thus ((f . x) . a) = TRUE by A15, A18, A20

          .= ((g . x) . a) by A16, A18, A20;

        end;

          suppose

           A21: D2[d, p];

          

          thus ((f . x) . a) = FALSE by A15, A18, A21

          .= ((g . x) . a) by A16, A18, A21;

        end;

      end;

    end

    definition

      let V, A, v, p;

      :: NOMIN_2:def2

      func SC_exists (p,v) -> SCPartialNominativePredicate of V, A equals (( SCexists (V,A,v)) . p);

      coherence

      proof

        p in ( Pr ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, FUNCT_2: 5;

      end;

    end

    theorem :: NOMIN_2:19

    

     Th18: x in ( dom ( SC_exists (p,v))) implies (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = FALSE )

    proof

      assume

       A1: x in ( dom ( SC_exists (p,v)));

      ( dom ( SC_exists (p,v))) = { d where d be TypeSCNominativeData of V, A : (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = FALSE ) } by Def1;

      then ex d2 be TypeSCNominativeData of V, A st x = d2 & ((ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d2,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d2,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d2,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d2,d1,v))) = FALSE )) by A1;

      hence thesis;

    end;

    theorem :: NOMIN_2:20

    ( SC_exists (( PP_BottomPred ( ND (V,A))),v)) = ( PP_BottomPred ( ND (V,A)))

    proof

      set B = ( PP_BottomPred ( ND (V,A)));

      set T = ( PP_True ( ND (V,A)));

      set o = ( SC_exists (B,v));

      thus ( dom o) = ( dom B)

      proof

        thus ( dom o) c= ( dom B)

        proof

          let x;

          assume x in ( dom o);

          then (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom B) & (B . ( local_overlapping (V,A,x,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom B) & (B . ( local_overlapping (V,A,x,d1,v))) = FALSE ) by Th18;

          hence thesis;

        end;

        thus ( dom B) c= ( dom o);

      end;

      let x;

      assume x in ( dom o);

      then (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom B) & (B . ( local_overlapping (V,A,x,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom B) & (B . ( local_overlapping (V,A,x,d1,v))) = FALSE ) by Th18;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: NOMIN_2:21

    ( SC_exists (( PP_or (p,q)),v)) = ( PP_or (( SC_exists (p,v)),( SC_exists (q,v))))

    proof

      set a = ( PP_or (p,q));

      set f = ( SC_exists (a,v));

      set g = ( SC_exists (p,v));

      set h = ( SC_exists (q,v));

      set b = ( PP_or (g,h));

      

       A1: ( dom a) = { d where d be TypeSCNominativeData of V, A : d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE } by Th15;

      

       A2: ( dom b) = { d where d be TypeSCNominativeData of V, A : d in ( dom g) & (g . d) = TRUE or d in ( dom h) & (h . d) = TRUE or d in ( dom g) & (g . d) = FALSE & d in ( dom h) & (h . d) = FALSE } by Th15;

      

       A3: ( dom f) = { d where d be TypeSCNominativeData of V, A : (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,d,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,d,d1,v))) = FALSE ) } by Def1;

      

       A4: ( dom g) = { d where d be TypeSCNominativeData of V, A : (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,d,d1,v))) = FALSE ) } by Def1;

      

       A5: ( dom h) = { d where d be TypeSCNominativeData of V, A : (ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,d,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,d,d1,v))) = TRUE ) or (for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,d,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,d,d1,v))) = FALSE ) } by Def1;

      thus ( dom f) = ( dom b)

      proof

        thus ( dom f) c= ( dom b)

        proof

          let x;

          assume

           A6: x in ( dom f);

          then

           A7: x is TypeSCNominativeData of V, A by NOMIN_1: 39;

          per cases by A6, Th18;

            suppose ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            then

            consider d1 be TypeSCNominativeData of V, A such that

             A8: ( local_overlapping (V,A,x,d1,v)) in ( dom a) and

             A9: (a . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            set L = ( local_overlapping (V,A,x,d1,v));

            per cases by A8, PARTPR_1: 8;

              suppose

               A10: L in ( dom p) & (p . L) = TRUE ;

              then

               A11: x in ( dom g) by A7, A4;

              (g . x) = TRUE by A7, A10, Def1;

              hence thesis by A2, A7, A11;

            end;

              suppose

               A12: L in ( dom q) & (q . L) = TRUE ;

              then

               A13: x in ( dom h) by A7, A5;

              (h . x) = TRUE by A7, A12, Def1;

              hence thesis by A2, A7, A13;

            end;

              suppose L in ( dom p) & (p . L) = FALSE & L in ( dom q) & (q . L) = FALSE ;

              hence thesis by A9, PARTPR_1: 9;

            end;

          end;

            suppose

             A14: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,x,d1,v))) = FALSE ;

            

             A15: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = FALSE

            proof

              let d1 be TypeSCNominativeData of V, A;

              set O = ( local_overlapping (V,A,x,d1,v));

              O in ( dom a) & (a . O) = FALSE by A14;

              hence thesis by PARTPR_1: 13;

            end;

            then

             A16: x in ( dom g) by A7, A4;

            

             A17: (g . x) = FALSE by A7, A15, Def1;

            

             A18: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,x,d1,v))) = FALSE

            proof

              let d1 be TypeSCNominativeData of V, A;

              set O = ( local_overlapping (V,A,x,d1,v));

              O in ( dom a) & (a . O) = FALSE by A14;

              hence thesis by PARTPR_1: 13;

            end;

            then

             A19: x in ( dom h) by A7, A5;

            (h . x) = FALSE by A7, A18, Def1;

            hence thesis by A2, A7, A16, A17, A19;

          end;

        end;

        let x;

        assume

         A20: x in ( dom b);

        then

         A21: x is TypeSCNominativeData of V, A by NOMIN_1: 39;

        per cases by A20, PARTPR_1: 8;

          suppose that

           A22: x in ( dom g) and

           A23: (g . x) = TRUE ;

          per cases by A22, Th18;

            suppose ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            then

            consider d1 be TypeSCNominativeData of V, A such that

             A24: ( local_overlapping (V,A,x,d1,v)) in ( dom p) and

             A25: (p . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            set L = ( local_overlapping (V,A,x,d1,v));

            L in ( dom a) & (a . L) = TRUE by A1, A24, A25, PARTPR_1:def 4;

            hence thesis by A3, A21;

          end;

            suppose for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = FALSE ;

            hence thesis by A21, A23, Def1;

          end;

        end;

          suppose that

           A26: x in ( dom h) and

           A27: (h . x) = TRUE ;

          per cases by A26, Th18;

            suppose ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            then

            consider d1 be TypeSCNominativeData of V, A such that

             A28: ( local_overlapping (V,A,x,d1,v)) in ( dom q) and

             A29: (q . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

            set L = ( local_overlapping (V,A,x,d1,v));

            L in ( dom a) & (a . L) = TRUE by A1, A28, A29, PARTPR_1:def 4;

            hence thesis by A3, A21;

          end;

            suppose for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,x,d1,v))) = FALSE ;

            hence thesis by A21, A27, Def1;

          end;

        end;

          suppose that

           A30: x in ( dom g) and

           A31: (g . x) = FALSE and

           A32: x in ( dom h) and

           A33: (h . x) = FALSE ;

          for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,x,d1,v))) = FALSE

          proof

            let d1 be TypeSCNominativeData of V, A;

            

             A34: not ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = TRUE by A21, A31, Def1;

            

             A35: not ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,x,d1,v))) = TRUE by A21, A33, Def1;

            set L = ( local_overlapping (V,A,x,d1,v));

            L in ( dom p) & (p . L) = FALSE & L in ( dom q) & (q . L) = FALSE by A34, A35, A30, A32, Th18;

            hence L in ( dom a) & (a . L) = FALSE by A1, PARTPR_1:def 4;

          end;

          hence thesis by A3, A21;

        end;

      end;

      let x;

      assume

       A36: x in ( dom f);

      then

       A37: x is TypeSCNominativeData of V, A by NOMIN_1: 39;

      per cases by A36, Th18;

        suppose ex d1 be TypeSCNominativeData of V, A st ( local_overlapping (V,A,x,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

        then

        consider d1 be TypeSCNominativeData of V, A such that

         A38: ( local_overlapping (V,A,x,d1,v)) in ( dom a) and

         A39: (a . ( local_overlapping (V,A,x,d1,v))) = TRUE ;

        set L = ( local_overlapping (V,A,x,d1,v));

        per cases by A38, PARTPR_1: 8;

          suppose

           A40: L in ( dom p) & (p . L) = TRUE ;

          then

           A41: x in ( dom g) by A37, A4;

          (g . x) = TRUE by A37, A40, Def1;

          

          hence (b . x) = TRUE by A41, PARTPR_1:def 4

          .= (f . x) by A38, A39, A37, Def1;

        end;

          suppose

           A42: L in ( dom q) & (q . L) = TRUE ;

          then

           A43: x in ( dom h) by A37, A5;

          (h . x) = TRUE by A37, A42, Def1;

          

          hence (b . x) = TRUE by A43, PARTPR_1:def 4

          .= (f . x) by A38, A39, A37, Def1;

        end;

          suppose L in ( dom p) & (p . L) = FALSE & L in ( dom q) & (q . L) = FALSE ;

          hence thesis by A39, PARTPR_1: 9;

        end;

      end;

        suppose

         A44: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom a) & (a . ( local_overlapping (V,A,x,d1,v))) = FALSE ;

        

         A45: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom p) & (p . ( local_overlapping (V,A,x,d1,v))) = FALSE

        proof

          let d1 be TypeSCNominativeData of V, A;

          set O = ( local_overlapping (V,A,x,d1,v));

          O in ( dom a) & (a . O) = FALSE by A44;

          hence thesis by PARTPR_1: 13;

        end;

        then

         A46: x in ( dom g) by A37, A4;

        

         A47: (g . x) = FALSE by A37, A45, Def1;

        

         A48: for d1 be TypeSCNominativeData of V, A holds ( local_overlapping (V,A,x,d1,v)) in ( dom q) & (q . ( local_overlapping (V,A,x,d1,v))) = FALSE

        proof

          let d1 be TypeSCNominativeData of V, A;

          set O = ( local_overlapping (V,A,x,d1,v));

          O in ( dom a) & (a . O) = FALSE by A44;

          hence thesis by PARTPR_1: 13;

        end;

        then

         A49: x in ( dom h) by A37, A5;

        (h . x) = FALSE by A37, A48, Def1;

        

        hence (b . x) = FALSE by A46, A47, A49, PARTPR_1:def 4

        .= (f . x) by A44, A37, Def1;

      end;

    end;

    begin

    reserve n for Nat;

    reserve X for Function;

    definition

      let F be Function-yielding Function;

      let d be object;

      :: NOMIN_2:def3

      pred d in_doms F means

      : Def3: for x be object st x in ( dom F) holds d in ( dom (F . x));

    end

    definition

      let g be Function-yielding Function;

      let X be Function;

      let d be object;

      :: NOMIN_2:def4

      func NDdataSeq (g,X,d) -> Function means

      : Def4: ( dom it ) = ( dom X) & for x st x in ( dom X) holds (it . x) = [(X . x), ((g . x) . d)];

      existence

      proof

        deffunc F( object) = [(X . $1), ((g . $1) . d)];

        consider p be Function such that

         A1: ( dom p) = ( dom X) & for x st x in ( dom X) holds (p . x) = F(x) from FUNCT_1:sch 3;

        take p;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function such that

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

         A3: for x st x in ( dom X) holds (F . x) = [(X . x), ((g . x) . d)] and

         A4: ( dom G) = ( dom X) and

         A5: for x st x in ( dom X) holds (G . x) = [(X . x), ((g . x) . d)];

        thus ( dom F) = ( dom G) by A2, A4;

        let x;

        assume

         A6: x in ( dom F);

        

        hence (F . x) = [(X . x), ((g . x) . d)] by A2, A3

        .= (G . x) by A2, A5, A6;

      end;

    end

    registration

      let g be Function-yielding Function;

      let X be finite Function;

      let d be object;

      cluster ( NDdataSeq (g,X,d)) -> finite;

      coherence

      proof

        ( dom ( NDdataSeq (g,X,d))) = ( dom X) by Def4;

        hence thesis by FINSET_1: 10;

      end;

    end

    registration

      let g be Function-yielding Function;

      let X be FinSequence;

      let d be object;

      cluster ( NDdataSeq (g,X,d)) -> FinSequence-like;

      coherence

      proof

        take ( len X);

        

        thus ( dom ( NDdataSeq (g,X,d))) = ( dom X) by Def4

        .= ( Seg ( len X)) by FINSEQ_1:def 3;

      end;

    end

    definition

      let g be Function-yielding Function;

      let X be Function;

      let d be object;

      :: NOMIN_2:def5

      func NDentry (g,X,d) -> set equals ( rng ( NDdataSeq (g,X,d)));

      coherence ;

    end

    theorem :: NOMIN_2:22

    for f be Function, a,d be object holds ( NDentry ( <*f*>, <*a*>,d)) = { [a, (f . d)]}

    proof

      let f be Function;

      let a,d be object;

      set X = <*a*>;

      set G = <*f*>;

      set A = { [a, (f . d)]};

      set N = ( NDdataSeq (G,X,d));

      set F = ( NDentry (G,X,d));

      

       A1: ( dom N) = ( dom X) by Def4;

      

       A2: ( dom X) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      

       A3: 1 in {1} by TARSKI:def 1;

      then

       A4: (N . 1) = [(X . 1), ((G . 1) . d)] by A2, Def4;

      

       A5: (X . 1) = a & (G . 1) = f by FINSEQ_1: 40;

      thus F c= A

      proof

        let y be object;

        assume y in F;

        then

        consider z be object such that

         A6: z in ( dom N) and

         A7: (N . z) = y by FUNCT_1:def 3;

        z = 1 by A1, A2, A6, TARSKI:def 1;

        hence thesis by A4, A5, A7, TARSKI:def 1;

      end;

      let y,z be object;

      assume [y, z] in A;

      then [y, z] = [a, (f . d)] by TARSKI:def 1;

      hence thesis by A1, A2, A3, A4, A5, FUNCT_1:def 3;

    end;

    theorem :: NOMIN_2:23

    

     Th22: for f,g be Function, a,b,d be object holds ( NDentry ( <*f, g*>, <*a, b*>,d)) = { [a, (f . d)], [b, (g . d)]}

    proof

      let f,g be Function;

      let a,b,d be object;

      set X = <*a, b*>;

      set G = <*f, g*>;

      set A = { [a, (f . d)], [b, (g . d)]};

      set N = ( NDdataSeq (G,X,d));

      set F = ( NDentry (G,X,d));

      

       A1: ( dom N) = ( dom X) by Def4;

      

       A2: ( dom X) = {1, 2} by FINSEQ_1: 92;

      

       A3: 1 in {1, 2} by TARSKI:def 2;

      then

       A4: (N . 1) = [(X . 1), ((G . 1) . d)] by A2, Def4;

      

       A5: 2 in {1, 2} by TARSKI:def 2;

      then

       A6: (N . 2) = [(X . 2), ((G . 2) . d)] by A2, Def4;

      

       A7: (X . 1) = a & (X . 2) = b & (G . 1) = f & (G . 2) = g by FINSEQ_1: 44;

      thus F c= A

      proof

        let y be object;

        assume y in F;

        then

        consider z be object such that

         A8: z in ( dom N) and

         A9: (N . z) = y by FUNCT_1:def 3;

        z = 1 or z = 2 by A1, A2, A8, TARSKI:def 2;

        hence thesis by A4, A6, A7, A9, TARSKI:def 2;

      end;

      let y,z be object;

      assume [y, z] in A;

      then [y, z] = [a, (f . d)] or [y, z] = [b, (g . d)] by TARSKI:def 2;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, FUNCT_1:def 3;

    end;

    theorem :: NOMIN_2:24

    

     Th23: for f,g,h be Function, a,b,c,d be object holds ( NDentry ( <*f, g, h*>, <*a, b, c*>,d)) = { [a, (f . d)], [b, (g . d)], [c, (h . d)]}

    proof

      let f,g,h be Function;

      let a,b,c,d be object;

      set X = <*a, b, c*>;

      set G = <*f, g, h*>;

      set A = { [a, (f . d)], [b, (g . d)], [c, (h . d)]};

      set N = ( NDdataSeq (G,X,d));

      set F = ( NDentry (G,X,d));

      

       A1: ( dom N) = ( dom X) by Def4;

      

       A2: ( dom X) = {1, 2, 3} by Th4;

      

       A3: 1 in {1, 2, 3} by ENUMSET1:def 1;

      then

       A4: (N . 1) = [(X . 1), ((G . 1) . d)] by A2, Def4;

      

       A5: 2 in {1, 2, 3} by ENUMSET1:def 1;

      then

       A6: (N . 2) = [(X . 2), ((G . 2) . d)] by A2, Def4;

      

       A7: 3 in {1, 2, 3} by ENUMSET1:def 1;

      then

       A8: (N . 3) = [(X . 3), ((G . 3) . d)] by A2, Def4;

      

       A9: (X . 1) = a & (X . 2) = b & (X . 3) = c & (G . 1) = f & (G . 2) = g & (G . 3) = h by FINSEQ_1: 45;

      thus F c= A

      proof

        let y be object;

        assume y in F;

        then

        consider z be object such that

         A10: z in ( dom N) and

         A11: (N . z) = y by FUNCT_1:def 3;

        z = 1 or z = 2 or z = 3 by A1, A2, A10, ENUMSET1:def 1;

        hence thesis by A4, A6, A8, A9, A11, ENUMSET1:def 1;

      end;

      let y,z be object;

      assume [y, z] in A;

      then [y, z] = [a, (f . d)] or [y, z] = [b, (g . d)] or [y, z] = [c, (h . d)] by ENUMSET1:def 1;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, FUNCT_1:def 3;

    end;

    registration

      let g be Function-yielding Function;

      let X be Function;

      let d be object;

      cluster ( NDentry (g,X,d)) -> Relation-like;

      coherence

      proof

        set f = ( NDdataSeq (g,X,d));

        let x;

        assume x in ( NDentry (g,X,d));

        then

        consider z be object such that

         A1: z in ( dom f) and

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

        ( dom f) = ( dom X) by Def4;

        then (f . z) = [(X . z), ((g . z) . d)] by A1, Def4;

        hence thesis by A2;

      end;

    end

    registration

      let g be Function-yielding Function;

      let X be one-to-one Function;

      let d be object;

      cluster ( NDentry (g,X,d)) -> Function-like;

      coherence

      proof

        set f = ( NDdataSeq (g,X,d));

        let x,y1,y2 be object such that

         A1: [x, y1] in ( NDentry (g,X,d)) and

         A2: [x, y2] in ( NDentry (g,X,d));

        consider a be object such that

         A3: a in ( dom f) and

         A4: (f . a) = [x, y1] by A1, FUNCT_1:def 3;

        consider b be object such that

         A5: b in ( dom f) and

         A6: (f . b) = [x, y2] by A2, FUNCT_1:def 3;

        

         A7: ( dom f) = ( dom X) by Def4;

        

         A8: (f . a) = [(X . a), ((g . a) . d)] by A3, A7, Def4;

        (f . b) = [(X . b), ((g . b) . d)] by A5, A7, Def4;

        then x = (X . a) & x = (X . b) by A4, A6, A8, XTUPLE_0: 1;

        then a = b by A3, A5, A7, FUNCT_1:def 4;

        hence y1 = y2 by A4, A6, XTUPLE_0: 1;

      end;

    end

    registration

      let g be Function-yielding Function;

      let X be finite Function;

      let d be object;

      cluster ( NDentry (g,X,d)) -> finite;

      coherence ;

    end

    theorem :: NOMIN_2:25

    

     Th24: for g be Function-yielding Function, X be Function, d be object holds ( dom ( NDentry (g,X,d))) = ( rng X)

    proof

      let g be Function-yielding Function;

      let X be Function;

      let d be object;

      set f = ( NDentry (g,X,d));

      set h = ( NDdataSeq (g,X,d));

      

       A1: ( dom h) = ( dom X) by Def4;

      thus ( dom f) c= ( rng X)

      proof

        let x;

        assume x in ( dom f);

        then

        consider v such that

         A2: [x, v] in f by XTUPLE_0:def 12;

        consider z be object such that

         A3: z in ( dom h) and

         A4: (h . z) = [x, v] by A2, FUNCT_1:def 3;

        (h . z) = [(X . z), ((g . z) . d)] by A1, A3, Def4;

        then (X . z) = x by A4, XTUPLE_0: 1;

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

      end;

      let x;

      assume x in ( rng X);

      then

      consider z be object such that

       A5: z in ( dom X) and

       A6: (X . z) = x by FUNCT_1:def 3;

      (h . z) = [(X . z), ((g . z) . d)] by A5, Def4;

      then [(X . z), ((g . z) . d)] in ( rng h) by A1, A5, FUNCT_1: 3;

      hence thesis by A6, XTUPLE_0:def 12;

    end;

    definition

      let V, A;

      mode SCBinominativeFunction of V,A is PartFunc of ( ND (V,A)), ( ND (V,A));

    end

    reserve f,g,h for SCBinominativeFunction of V, A;

    theorem :: NOMIN_2:26

    

     Th25: ( rng ( NDdataSeq ( <*f*>, <*v*>,d))) = (v .--> (f . d))

    proof

      set g = <*f*>;

      set X = <*v*>;

      set N = ( NDdataSeq (g,X,d));

      set F = (v .--> (f . d));

      

       A1: ( dom N) = ( dom X) by Def4;

      

       A2: ( dom X) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      

       A3: (X . 1) = v by FINSEQ_1: 40;

      

       A4: (g . 1) = f by FINSEQ_1: 40;

      

       A5: F = { [v, (f . d)]} by ZFMISC_1: 29;

      thus ( rng N) c= F

      proof

        let y be object;

        assume y in ( rng N);

        then

        consider z be object such that

         A6: z in ( dom N) and

         A7: (N . z) = y by FUNCT_1:def 3;

        

         A8: z = 1 by A1, A2, A6, TARSKI:def 1;

        (N . z) = [(X . z), ((g . z) . d)] by A1, A6, Def4;

        hence thesis by A3, A4, A7, A8, A5, TARSKI:def 1;

      end;

      let m,n be object;

      assume [m, n] in F;

      then

       A9: [m, n] = [v, (f . d)] by A5, TARSKI:def 1;

      

       A10: 1 in ( dom N) by A1, A2, TARSKI:def 1;

      then (N . 1) = [(X . 1), ((g . 1) . d)] by A1, Def4;

      hence thesis by A3, A4, A9, A10, FUNCT_1:def 3;

    end;

    theorem :: NOMIN_2:27

    

     Th26: a in V & d in ( dom f) implies ( NDentry ( <*f*>, <*a*>,d)) = ( naming (V,A,a,(f . d)))

    proof

      set g = <*f*>;

      set X = <*a*>;

      assume

       A1: a in V;

      assume d in ( dom f);

      then

       A2: (f . d) is TypeSCNominativeData of V, A by NOMIN_1: 39, PARTFUN1: 4;

      ( rng ( NDdataSeq (g,X,d))) = (a .--> (f . d)) by Th25;

      hence thesis by A1, A2, NOMIN_1:def 13;

    end;

    theorem :: NOMIN_2:28

    a in V & d in ( dom f) implies ( NDentry ( <*f*>, <*a*>,d)) is NonatomicND of V, A

    proof

      assume a in V & d in ( dom f);

      then ( NDentry ( <*f*>, <*a*>,d)) = ( naming (V,A,a,(f . d))) by Th26;

      hence thesis;

    end;

    theorem :: NOMIN_2:29

     {a, b} c= V & a <> b & d in ( dom f) & d in ( dom g) implies ( NDentry ( <*f, g*>, <*a, b*>,d)) is NonatomicND of V, A

    proof

      assume that

       A1: {a, b} c= V and

       A2: a <> b and

       A3: d in ( dom f) & d in ( dom g);

      reconsider O = <*a, b*> as one-to-one FinSequence by A2, FINSEQ_3: 94;

      set F = ( NDentry ( <*f, g*>,O,d));

      

       A4: F = { [a, (f . d)], [b, (g . d)]} by Th22;

      then

       A5: ( dom F) = {a, b} by RELAT_1: 10;

      

       A6: ( rng F) = {(f . d), (g . d)} by A4, RELAT_1: 10;

      (f . d) in ( ND (V,A)) & (g . d) in ( ND (V,A)) by A3, PARTFUN1: 4;

      then ( rng F) c= ( ND (V,A)) by A6, ZFMISC_1: 32;

      hence thesis by A1, A5, Th6;

    end;

    theorem :: NOMIN_2:30

     {a, b, c} c= V & (a,b,c) are_mutually_distinct & d in ( dom f) & d in ( dom g) & d in ( dom h) implies ( NDentry ( <*f, g, h*>, <*a, b, c*>,d)) is NonatomicND of V, A

    proof

      assume that

       A1: {a, b, c} c= V and

       A2: (a,b,c) are_mutually_distinct and

       A3: d in ( dom f) & d in ( dom g) & d in ( dom h);

      reconsider O = <*a, b, c*> as one-to-one FinSequence by A2, FINSEQ_3: 95;

      set F = ( NDentry ( <*f, g, h*>,O,d));

      

       A4: F = { [a, (f . d)], [b, (g . d)], [c, (h . d)]} by Th23;

      then

       A5: ( dom F) = {a, b, c} by Th2;

      

       A6: ( rng F) = {(f . d), (g . d), (h . d)} by A4, Th3;

      (f . d) in ( ND (V,A)) & (g . d) in ( ND (V,A)) & (h . d) in ( ND (V,A)) by A3, PARTFUN1: 4;

      then ( rng F) c= ( ND (V,A)) by A6, Th1;

      hence thesis by A1, A5, Th6;

    end;

    definition

      let V, A;

      let f be FinSequence;

      :: NOMIN_2:def6

      attr f is V,A -FPrg-yielding means

      : Def6: for n st 1 <= n <= ( len f) holds (f . n) is SCBinominativeFunction of V, A;

    end

    registration

      let V, A, f;

      cluster <*f*> -> V, A -FPrg-yielding;

      coherence

      proof

        let n such that

         A1: 1 <= n <= ( len <*f*>);

        ( len <*f*>) = 1 by FINSEQ_1: 40;

        then n = 1 by A1, XXREAL_0: 1;

        hence thesis by FINSEQ_1: 40;

      end;

    end

    registration

      let V, A, f, g;

      cluster <*f, g*> -> V, A -FPrg-yielding;

      coherence

      proof

        let n such that

         A1: 1 <= n <= ( len <*f, g*>);

        ( len <*f, g*>) = (1 + 1) by FINSEQ_1: 44;

        then n = 1 or ... or n = 2 by A1;

        hence thesis by FINSEQ_1: 44;

      end;

    end

    registration

      let V, A, f, g, h;

      cluster <*f, g, h*> -> V, A -FPrg-yielding;

      coherence

      proof

        let n such that

         A1: 1 <= n <= ( len <*f, g, h*>);

        ( len <*f, g, h*>) = (1 + 2) by FINSEQ_1: 45;

        then n = 1 or ... or n = 3 by A1;

        hence thesis by FINSEQ_1: 45;

      end;

    end

    registration

      let V, A, n;

      cluster V, A -FPrg-yieldingn -element for FinSequence;

      existence

      proof

        take f = (n |-> the SCBinominativeFunction of V, A);

        thus f is V, A -FPrg-yielding

        proof

          let a be Nat;

          ( dom f) = ( Seg n);

          hence thesis by FINSEQ_2: 57, FINSEQ_3: 25;

        end;

        thus thesis;

      end;

    end

    registration

      let V, A, x;

      let g be V, A -FPrg-yielding FinSequence;

      cluster (g . x) -> Function-like Relation-like;

      coherence

      proof

        per cases ;

          suppose

           A1: x in ( dom g);

          then

          reconsider x as Element of NAT ;

          1 <= x <= ( len g) by A1, FINSEQ_3: 25;

          hence thesis by Def6;

        end;

          suppose not x in ( dom g);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let V, A;

      cluster V, A -FPrg-yielding -> Function-yielding for FinSequence;

      coherence ;

    end

    theorem :: NOMIN_2:31

    

     Th30: for g be V, A -FPrg-yielding FinSequence holds for X be one-to-one FinSequence st ( dom g) = ( dom X) & d in_doms g holds ( rng ( NDentry (g,X,d))) c= ( ND (V,A))

    proof

      let g be V, A -FPrg-yielding FinSequence;

      let X be one-to-one FinSequence;

      assume that

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

       A2: d in_doms g;

      set f = ( NDdataSeq (g,X,d));

      set D = ( NDentry (g,X,d));

      

       A3: ( dom f) = ( dom X) by Def4;

      let y be object;

      assume y in ( rng D);

      then

      consider a such that

       A4: a in ( dom D) and

       A5: (D . a) = y by FUNCT_1:def 3;

       [a, y] in D by A4, A5, FUNCT_1: 1;

      then

      consider v such that

       A6: v in ( dom f) and

       A7: (f . v) = [a, y] by FUNCT_1:def 3;

      reconsider v as Element of NAT by A6;

      (f . v) = [(X . v), ((g . v) . d)] by A3, A6, Def4;

      then

       A8: y = ((g . v) . d) by A7, XTUPLE_0: 1;

      1 <= v <= ( len g) by A1, A3, A6, FINSEQ_3: 25;

      then (g . v) is SCBinominativeFunction of V, A by Def6;

      then

       A9: ( rng (g . v)) c= ( ND (V,A)) by RELAT_1:def 19;

      d in ( dom (g . v)) by A1, A3, A6, A2;

      hence thesis by A8, A9, FUNCT_1: 3;

    end;

    theorem :: NOMIN_2:32

    for g be V, A -FPrg-yielding FinSequence holds for X be one-to-oneV -valued FinSequence st ( dom g) = ( dom X) & d in_doms g holds ( NDentry (g,X,d)) is NonatomicND of V, A

    proof

      let g be V, A -FPrg-yielding FinSequence;

      let X be one-to-oneV -valued FinSequence;

      assume

       A1: ( dom g) = ( dom X) & d in_doms g;

      

       A2: ( dom ( NDentry (g,X,d))) = ( rng X) by Th24;

      

       A3: ( rng X) c= V by RELAT_1:def 19;

      ( rng ( NDentry (g,X,d))) c= ( ND (V,A)) by A1, Th30;

      hence thesis by A2, A3, Th6;

    end;

    ::$Notion-Name

    definition

      let V, A, v;

      :: NOMIN_2:def7

      func SCassignment (V,A,v) -> Function of ( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))) means

      : Def7: for f be SCBinominativeFunction of V, A holds ( dom (it . f)) = ( dom f) & for d be TypeSCNominativeData of V, A holds d in ( dom (it . f)) implies ((it . f) . d) = ( local_overlapping (V,A,d,(f . d),v));

      existence

      proof

        defpred P[ Function, Function] means for f be SCBinominativeFunction of V, A st f = $1 holds ( dom $2) = ( dom f) & for d be TypeSCNominativeData of V, A holds d in ( dom $2) implies ($2 . d) = ( local_overlapping (V,A,d,($1 . d),v));

        

         A1: for x be Element of ( FPrg ( ND (V,A))) holds ex y be Element of ( FPrg ( ND (V,A))) st P[x, y]

        proof

          let x be Element of ( FPrg ( ND (V,A)));

          defpred Q[ object, object] means $2 = ( local_overlapping (V,A,$1,(x . $1),v));

          

           A2: for a be object st a in ( dom x) holds ex y be object st y in ( ND (V,A)) & Q[a, y]

          proof

            let a be object;

            ( local_overlapping (V,A,a,(x . a),v)) in ( ND (V,A));

            hence thesis;

          end;

          consider F be Function such that

           A3: ( dom F) = ( dom x) and

           A4: ( rng F) c= ( ND (V,A)) and

           A5: for a be object st a in ( dom x) holds Q[a, (F . a)] from FUNCT_1:sch 6( A2);

          F is PartFunc of ( ND (V,A)), ( ND (V,A)) by A3, A4, RELSET_1: 4, RELAT_1:def 18;

          then

          reconsider F as Element of ( FPrg ( ND (V,A))) by PARTFUN1: 45;

          take F;

          thus thesis by A3, A5;

        end;

        consider F be Function of ( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))) such that

         A6: for x be Element of ( FPrg ( ND (V,A))) holds P[x, (F . x)] from FUNCT_2:sch 3( A1);

        take F;

        let f be SCBinominativeFunction of V, A;

        f in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let F,G be Function of ( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))) such that

         A7: for f be SCBinominativeFunction of V, A holds ( dom (F . f)) = ( dom f) & for d be TypeSCNominativeData of V, A holds d in ( dom (F . f)) implies ((F . f) . d) = ( local_overlapping (V,A,d,(f . d),v)) and

         A8: for f be SCBinominativeFunction of V, A holds ( dom (G . f)) = ( dom f) & for d be TypeSCNominativeData of V, A holds d in ( dom (G . f)) implies ((G . f) . d) = ( local_overlapping (V,A,d,(f . d),v));

        let f be Element of ( FPrg ( ND (V,A)));

        

         A9: f is SCBinominativeFunction of V, A by PARTFUN1: 46;

        

        hence

         A10: ( dom (F . f)) = ( dom f) by A7

        .= ( dom (G . f)) by A8, A9;

        let d be object such that

         A11: d in ( dom (F . f));

        ( dom (F . f)) c= ( ND (V,A)) by RELAT_1:def 18;

        then

         A12: d is TypeSCNominativeData of V, A by A11, NOMIN_1: 39;

        

        hence ((F . f) . d) = ( local_overlapping (V,A,d,(f . d),v)) by A7, A9, A11

        .= ((G . f) . d) by A8, A9, A10, A11, A12;

      end;

    end

    ::$Notion-Name

    definition

      let V, A, v, f;

      :: NOMIN_2:def8

      func SC_assignment (f,v) -> SCBinominativeFunction of V, A equals (( SCassignment (V,A,v)) . f);

      coherence

      proof

        f in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, FUNCT_2: 5;

      end;

    end

    registration

      let V, A, f, v;

      let d be NonatomicND of V, A;

      cluster (( SC_assignment (f,v)) . d) -> Function-like Relation-like;

      coherence

      proof

        set a = ( SC_assignment (f,v));

        reconsider d1 = d as TypeSCNominativeData of V, A;

        per cases ;

          suppose d in ( dom a);

          then (a . d1) = ( local_overlapping (V,A,d1,(f . d1),v)) by Def7;

          hence thesis;

        end;

          suppose not d in ( dom a);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    theorem :: NOMIN_2:33

    for d be NonatomicND of V, A holds v in V & not d in A & not ( naming (V,A,v,(f . d))) in A & d in ( dom f) implies ( dom (( SC_assignment (f,v)) . d)) = (( dom d) \/ {v})

    proof

      set a = ( SC_assignment (f,v));

      let d be NonatomicND of V, A;

      assume that

       A1: v in V & not d in A & not ( naming (V,A,v,(f . d))) in A and

       A2: d in ( dom f);

      

       A3: ( dom a) = ( dom f) by Def7;

      reconsider d1 = d as TypeSCNominativeData of V, A;

      reconsider d2 = (f . d1) as TypeSCNominativeData of V, A by A2, PARTFUN1: 4, NOMIN_1: 39;

      ( dom ( local_overlapping (V,A,d,d2,v))) = ( {v} \/ ( dom d)) by A1, Th14;

      hence thesis by A2, A3, Def7;

    end;

    ::$Notion-Name

    definition

      let V, A;

      let g be V, A -FPrg-yielding FinSequence;

      let X be Function;

      defpred A[ object] means $1 in_doms g;

      deffunc D( Function) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom $1) & A[d] };

      :: NOMIN_2:def9

      func SCPsuperpos (g,X) -> Function of [:( Pr ( ND (V,A))), ( product g):], ( Pr ( ND (V,A))) means

      : Def9: for p be SCPartialNominativePredicate of V, A holds for x be Element of ( product g) holds ( dom (it . (p,x))) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p) & d in_doms g } & for d be TypeSCNominativeData of V, A st d in_doms g holds ((it . (p,x)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d)))));

      existence

      proof

        defpred P[ object, object, object] means for p be SCPartialNominativePredicate of V, A holds for x be Element of ( product g) st $1 = p & $2 = x holds for f be Function st f = $3 holds ( dom f) = D(p) & for d be TypeSCNominativeData of V, A holds d in ( dom f) implies (f . d) = (p . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

        

         A2: for x1,x2 be object st x1 in ( Pr ( ND (V,A))) & x2 in ( product g) holds ex y be object st y in ( Pr ( ND (V,A))) & P[x1, x2, y]

        proof

          let x1,x2 be object;

          assume x1 in ( Pr ( ND (V,A)));

          then

          reconsider X1 = x1 as PartFunc of ( ND (V,A)), BOOLEAN by PARTFUN1: 46;

          assume x2 in ( product g);

          defpred Q[ object, object] means for d be TypeSCNominativeData of V, A st d = $1 holds ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) implies $2 = (X1 . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

          

           A3: for a be object st a in D(X1) holds ex b be object st b in BOOLEAN & Q[a, b]

          proof

            let a be object;

            assume a in D(X1);

            then

            consider d be TypeSCNominativeData of V, A such that

             A4: d = a and

             A5: ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) and A[d];

            take (X1 . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

            thus thesis by A4, A5, PARTFUN1: 4;

          end;

          consider K be Function such that

           A6: ( dom K) = D(X1) and

           A7: ( rng K) c= BOOLEAN and

           A8: for x be object st x in D(X1) holds Q[x, (K . x)] from FUNCT_1:sch 6( A3);

          take K;

           D(X1) c= ( ND (V,A))

          proof

            let x;

            assume x in D(X1);

            then ex d be TypeSCNominativeData of V, A st d = x & ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) & A[d];

            hence thesis;

          end;

          then K is PartFunc of ( ND (V,A)), BOOLEAN by A6, A7, RELSET_1: 4;

          hence K in ( Pr ( ND (V,A))) by PARTFUN1: 45;

          let p be SCPartialNominativePredicate of V, A;

          let q be Element of ( product g) such that

           A9: x1 = p & x2 = q;

          let f be Function such that

           A10: f = K;

          thus ( dom f) = D(p) by A6, A9, A10;

          let d be TypeSCNominativeData of V, A;

          assume

           A11: d in ( dom f);

          then ex d1 be TypeSCNominativeData of V, A st d1 = d & ( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom X1) & A[d1] by A6, A10;

          hence (f . d) = (p . ( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A6, A8, A9, A10, A11;

        end;

        consider F be Function of [:( Pr ( ND (V,A))), ( product g):], ( Pr ( ND (V,A))) such that

         A12: for x,y be object st x in ( Pr ( ND (V,A))) & y in ( product g) holds P[x, y, (F . (x,y))] from BINOP_1:sch 1( A2);

        take F;

        let p be SCPartialNominativePredicate of V, A;

        let q be Element of ( product g);

        

         A13: p in ( Pr ( ND (V,A))) & q in ( product g) by A1, PARTFUN1: 45;

        hence

         A14: ( dom (F . (p,q))) = D(p) by A12;

        let d be TypeSCNominativeData of V, A such that

         A15: A[d];

        thus d in ( dom (F . (p,q))) iff ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p)

        proof

          hereby

            assume d in ( dom (F . (p,q)));

            then ex d1 be TypeSCNominativeData of V, A st d = d1 & ( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom p) & A[d1] by A14;

            hence ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p);

          end;

          thus thesis by A14, A15;

        end;

        thus thesis by A12, A13;

      end;

      uniqueness

      proof

        let F,G be Function of [:( Pr ( ND (V,A))), ( product g):], ( Pr ( ND (V,A))) such that

         A16: for p be SCPartialNominativePredicate of V, A holds for x be Element of ( product g) holds ( dom (F . (p,x))) = D(p) & for d be TypeSCNominativeData of V, A st A[d] holds ((F . (p,x)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d))))) and

         A17: for p be SCPartialNominativePredicate of V, A holds for x be Element of ( product g) holds ( dom (G . (p,x))) = D(p) & for d be TypeSCNominativeData of V, A st A[d] holds ((G . (p,x)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d)))));

        let a,b be set;

        assume a in ( Pr ( ND (V,A)));

        then

        reconsider p = a as SCPartialNominativePredicate of V, A by PARTFUN1: 46;

        assume

         A18: b in ( product g);

        then

         A19: ( dom (F . (a,b))) = D(p) by A16;

        hence ( dom (F . (a,b))) = ( dom (G . (a,b))) by A17, A18;

        let z be object;

        assume

         A20: z in ( dom (F . (a,b)));

        then

        consider d be TypeSCNominativeData of V, A such that

         A21: d = z and ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p) and

         A22: A[d] by A19;

        

         A23: ((G . (p,b)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A17, A18, A22;

        ((F . (p,b)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A16, A18, A22;

        hence thesis by A20, A23, A21;

      end;

    end

    ::$Notion-Name

    definition

      let V, A, p;

      let g be V, A -FPrg-yielding FinSequence;

      let X be Function;

      let x be Element of ( product g);

      :: NOMIN_2:def10

      func SC_Psuperpos (p,x,X) -> SCPartialNominativePredicate of V, A equals

      : Def10: (( SCPsuperpos (g,X)) . (p,x));

      coherence

      proof

        p in ( Pr ( ND (V,A))) & x in ( product g) by A1, PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    theorem :: NOMIN_2:34

    

     Th33: for g be V, A -FPrg-yielding FinSequence st ( product g) <> {} holds for x be Element of ( product g) st d in ( dom ( SC_Psuperpos (p,x,X))) holds d in_doms g & (( SC_Psuperpos (p,x,X)) . d) = (p . ( global_overlapping (V,A,d,( NDentry (g,X,d)))))

    proof

      let g be V, A -FPrg-yielding FinSequence such that

       A1: ( product g) <> {} ;

      let x be Element of ( product g) such that

       A2: d in ( dom ( SC_Psuperpos (p,x,X)));

      ( SC_Psuperpos (p,x,X)) = (( SCPsuperpos (g,X)) . (p,x)) by A1, Def10;

      then ( dom ( SC_Psuperpos (p,x,X))) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p) & d in_doms g } by A1, Def9;

      then

       A3: ex d1 be TypeSCNominativeData of V, A st d1 = d & ( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom p) & d1 in_doms g by A2;

      then ((( SCPsuperpos (g,X)) . (p,x)),d) =~ (p,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A1, Def9;

      hence thesis by A1, A3, Def10;

    end;

    ::$Notion-Name

    definition

      let V, A, v;

      deffunc D( Function, Function) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,($2 . d),v)) in ( dom $1) & d in ( dom $2) };

      :: NOMIN_2:def11

      func SCPsuperpos (V,A,v) -> Function of [:( Pr ( ND (V,A))), ( FPrg ( ND (V,A))):], ( Pr ( ND (V,A))) means

      : Def11: for p be SCPartialNominativePredicate of V, A holds for f be SCBinominativeFunction of V, A holds ( dom (it . (p,f))) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) & d in ( dom f) } & for d be TypeSCNominativeData of V, A st d in ( dom f) holds ((it . (p,f)),d) =~ (p,( local_overlapping (V,A,d,(f . d),v)));

      existence

      proof

        defpred P[ object, object, object] means for p be SCPartialNominativePredicate of V, A holds for f be SCBinominativeFunction of V, A st $1 = p & $2 = f holds for F be Function st F = $3 holds ( dom F) = D(p,f) & for d be TypeSCNominativeData of V, A holds d in ( dom F) implies (F . d) = (p . ( local_overlapping (V,A,d,(f . d),v)));

        

         A1: for x1,x2 be object st x1 in ( Pr ( ND (V,A))) & x2 in ( FPrg ( ND (V,A))) holds ex y be object st y in ( Pr ( ND (V,A))) & P[x1, x2, y]

        proof

          let x1,x2 be object;

          assume x1 in ( Pr ( ND (V,A)));

          then

          reconsider X1 = x1 as PartFunc of ( ND (V,A)), BOOLEAN by PARTFUN1: 46;

          assume x2 in ( FPrg ( ND (V,A)));

          then

          reconsider X2 = x2 as PartFunc of ( ND (V,A)), ( ND (V,A)) by PARTFUN1: 46;

          defpred Q[ object, object] means for d be TypeSCNominativeData of V, A st d = $1 holds ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) implies $2 = (X1 . ( local_overlapping (V,A,d,(X2 . d),v)));

          

           A2: for a be object st a in D(X1,X2) holds ex b be object st b in BOOLEAN & Q[a, b]

          proof

            let a be object;

            assume a in D(X1,X2);

            then

            consider d be TypeSCNominativeData of V, A such that

             A3: d = a & ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) & d in ( dom X2);

            take (X1 . ( local_overlapping (V,A,d,(X2 . d),v)));

            thus thesis by A3, PARTFUN1: 4;

          end;

          consider K be Function such that

           A4: ( dom K) = D(X1,X2) and

           A5: ( rng K) c= BOOLEAN and

           A6: for x be object st x in D(X1,X2) holds Q[x, (K . x)] from FUNCT_1:sch 6( A2);

          take K;

           D(X1,X2) c= ( ND (V,A))

          proof

            let x;

            assume x in D(X1,X2);

            then ex d be TypeSCNominativeData of V, A st d = x & ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) & d in ( dom X2);

            hence thesis;

          end;

          then K is PartFunc of ( ND (V,A)), BOOLEAN by A4, A5, RELSET_1: 4;

          hence K in ( Pr ( ND (V,A))) by PARTFUN1: 45;

          let p be SCPartialNominativePredicate of V, A;

          let f be SCBinominativeFunction of V, A such that

           A7: x1 = p & x2 = f;

          let F be Function such that

           A8: F = K;

          thus ( dom F) = D(p,f) by A4, A7, A8;

          let d be TypeSCNominativeData of V, A;

          assume

           A9: d in ( dom F);

          then ex d1 be TypeSCNominativeData of V, A st d1 = d & ( local_overlapping (V,A,d1,(X2 . d1),v)) in ( dom X1) & d1 in ( dom X2) by A4, A8;

          hence thesis by A4, A6, A7, A8, A9;

        end;

        consider F be Function of [:( Pr ( ND (V,A))), ( FPrg ( ND (V,A))):], ( Pr ( ND (V,A))) such that

         A10: for x,y be object st x in ( Pr ( ND (V,A))) & y in ( FPrg ( ND (V,A))) holds P[x, y, (F . (x,y))] from BINOP_1:sch 1( A1);

        take F;

        let p be SCPartialNominativePredicate of V, A;

        let f be SCBinominativeFunction of V, A;

        

         A11: p in ( Pr ( ND (V,A))) & f in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence

         A12: ( dom (F . (p,f))) = D(p,f) by A10;

        let d be TypeSCNominativeData of V, A such that

         A13: d in ( dom f);

        thus d in ( dom (F . (p,f))) iff ( local_overlapping (V,A,d,(f . d),v)) in ( dom p)

        proof

          hereby

            assume d in ( dom (F . (p,f)));

            then ex d1 be TypeSCNominativeData of V, A st d = d1 & ( local_overlapping (V,A,d1,(f . d1),v)) in ( dom p) & d1 in ( dom f) by A12;

            hence ( local_overlapping (V,A,d,(f . d),v)) in ( dom p);

          end;

          thus thesis by A12, A13;

        end;

        thus thesis by A10, A11;

      end;

      uniqueness

      proof

        let F,G be Function of [:( Pr ( ND (V,A))), ( FPrg ( ND (V,A))):], ( Pr ( ND (V,A))) such that

         A14: for p be SCPartialNominativePredicate of V, A holds for f be SCBinominativeFunction of V, A holds ( dom (F . (p,f))) = D(p,f) & for d be TypeSCNominativeData of V, A st d in ( dom f) holds ((F . (p,f)),d) =~ (p,( local_overlapping (V,A,d,(f . d),v))) and

         A15: for p be SCPartialNominativePredicate of V, A holds for f be SCBinominativeFunction of V, A holds ( dom (G . (p,f))) = D(p,f) & for d be TypeSCNominativeData of V, A st d in ( dom f) holds ((G . (p,f)),d) =~ (p,( local_overlapping (V,A,d,(f . d),v)));

        let a,b be set;

        assume a in ( Pr ( ND (V,A)));

        then

        reconsider p = a as SCPartialNominativePredicate of V, A by PARTFUN1: 46;

        assume b in ( FPrg ( ND (V,A)));

        then

        reconsider f = b as SCBinominativeFunction of V, A by PARTFUN1: 46;

        

         A16: ( dom (F . (a,b))) = D(p,f) by A14;

        hence ( dom (F . (a,b))) = ( dom (G . (a,b))) by A15;

        let z be object;

        assume z in ( dom (F . (a,b)));

        then

        consider d be TypeSCNominativeData of V, A such that

         A17: z = d & ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) and

         A18: d in ( dom f) by A16;

        

         A19: ((G . (p,f)),d) =~ (p,( local_overlapping (V,A,d,(f . d),v))) by A15, A18;

        ((F . (p,f)),d) =~ (p,( local_overlapping (V,A,d,(f . d),v))) by A14, A18;

        hence thesis by A17, A19;

      end;

    end

    ::$Notion-Name

    definition

      let V, A, v, p, f;

      :: NOMIN_2:def12

      func SC_Psuperpos (p,f,v) -> SCPartialNominativePredicate of V, A equals (( SCPsuperpos (V,A,v)) . (p,f));

      coherence

      proof

        p in ( Pr ( ND (V,A))) & f in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    theorem :: NOMIN_2:35

    

     Th34: d in ( dom ( SC_Psuperpos (p,f,v))) implies (( SC_Psuperpos (p,f,v)) . d) = (p . ( local_overlapping (V,A,d,(f . d),v))) & d in ( dom f)

    proof

      set F = ( SC_Psuperpos (p,f,v));

      assume

       A1: d in ( dom F);

      ( dom F) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) & d in ( dom f) } by Def11;

      then

       A2: ex d1 be TypeSCNominativeData of V, A st d1 = d & ( local_overlapping (V,A,d1,(f . d1),v)) in ( dom p) & d1 in ( dom f) by A1;

      then (F,d) =~ (p,( local_overlapping (V,A,d,(f . d),v))) by Def11;

      hence thesis by A2;

    end;

    theorem :: NOMIN_2:36

    for x be Element of ( product <*f*>) st v in V & ( product <*f*>) <> {} holds ( SC_Psuperpos (p,f,v)) = ( SC_Psuperpos (p,x, <*v*>))

    proof

      set g = <*f*>;

      let x be Element of ( product g);

      assume that

       A1: v in V and

       A2: ( product g) <> {} ;

      set X = <*v*>;

      set S1 = ( SC_Psuperpos (p,f,v));

      set S2 = ( SC_Psuperpos (p,x,X));

      defpred A[ object] means $1 in_doms g;

      

       A3: (g . 1) = f by FINSEQ_1: 40;

      

       A4: ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      

       A5: ( dom S1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) & d in ( dom f) } by Def11;

      S2 = (( SCPsuperpos (g,X)) . (p,x)) by A2, Def10;

      then

       A6: ( dom S2) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p) & A[d] } by A2, Def9;

      thus

       A7: ( dom S1) = ( dom S2)

      proof

        thus ( dom S1) c= ( dom S2)

        proof

          let a be object;

          assume a in ( dom S1);

          then

          consider d such that

           A8: d = a and

           A9: ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) and

           A10: d in ( dom f) by A5;

          

           A11: A[d]

          proof

            let x;

            thus thesis by A10, A3, A4, TARSKI:def 1;

          end;

          ( NDentry (g,X,d)) = ( naming (V,A,v,(f . d))) by A1, A10, Th26;

          hence thesis by A8, A9, A11, A6;

        end;

        let a be object;

        assume a in ( dom S2);

        then

        consider d such that

         A12: a = d and

         A13: ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom p) and

         A14: A[d] by A6;

        1 in ( dom g) by A4, TARSKI:def 1;

        then

         A15: d in ( dom (g . 1)) by A14, Def3;

        then ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) by A1, Th26, A13, A3;

        hence thesis by A5, A12, A3, A15;

      end;

      let a be object;

      assume

       A16: a in ( dom S1);

      then

      consider d such that

       A17: d = a and ( local_overlapping (V,A,d,(f . d),v)) in ( dom p) and

       A18: d in ( dom f) by A5;

      ( NDentry (g,X,d)) = ( naming (V,A,v,(f . d))) by A1, A18, Th26;

      

      hence (S2 . a) = (p . ( local_overlapping (V,A,d,(f . d),v))) by A7, A16, A17, A2, Th33

      .= (S1 . a) by A16, A17, Th34;

    end;

    ::$Notion-Name

    definition

      let V, A;

      let g be V, A -FPrg-yielding FinSequence;

      let X be Function;

      defpred A[ object] means $1 in_doms g;

      deffunc D( Function) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom $1) & A[d] };

      :: NOMIN_2:def13

      func SCFsuperpos (g,X) -> Function of [:( FPrg ( ND (V,A))), ( product g):], ( FPrg ( ND (V,A))) means

      : Def13: for f be SCBinominativeFunction of V, A holds for x be Element of ( product g) holds ( dom (it . (f,x))) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom f) & d in_doms g } & for d be TypeSCNominativeData of V, A st d in_doms g holds ((it . (f,x)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d)))));

      existence

      proof

        defpred P[ object, object, object] means for f be SCBinominativeFunction of V, A holds for x be Element of ( product g) st $1 = f & $2 = x holds for h be Function st h = $3 holds ( dom h) = D(f) & for d be TypeSCNominativeData of V, A holds d in ( dom h) implies (h . d) = (f . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

        

         A2: for x1,x2 be object st x1 in ( FPrg ( ND (V,A))) & x2 in ( product g) holds ex y be object st y in ( FPrg ( ND (V,A))) & P[x1, x2, y]

        proof

          let x1,x2 be object;

          assume x1 in ( FPrg ( ND (V,A)));

          then

          reconsider X1 = x1 as PartFunc of ( ND (V,A)), ( ND (V,A)) by PARTFUN1: 46;

          assume x2 in ( product g);

          defpred Q[ object, object] means for d be TypeSCNominativeData of V, A st d = $1 holds ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) implies $2 = (X1 . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

          

           A3: for a be object st a in D(X1) holds ex b be object st b in ( ND (V,A)) & Q[a, b]

          proof

            let a be object;

            assume a in D(X1);

            then

            consider d be TypeSCNominativeData of V, A such that

             A4: d = a & ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) & A[d];

            take (X1 . ( global_overlapping (V,A,d,( NDentry (g,X,d)))));

            thus thesis by A4, PARTFUN1: 4;

          end;

          consider K be Function such that

           A5: ( dom K) = D(X1) and

           A6: ( rng K) c= ( ND (V,A)) and

           A7: for x be object st x in D(X1) holds Q[x, (K . x)] from FUNCT_1:sch 6( A3);

          take K;

           D(X1) c= ( ND (V,A))

          proof

            let x;

            assume x in D(X1);

            then ex d be TypeSCNominativeData of V, A st d = x & ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom X1) & A[d];

            hence thesis;

          end;

          then K is PartFunc of ( ND (V,A)), ( ND (V,A)) by A5, A6, RELSET_1: 4;

          hence K in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

          let f be SCBinominativeFunction of V, A;

          let q be Element of ( product g) such that

           A8: x1 = f & x2 = q;

          let h be Function such that

           A9: h = K;

          thus ( dom h) = D(f) by A5, A8, A9;

          let d be TypeSCNominativeData of V, A;

          assume

           A10: d in ( dom h);

          then ex d1 be TypeSCNominativeData of V, A st d1 = d & ( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom X1) & A[d1] by A5, A9;

          hence (h . d) = (f . ( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A5, A7, A8, A9, A10;

        end;

        consider F be Function of [:( FPrg ( ND (V,A))), ( product g):], ( FPrg ( ND (V,A))) such that

         A11: for x,y be object st x in ( FPrg ( ND (V,A))) & y in ( product g) holds P[x, y, (F . (x,y))] from BINOP_1:sch 1( A2);

        take F;

        let f be SCBinominativeFunction of V, A;

        let q be Element of ( product g);

        

         A12: f in ( FPrg ( ND (V,A))) & q in ( product g) by A1, PARTFUN1: 45;

        hence

         A13: ( dom (F . (f,q))) = D(f) by A11;

        let d be TypeSCNominativeData of V, A such that

         A14: A[d];

        thus d in ( dom (F . (f,q))) iff ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom f)

        proof

          hereby

            assume d in ( dom (F . (f,q)));

            then ex d1 be TypeSCNominativeData of V, A st d = d1 & ( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom f) & A[d1] by A13;

            hence ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom f);

          end;

          thus thesis by A13, A14;

        end;

        thus thesis by A11, A12;

      end;

      uniqueness

      proof

        let F,G be Function of [:( FPrg ( ND (V,A))), ( product g):], ( FPrg ( ND (V,A))) such that

         A15: for f be SCBinominativeFunction of V, A holds for x be Element of ( product g) holds ( dom (F . (f,x))) = D(f) & for d be TypeSCNominativeData of V, A st d in_doms g holds ((F . (f,x)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d))))) and

         A16: for f be SCBinominativeFunction of V, A holds for x be Element of ( product g) holds ( dom (G . (f,x))) = D(f) & for d be TypeSCNominativeData of V, A st d in_doms g holds ((G . (f,x)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d)))));

        let a,b be set;

        assume a in ( FPrg ( ND (V,A)));

        then

        reconsider f = a as SCBinominativeFunction of V, A by PARTFUN1: 46;

        assume

         A17: b in ( product g);

        then

         A18: ( dom (F . (a,b))) = D(f) by A15;

        hence ( dom (F . (a,b))) = ( dom (G . (a,b))) by A16, A17;

        let z be object;

        assume z in ( dom (F . (a,b)));

        then

        consider d be TypeSCNominativeData of V, A such that

         A19: z = d & ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom f) & A[d] by A18;

        

         A20: ((G . (f,b)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A16, A17, A19;

        ((F . (f,b)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A15, A17, A19;

        hence thesis by A19, A20;

      end;

    end

    ::$Notion-Name

    definition

      let V, A, f;

      let g be V, A -FPrg-yielding FinSequence;

      let X be Function;

      let x be Element of ( product g);

      :: NOMIN_2:def14

      func SC_Fsuperpos (f,x,X) -> SCBinominativeFunction of V, A equals

      : Def14: (( SCFsuperpos (g,X)) . (f,x));

      coherence

      proof

        f in ( FPrg ( ND (V,A))) & x in ( product g) by A1, PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    theorem :: NOMIN_2:37

    

     Th36: for g be V, A -FPrg-yielding FinSequence st ( product g) <> {} holds for x be Element of ( product g) st d in ( dom ( SC_Fsuperpos (f,x,X))) holds d in_doms g & (( SC_Fsuperpos (f,x,X)) . d) = (f . ( global_overlapping (V,A,d,( NDentry (g,X,d)))))

    proof

      let g be V, A -FPrg-yielding FinSequence such that

       A1: ( product g) <> {} ;

      let x be Element of ( product g) such that

       A2: d in ( dom ( SC_Fsuperpos (f,x,X)));

      

       A3: ( dom (( SCFsuperpos (g,X)) . (f,x))) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (g,X,d)))) in ( dom f) & d in_doms g } by A1, Def13;

      ( SC_Fsuperpos (f,x,X)) = (( SCFsuperpos (g,X)) . (f,x)) by A1, Def14;

      then

       A4: ex d1 be TypeSCNominativeData of V, A st d1 = d & (( global_overlapping (V,A,d1,( NDentry (g,X,d1)))) in ( dom f) & d1 in_doms g) by A2, A3;

      then ((( SCFsuperpos (g,X)) . (f,x)),d) =~ (f,( global_overlapping (V,A,d,( NDentry (g,X,d))))) by A1, Def13;

      hence thesis by A1, A4, Def14;

    end;

    ::$Notion-Name

    definition

      let V, A, v;

      deffunc D( Function, Function) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,($2 . d),v)) in ( dom $1) & d in ( dom $2) };

      :: NOMIN_2:def15

      func SCFsuperpos (V,A,v) -> Function of [:( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))):], ( FPrg ( ND (V,A))) means

      : Def15: for f,g be SCBinominativeFunction of V, A holds ( dom (it . (f,g))) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) & d in ( dom g) } & for d be TypeSCNominativeData of V, A st d in ( dom g) holds ((it . (f,g)),d) =~ (f,( local_overlapping (V,A,d,(g . d),v)));

      existence

      proof

        defpred P[ object, object, object] means for f,g be SCBinominativeFunction of V, A st $1 = f & $2 = g holds for F be Function st F = $3 holds ( dom F) = D(f,g) & for d be TypeSCNominativeData of V, A holds d in ( dom F) implies (F . d) = (f . ( local_overlapping (V,A,d,(g . d),v)));

        

         A1: for x1,x2 be object st x1 in ( FPrg ( ND (V,A))) & x2 in ( FPrg ( ND (V,A))) holds ex y be object st y in ( FPrg ( ND (V,A))) & P[x1, x2, y]

        proof

          let x1,x2 be object;

          assume x1 in ( FPrg ( ND (V,A)));

          then

          reconsider X1 = x1 as PartFunc of ( ND (V,A)), ( ND (V,A)) by PARTFUN1: 46;

          assume x2 in ( FPrg ( ND (V,A)));

          then

          reconsider X2 = x2 as PartFunc of ( ND (V,A)), ( ND (V,A)) by PARTFUN1: 46;

          defpred Q[ object, object] means for d be TypeSCNominativeData of V, A st d = $1 holds ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) implies $2 = (X1 . ( local_overlapping (V,A,d,(X2 . d),v)));

          

           A2: for a be object st a in D(X1,X2) holds ex b be object st b in ( ND (V,A)) & Q[a, b]

          proof

            let a be object;

            assume a in D(X1,X2);

            then

            consider d be TypeSCNominativeData of V, A such that

             A3: d = a & ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) & d in ( dom X2);

            take (X1 . ( local_overlapping (V,A,d,(X2 . d),v)));

            thus thesis by A3, PARTFUN1: 4;

          end;

          consider K be Function such that

           A4: ( dom K) = D(X1,X2) and

           A5: ( rng K) c= ( ND (V,A)) and

           A6: for x be object st x in D(X1,X2) holds Q[x, (K . x)] from FUNCT_1:sch 6( A2);

          take K;

           D(X1,X2) c= ( ND (V,A))

          proof

            let x;

            assume x in D(X1,X2);

            then ex d be TypeSCNominativeData of V, A st d = x & ( local_overlapping (V,A,d,(X2 . d),v)) in ( dom X1) & d in ( dom X2);

            hence thesis;

          end;

          then K is PartFunc of ( ND (V,A)), ( ND (V,A)) by A4, A5, RELSET_1: 4;

          hence K in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

          let f,g be SCBinominativeFunction of V, A such that

           A7: x1 = f & x2 = g;

          let F be Function such that

           A8: F = K;

          thus ( dom F) = D(f,g) by A4, A7, A8;

          let d be TypeSCNominativeData of V, A;

          assume

           A9: d in ( dom F);

          then ex d1 be TypeSCNominativeData of V, A st d1 = d & ( local_overlapping (V,A,d1,(X2 . d1),v)) in ( dom X1) & d1 in ( dom X2) by A4, A8;

          hence thesis by A4, A6, A7, A8, A9;

        end;

        consider F be Function of [:( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))):], ( FPrg ( ND (V,A))) such that

         A10: for x,y be object st x in ( FPrg ( ND (V,A))) & y in ( FPrg ( ND (V,A))) holds P[x, y, (F . (x,y))] from BINOP_1:sch 1( A1);

        take F;

        let f, g;

        

         A11: f in ( FPrg ( ND (V,A))) & g in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence

         A12: ( dom (F . (f,g))) = D(f,g) by A10;

        let d be TypeSCNominativeData of V, A such that

         A13: d in ( dom g);

        thus d in ( dom (F . (f,g))) iff ( local_overlapping (V,A,d,(g . d),v)) in ( dom f)

        proof

          hereby

            assume d in ( dom (F . (f,g)));

            then ex d1 be TypeSCNominativeData of V, A st d = d1 & ( local_overlapping (V,A,d1,(g . d1),v)) in ( dom f) & d1 in ( dom g) by A12;

            hence ( local_overlapping (V,A,d,(g . d),v)) in ( dom f);

          end;

          thus thesis by A12, A13;

        end;

        thus thesis by A10, A11;

      end;

      uniqueness

      proof

        let F,G be Function of [:( FPrg ( ND (V,A))), ( FPrg ( ND (V,A))):], ( FPrg ( ND (V,A))) such that

         A14: for f,g be SCBinominativeFunction of V, A holds ( dom (F . (f,g))) = D(f,g) & for d be TypeSCNominativeData of V, A st d in ( dom g) holds ((F . (f,g)),d) =~ (f,( local_overlapping (V,A,d,(g . d),v))) and

         A15: for f,g be SCBinominativeFunction of V, A holds ( dom (G . (f,g))) = D(f,g) & for d be TypeSCNominativeData of V, A st d in ( dom g) holds ((G . (f,g)),d) =~ (f,( local_overlapping (V,A,d,(g . d),v)));

        let a,b be set;

        assume a in ( FPrg ( ND (V,A)));

        then

        reconsider f = a as SCBinominativeFunction of V, A by PARTFUN1: 46;

        assume b in ( FPrg ( ND (V,A)));

        then

        reconsider g = b as SCBinominativeFunction of V, A by PARTFUN1: 46;

        

         A16: ( dom (F . (a,b))) = D(f,g) by A14;

        hence ( dom (F . (a,b))) = ( dom (G . (a,b))) by A15;

        let z be object;

        assume z in ( dom (F . (a,b)));

        then

        consider d be TypeSCNominativeData of V, A such that

         A17: z = d & ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) and

         A18: d in ( dom g) by A16;

        

         A19: ((G . (f,g)),d) =~ (f,( local_overlapping (V,A,d,(g . d),v))) by A15, A18;

        ((F . (f,g)),d) =~ (f,( local_overlapping (V,A,d,(g . d),v))) by A14, A18;

        hence thesis by A17, A19;

      end;

    end

    ::$Notion-Name

    definition

      let V, A, v, f, g;

      :: NOMIN_2:def16

      func SC_Fsuperpos (f,g,v) -> SCBinominativeFunction of V, A equals (( SCFsuperpos (V,A,v)) . (f,g));

      coherence

      proof

        f in ( FPrg ( ND (V,A))) & g in ( FPrg ( ND (V,A))) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    theorem :: NOMIN_2:38

    

     Th37: d in ( dom ( SC_Fsuperpos (f,g,v))) implies (( SC_Fsuperpos (f,g,v)) . d) = (f . ( local_overlapping (V,A,d,(g . d),v))) & d in ( dom g)

    proof

      set F = ( SC_Fsuperpos (f,g,v));

      assume

       A1: d in ( dom F);

      ( dom F) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) & d in ( dom g) } by Def15;

      then

       A2: ex d1 be TypeSCNominativeData of V, A st d1 = d & (( local_overlapping (V,A,d1,(g . d1),v)) in ( dom f) & d1 in ( dom g)) by A1;

      (F,d) =~ (f,( local_overlapping (V,A,d,(g . d),v))) by A2, Def15;

      hence thesis by A2;

    end;

    theorem :: NOMIN_2:39

    for x be Element of ( product <*g*>) st v in V & ( product <*g*>) <> {} holds ( SC_Fsuperpos (f,g,v)) = ( SC_Fsuperpos (f,x, <*v*>))

    proof

      set G = <*g*>;

      let x be Element of ( product G);

      assume that

       A1: v in V and

       A2: ( product G) <> {} ;

      set X = <*v*>;

      set S1 = ( SC_Fsuperpos (f,g,v));

      set S2 = ( SC_Fsuperpos (f,x,X));

      defpred A[ object] means $1 in_doms G;

      

       A3: (G . 1) = g by FINSEQ_1: 40;

      

       A4: ( dom G) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      

       A5: ( dom S1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) & d in ( dom g) } by Def15;

      S2 = (( SCFsuperpos (G,X)) . (f,x)) by A2, Def14;

      then

       A6: ( dom S2) = { d where d be TypeSCNominativeData of V, A : ( global_overlapping (V,A,d,( NDentry (G,X,d)))) in ( dom f) & A[d] } by A2, Def13;

      thus

       A7: ( dom S1) = ( dom S2)

      proof

        thus ( dom S1) c= ( dom S2)

        proof

          let a be object;

          assume a in ( dom S1);

          then

          consider d such that

           A8: d = a and

           A9: ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) and

           A10: d in ( dom g) by A5;

          

           A11: A[d]

          proof

            let x;

            thus thesis by A10, A3, A4, TARSKI:def 1;

          end;

          ( NDentry (G,X,d)) = ( naming (V,A,v,(g . d))) by A1, A10, Th26;

          hence thesis by A8, A9, A11, A6;

        end;

        let a be object;

        assume a in ( dom S2);

        then

        consider d such that

         A12: a = d and

         A13: ( global_overlapping (V,A,d,( NDentry (G,X,d)))) in ( dom f) and

         A14: A[d] by A6;

        1 in ( dom G) by A4, TARSKI:def 1;

        then

         A15: d in ( dom (G . 1)) by A14, Def3;

        then ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) by A1, Th26, A13, A3;

        hence thesis by A5, A12, A3, A15;

      end;

      let a be object;

      assume

       A16: a in ( dom S1);

      then

      consider d such that

       A17: d = a and ( local_overlapping (V,A,d,(g . d),v)) in ( dom f) and

       A18: d in ( dom g) by A5;

      ( NDentry (G,X,d)) = ( naming (V,A,v,(g . d))) by A1, A18, Th26;

      

      hence (S2 . a) = (f . ( local_overlapping (V,A,d,(g . d),v))) by A7, A16, A17, A2, Th36

      .= (S1 . a) by A16, A17, Th37;

    end;

    ::$Notion-Name

    definition

      let V, A, v;

      defpred P[ object] means ex d be NonatomicND of V, A st d = $1 & ( denaming (v,d)) in (( ND (V,A)) \ A);

      :: NOMIN_2:def17

      func SC_name_check (V,A,v) -> SCPartialNominativePredicate of V, A means ( dom it ) = (( ND (V,A)) \ A) & for d be NonatomicND of V, A st d in ( dom it ) holds (( denaming (v,d)) in ( dom it ) implies (it . d) = TRUE ) & ( not ( denaming (v,d)) in ( dom it ) implies (it . d) = FALSE );

      existence

      proof

        

         A1: (( ND (V,A)) \ A) c= ( ND (V,A));

        consider p be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = (( ND (V,A)) \ A) and

         A3: for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ) from PARTPR_2:sch 1( A1);

        take p;

        thus ( dom p) = (( ND (V,A)) \ A) by A2;

        let d be NonatomicND of V, A such that

         A4: d in ( dom p);

        thus ( denaming (v,d)) in ( dom p) implies (p . d) = TRUE by A2, A3, A4;

        assume not ( denaming (v,d)) in ( dom p);

        then not P[d] by A2;

        hence thesis by A3, A4;

      end;

      uniqueness

      proof

        let F,G be SCPartialNominativePredicate of V, A such that

         A5: ( dom F) = (( ND (V,A)) \ A) and

         A6: for d be NonatomicND of V, A st d in ( dom F) holds (( denaming (v,d)) in ( dom F) implies (F . d) = TRUE ) & ( not ( denaming (v,d)) in ( dom F) implies (F . d) = FALSE ) and

         A7: ( dom G) = (( ND (V,A)) \ A) and

         A8: for d be NonatomicND of V, A st d in ( dom G) holds (( denaming (v,d)) in ( dom G) implies (G . d) = TRUE ) & ( not ( denaming (v,d)) in ( dom G) implies (G . d) = FALSE );

        thus ( dom F) = ( dom G) by A5, A7;

        let x;

        assume

         A9: x in ( dom F);

        then

        reconsider d = x as NonatomicND of V, A by A5, NOMIN_1: 43;

        per cases ;

          suppose

           A10: ( denaming (v,d)) in ( dom F);

          

          hence (F . x) = TRUE by A6, A9

          .= (G . x) by A5, A7, A8, A9, A10;

        end;

          suppose

           A11: not ( denaming (v,d)) in ( dom F);

          

          hence (F . x) = FALSE by A6, A9

          .= (G . x) by A5, A7, A8, A9, A11;

        end;

      end;

    end