substut1.miz



    begin

    reserve A for QC-alphabet;

    reserve a,b,b1,b2,c,d for object,

i,j,k,n for Nat,

x,y,x1,x2 for bound_QC-variable of A,

P for QC-pred_symbol of k, A,

ll for CQC-variable_list of k, A,

l1,l2 for FinSequence of ( QC-variables A),

p for QC-formula of A,

s,t for QC-symbol of A;

    definition

      let A;

      :: SUBSTUT1:def1

      func vSUB (A) -> set equals ( PFuncs (( bound_QC-variables A),( bound_QC-variables A)));

      coherence ;

    end

    registration

      let A;

      cluster ( vSUB A) -> non empty;

      coherence ;

    end

    definition

      let A;

      mode CQC_Substitution of A is Element of ( vSUB A);

    end

    registration

      let A;

      cluster ( vSUB A) -> functional;

      coherence ;

    end

    reserve Sub for CQC_Substitution of A;

    definition

      let A;

      let Sub;

      :: SUBSTUT1:def2

      func @ Sub -> PartFunc of ( bound_QC-variables A), ( bound_QC-variables A) equals Sub;

      coherence by PARTFUN1: 47;

    end

    theorem :: SUBSTUT1:1

    

     Th1: a in ( dom Sub) implies (Sub . a) in ( bound_QC-variables A)

    proof

      assume a in ( dom Sub);

      then a in ( dom ( @ Sub));

      hence thesis by PARTFUN1: 4;

    end;

    definition

      let A;

      let l be FinSequence of ( QC-variables A);

      let Sub;

      :: SUBSTUT1:def3

      func CQC_Subst (l,Sub) -> FinSequence of ( QC-variables A) means

      : Def3: ( len it ) = ( len l) & for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom Sub) implies (it . k) = (Sub . (l . k))) & ( not (l . k) in ( dom Sub) implies (it . k) = (l . k));

      existence

      proof

        defpred P[ set, object] means ((l . $1) in ( dom Sub) implies $2 = (Sub . (l . $1))) & ( not (l . $1) in ( dom Sub) implies $2 = (l . $1));

        

         A1: for k be Nat st k in ( Seg ( len l)) holds ex y be object st P[k, y]

        proof

          let k be Nat;

          assume k in ( Seg ( len l));

          (l . k) in ( dom Sub) implies thesis;

          hence thesis;

        end;

        consider s be FinSequence such that

         A2: ( dom s) = ( Seg ( len l)) and

         A3: for k be Nat st k in ( Seg ( len l)) holds P[k, (s . k)] from FINSEQ_1:sch 1( A1);

        ( rng s) c= ( QC-variables A)

        proof

          let y be object;

          assume y in ( rng s);

          then

          consider x be object such that

           A4: x in ( dom s) and

           A5: (s . x) = y by FUNCT_1:def 3;

          reconsider x as Nat by A4;

          now

            per cases ;

              case

               A6: (l . x) in ( dom Sub);

              then (s . x) = (Sub . (l . x)) by A2, A3, A4;

              hence (s . x) in ( bound_QC-variables A) by A6, Th1;

            end;

              case

               A7: not (l . x) in ( dom Sub);

              x in ( dom l) by A2, A4, FINSEQ_1:def 3;

              then

               A8: (l . x) in ( rng l) by FUNCT_1: 3;

              (s . x) = (l . x) by A2, A3, A4, A7;

              hence (s . x) in ( QC-variables A) by A8;

            end;

          end;

          hence thesis by A5;

        end;

        then

        reconsider s as FinSequence of ( QC-variables A) by FINSEQ_1:def 4;

        take s;

        thus ( len s) = ( len l) by A2, FINSEQ_1:def 3;

        thus for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom Sub) implies (s . k) = (Sub . (l . k))) & ( not (l . k) in ( dom Sub) implies (s . k) = (l . k))

        proof

          let k;

          assume 1 <= k & k <= ( len l);

          then k in ( dom l) by FINSEQ_3: 25;

          then k in ( Seg ( len l)) by FINSEQ_1:def 3;

          hence thesis by A3;

        end;

      end;

      uniqueness

      proof

        let l1, l2 such that

         A9: ( len l1) = ( len l) and

         A10: for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom Sub) implies (l1 . k) = (Sub . (l . k))) & ( not (l . k) in ( dom Sub) implies (l1 . k) = (l . k)) and

         A11: ( len l2) = ( len l) and

         A12: for k st 1 <= k & k <= ( len l) holds ((l . k) in ( dom Sub) implies (l2 . k) = (Sub . (l . k))) & ( not (l . k) in ( dom Sub) implies (l2 . k) = (l . k));

        now

          let k be Nat;

          assume

           A13: 1 <= k & k <= ( len l);

          

           A14: not (l . k) in ( dom Sub) implies (l1 . k) = (l . k) by A10, A13;

          (l . k) in ( dom Sub) implies (l1 . k) = (Sub . (l . k)) by A10, A13;

          hence (l1 . k) = (l2 . k) by A12, A13, A14;

        end;

        hence thesis by A9, A11, FINSEQ_1: 14;

      end;

    end

    definition

      let A;

      let l be FinSequence of ( bound_QC-variables A);

      :: SUBSTUT1:def4

      func @ l -> FinSequence of ( QC-variables A) equals l;

      coherence

      proof

        ( rng l) c= ( QC-variables A) by XBOOLE_1: 1;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let A;

      let l be FinSequence of ( bound_QC-variables A);

      let Sub;

      :: SUBSTUT1:def5

      func CQC_Subst (l,Sub) -> FinSequence of ( bound_QC-variables A) equals ( CQC_Subst (( @ l),Sub));

      coherence

      proof

        ( len ( CQC_Subst (( @ l),Sub))) = ( len ( @ l)) by Def3;

        then

         A1: ( dom ( CQC_Subst (( @ l),Sub))) = ( Seg ( len ( @ l))) by FINSEQ_1:def 3;

        

         A2: for k st k in ( Seg ( len ( @ l))) holds ((( @ l) . k) in ( dom Sub) implies (( CQC_Subst (( @ l),Sub)) . k) = (Sub . (( @ l) . k))) & ( not (( @ l) . k) in ( dom Sub) implies (( CQC_Subst (( @ l),Sub)) . k) = (( @ l) . k))

        proof

          let k;

          assume k in ( Seg ( len ( @ l)));

          then 1 <= k & k <= ( len ( @ l)) by FINSEQ_1: 1;

          hence thesis by Def3;

        end;

        ( rng ( CQC_Subst (( @ l),Sub))) c= ( bound_QC-variables A)

        proof

          let y be object;

          assume y in ( rng ( CQC_Subst (( @ l),Sub)));

          then

          consider x be object such that

           A3: x in ( dom ( CQC_Subst (( @ l),Sub))) and

           A4: (( CQC_Subst (( @ l),Sub)) . x) = y by FUNCT_1:def 3;

          reconsider x as Nat by A3;

          now

            per cases ;

              case

               A5: (( @ l) . x) in ( dom Sub);

              then (( CQC_Subst (( @ l),Sub)) . x) = (Sub . (( @ l) . x)) by A1, A2, A3;

              hence (( CQC_Subst (( @ l),Sub)) . x) in ( bound_QC-variables A) by A5, Th1;

            end;

              case

               A6: not (( @ l) . x) in ( dom Sub);

              

               A7: ( rng l) c= ( bound_QC-variables A);

              x in ( dom ( @ l)) by A1, A3, FINSEQ_1:def 3;

              then

               A8: (( @ l) . x) in ( rng ( @ l)) by FUNCT_1: 3;

              (( CQC_Subst (( @ l),Sub)) . x) = (( @ l) . x) by A1, A2, A3, A6;

              hence (( CQC_Subst (( @ l),Sub)) . x) in ( bound_QC-variables A) by A8, A7;

            end;

          end;

          hence thesis by A4;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let A;

      let Sub;

      let X be set;

      :: original: |

      redefine

      func Sub | X -> CQC_Substitution of A ;

      coherence

      proof

        (Sub | X) = (( @ Sub) | X);

        hence thesis by PARTFUN1: 45;

      end;

    end

    registration

      let A;

      cluster finite for CQC_Substitution of A;

      existence

      proof

        take L = {} ;

        L is PartFunc of ( bound_QC-variables A), ( bound_QC-variables A) by RELSET_1: 12;

        hence L is CQC_Substitution of A by PARTFUN1: 45;

        thus thesis;

      end;

    end

    definition

      let A;

      let x, p, Sub;

      :: SUBSTUT1:def6

      func RestrictSub (x,p,Sub) -> finite CQC_Substitution of A equals (Sub | { y : y in ( still_not-bound_in p) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) });

      coherence

      proof

        set Y = { y : y is Element of ( dom Sub) & y <> x & y <> (Sub . y) };

        set X = { y : y in ( still_not-bound_in p) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) };

        reconsider Z = ( still_not-bound_in p) as finite set by CQC_SIM1: 19;

        for a be object holds (a in X iff a in (Z /\ Y))

        proof

          let a be object;

          thus a in X implies a in (Z /\ Y)

          proof

            assume a in X;

            then

            consider y such that

             A1: a = y & y in ( still_not-bound_in p) and

             A2: y is Element of ( dom Sub) & y <> x & y <> (Sub . y);

            y in Y by A2;

            hence thesis by A1, XBOOLE_0:def 4;

          end;

          thus a in (Z /\ Y) implies a in X

          proof

            assume

             A3: a in (Z /\ Y);

            then a in Y by XBOOLE_0:def 4;

            then

             A4: ex y st a = y & y is Element of ( dom Sub) & y <> x & y <> (Sub . y);

            a in Z by A3, XBOOLE_0:def 4;

            hence thesis by A4;

          end;

        end;

        then

        reconsider X as finite set by TARSKI: 2;

        (Sub | X) is finite;

        hence thesis;

      end;

    end

    definition

      let A;

      let l1;

      :: SUBSTUT1:def7

      func Bound_Vars (l1) -> Subset of ( bound_QC-variables A) equals { (l1 . k) : 1 <= k & k <= ( len l1) & (l1 . k) in ( bound_QC-variables A) };

      coherence

      proof

        set A2 = { (l1 . k) : 1 <= k & k <= ( len l1) & (l1 . k) in ( bound_QC-variables A) };

        A2 c= ( bound_QC-variables A)

        proof

          let x be object;

          assume x in A2;

          then ex k st (l1 . k) = x & 1 <= k & k <= ( len l1) & (l1 . k) in ( bound_QC-variables A);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let A;

      let p;

      :: SUBSTUT1:def8

      func Bound_Vars (p) -> Subset of ( bound_QC-variables A) means

      : Def8: ex F be Function of ( QC-WFF A), ( bool ( bound_QC-variables A)) st it = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} ( bound_QC-variables A))) & (p is atomic implies (F . p) = ( Bound_Vars ( the_arguments_of p))) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = d1) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = (d1 \/ d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = (d1 \/ {( bound_in p)}));

      correctness

      proof

        deffunc A( Element of ( QC-WFF A)) = ( Bound_Vars ( the_arguments_of $1));

        set V = ( bound_QC-variables A);

        deffunc N( Subset of V) = $1;

        deffunc C( Subset of V, Subset of V) = ($1 \/ $2);

        deffunc Q( Element of ( QC-WFF A), Subset of V) = ($2 \/ {( bound_in $1)});

        thus (ex d be Subset of V, F be Function of ( QC-WFF A), ( bool V) st d = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & for x1,x2 be Subset of V st (ex F be Function of ( QC-WFF A), ( bool V) st x1 = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) & (ex F be Function of ( QC-WFF A), ( bool V) st x2 = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of V holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1))) holds x1 = x2 from QC_LANG3:sch 2;

      end;

    end

    

     Lm1: ( Bound_Vars ( VERUM A)) = ( {} ( bound_QC-variables A)) & (p is atomic implies ( Bound_Vars p) = ( Bound_Vars ( the_arguments_of p))) & (p is negative implies ( Bound_Vars p) = ( Bound_Vars ( the_argument_of p))) & (p is conjunctive implies ( Bound_Vars p) = (( Bound_Vars ( the_left_argument_of p)) \/ ( Bound_Vars ( the_right_argument_of p)))) & (p is universal implies ( Bound_Vars p) = (( Bound_Vars ( the_scope_of p)) \/ {( bound_in p)}))

    proof

      deffunc A( Element of ( QC-WFF A)) = ( Bound_Vars ( the_arguments_of $1));

      deffunc F1( Element of ( QC-WFF A)) = ( Bound_Vars $1);

      set V = ( bound_QC-variables A);

      deffunc N( Subset of V) = $1;

      deffunc C( Subset of V, Subset of V) = ($1 \/ $2);

      deffunc Q( Element of ( QC-WFF A), Subset of V) = ($2 \/ {( bound_in $1)});

      

       A1: for p be QC-formula of A, X be Subset of V holds X = F1(p) iff ex F be Function of ( QC-WFF A), ( bool V) st X = (F . p) & for p be Element of ( QC-WFF A) holds for d1,d2 be Subset of ( bound_QC-variables A) holds (p = ( VERUM A) implies (F . p) = ( {} V)) & (p is atomic implies (F . p) = A(p)) & (p is negative & d1 = (F . ( the_argument_of p)) implies (F . p) = N(d1)) & (p is conjunctive & d1 = (F . ( the_left_argument_of p)) & d2 = (F . ( the_right_argument_of p)) implies (F . p) = C(d1,d2)) & (p is universal & d1 = (F . ( the_scope_of p)) implies (F . p) = Q(p,d1)) by Def8;

       F1(VERUM) = ( {} V) from QC_LANG3:sch 3( A1)

      .= {} ;

      hence ( Bound_Vars ( VERUM A)) = ( {} ( bound_QC-variables A));

      thus p is atomic implies ( Bound_Vars p) = ( Bound_Vars ( the_arguments_of p))

      proof

        assume

         A2: p is atomic;

        thus F1(p) = A(p) from QC_LANG3:sch 4( A1, A2);

      end;

      thus p is negative implies ( Bound_Vars p) = ( Bound_Vars ( the_argument_of p))

      proof

        assume

         A3: p is negative;

        thus F1(p) = N(F1) from QC_LANG3:sch 5( A1, A3);

      end;

      thus p is conjunctive implies ( Bound_Vars p) = (( Bound_Vars ( the_left_argument_of p)) \/ ( Bound_Vars ( the_right_argument_of p)))

      proof

        assume

         A4: p is conjunctive;

        for d1,d2 be Subset of V st d1 = F1(the_left_argument_of) & d2 = F1(the_right_argument_of) holds F1(p) = C(d1,d2) from QC_LANG3:sch 6( A1, A4);

        hence thesis;

      end;

      thus p is universal implies ( Bound_Vars p) = (( Bound_Vars ( the_scope_of p)) \/ {( bound_in p)})

      proof

        assume

         A5: p is universal;

        thus F1(p) = Q(p,F1) from QC_LANG3:sch 7( A1, A5);

      end;

    end;

    theorem :: SUBSTUT1:2

    

     Th2: ( Bound_Vars ( VERUM A)) = {}

    proof

      ( Bound_Vars ( VERUM A)) = ( {} ( bound_QC-variables A)) by Lm1;

      hence ( Bound_Vars ( VERUM A)) = {} ;

    end;

    theorem :: SUBSTUT1:3

    for p be QC-formula of A st p is atomic holds ( Bound_Vars p) = ( Bound_Vars ( the_arguments_of p)) by Lm1;

    theorem :: SUBSTUT1:4

    for p be QC-formula of A st p is negative holds ( Bound_Vars p) = ( Bound_Vars ( the_argument_of p)) by Lm1;

    theorem :: SUBSTUT1:5

    for p be QC-formula of A st p is conjunctive holds ( Bound_Vars p) = (( Bound_Vars ( the_left_argument_of p)) \/ ( Bound_Vars ( the_right_argument_of p))) by Lm1;

    theorem :: SUBSTUT1:6

    for p be QC-formula of A st p is universal holds ( Bound_Vars p) = (( Bound_Vars ( the_scope_of p)) \/ {( bound_in p)}) by Lm1;

    registration

      let A;

      let p;

      cluster ( Bound_Vars p) -> finite;

      coherence

      proof

        defpred P[ Element of ( QC-WFF A)] means ( Bound_Vars $1) is finite;

        

         A1: for p be Element of ( QC-WFF A) holds (p is atomic implies P[p]) & P[( VERUM A)] & (p is negative & P[( the_argument_of p)] implies P[p]) & (p is conjunctive & P[( the_left_argument_of p)] & P[( the_right_argument_of p)] implies P[p]) & (p is universal & P[( the_scope_of p)] implies P[p])

        proof

          let p be Element of ( QC-WFF A);

          thus p is atomic implies ( Bound_Vars p) is finite

          proof

            deffunc F( set) = (( the_arguments_of p) . $1);

            defpred B[ Nat] means 1 <= $1 & $1 <= ( len ( the_arguments_of p));

            defpred A[ Nat] means 1 <= $1 & $1 <= ( len ( the_arguments_of p)) & (( the_arguments_of p) . $1) in ( bound_QC-variables A);

            

             A2: { F(k) : A[k] } c= { F(n) : B[n] }

            proof

              let e be object;

              assume e in { F(k) : A[k] };

              then ex k st e = F(k) & A[k];

              hence thesis;

            end;

            assume p is atomic;

            

            then ( Bound_Vars p) = ( Bound_Vars ( the_arguments_of p)) by Lm1

            .= { (( the_arguments_of p) . k) : 1 <= k & k <= ( len ( the_arguments_of p)) & (( the_arguments_of p) . k) in ( bound_QC-variables A) };

            then ( Bound_Vars p) c= ( rng ( the_arguments_of p)) by A2, CQC_SIM1: 9;

            hence thesis;

          end;

          thus ( Bound_Vars ( VERUM A)) is finite by Th2;

          thus p is negative & ( Bound_Vars ( the_argument_of p)) is finite implies ( Bound_Vars p) is finite by Lm1;

          thus p is conjunctive & ( Bound_Vars ( the_left_argument_of p)) is finite & ( Bound_Vars ( the_right_argument_of p)) is finite implies ( Bound_Vars p) is finite

          proof

            assume that

             A3: p is conjunctive and

             A4: ( Bound_Vars ( the_left_argument_of p)) is finite & ( Bound_Vars ( the_right_argument_of p)) is finite;

            ( Bound_Vars p) = (( Bound_Vars ( the_left_argument_of p)) \/ ( Bound_Vars ( the_right_argument_of p))) by A3, Lm1;

            hence thesis by A4;

          end;

          assume that

           A5: p is universal and

           A6: ( Bound_Vars ( the_scope_of p)) is finite;

          ( Bound_Vars p) = (( Bound_Vars ( the_scope_of p)) \/ {( bound_in p)}) by A5, Lm1;

          hence thesis by A6;

        end;

        for p be Element of ( QC-WFF A) holds P[p] from QC_LANG1:sch 2( A1);

        hence thesis;

      end;

    end

    definition

      let A;

      let p;

      :: SUBSTUT1:def9

      func Dom_Bound_Vars (p) -> finite Subset of ( QC-symbols A) equals { s : ( x. s) in ( Bound_Vars p) };

      coherence

      proof

        defpred P[ object, object] means ex s st s = $1 & $2 = ( x. s);

        set X = { s : ( x. s) in ( Bound_Vars p) };

        

         A1: X c= ( QC-symbols A)

        proof

          let a be object;

          assume a in X;

          then ex s st a = s & ( x. s) in ( Bound_Vars p);

          hence thesis;

        end;

        

         A2: for a be object st a in ( QC-symbols A) holds ex b be object st P[a, b]

        proof

          let a be object;

          assume a in ( QC-symbols A);

          then

          reconsider s = a as QC-symbol of A;

          take ( x. s);

          take s;

          thus thesis;

        end;

        consider f be Function such that

         A3: ( dom f) = ( QC-symbols A) & for a be object st a in ( QC-symbols A) holds P[a, (f . a)] from CLASSES1:sch 1( A2);

        

         A4: ( rng (f | X)) c= ( Bound_Vars p)

        proof

          let b be object;

          assume b in ( rng (f | X));

          then

          consider a be object such that

           A5: a in ( dom (f | X)) and

           A6: b = ((f | X) . a) by FUNCT_1:def 3;

          a in X by A5, RELAT_1: 57;

          then

           A7: ex s st a = s & ( x. s) in ( Bound_Vars p);

          b = (f . a) & a in ( dom f) by A5, A6, FUNCT_1: 47, RELAT_1: 57;

          then ex s st s = a & b = ( x. s) by A3;

          hence thesis by A7;

        end;

        f is one-to-one

        proof

          let a1,a2 be object such that

           A8: a1 in ( dom f) & a2 in ( dom f) and

           A9: (f . a1) = (f . a2);

          (ex s st s = a1 & (f . a1) = ( x. s)) & ex t st t = a2 & (f . a2) = ( x. t) by A3, A8;

          hence thesis by A9, XTUPLE_0: 1;

        end;

        then (f | X) is one-to-one by FUNCT_1: 52;

        then

         A10: ( dom (f | X)) is finite by A4, CARD_1: 59;

        reconsider X as Subset of ( QC-symbols A) by A1;

        for a be object holds a in ( dom (f | X)) iff a in X & a in ( dom f) by RELAT_1: 57;

        then ( dom (f | X)) = (X /\ ( QC-symbols A)) by A3, XBOOLE_0:def 4;

        hence thesis by A10, XBOOLE_1: 28;

      end;

    end

    reserve finSub for finite CQC_Substitution of A;

    definition

      let A;

      let finSub;

      :: SUBSTUT1:def10

      func Sub_Var (finSub) -> finite Subset of ( QC-symbols A) equals { s : ( x. s) in ( rng finSub) };

      coherence

      proof

        defpred P[ object, object] means ex s st s = $1 & $2 = ( x. s);

        set X = { s : ( x. s) in ( rng finSub) };

        

         A1: X c= ( QC-symbols A)

        proof

          let a be object;

          assume a in X;

          then ex s st a = s & ( x. s) in ( rng finSub);

          hence thesis;

        end;

        

         A2: for a be object st a in ( QC-symbols A) holds ex b be object st P[a, b]

        proof

          let a be object;

          assume a in ( QC-symbols A);

          then

          reconsider s = a as QC-symbol of A;

          take ( x. s);

          take s;

          thus thesis;

        end;

        consider f be Function such that

         A3: ( dom f) = ( QC-symbols A) & for a be object st a in ( QC-symbols A) holds P[a, (f . a)] from CLASSES1:sch 1( A2);

        

         A4: ( rng (f | X)) c= ( rng finSub)

        proof

          let b be object;

          assume b in ( rng (f | X));

          then

          consider a be object such that

           A5: a in ( dom (f | X)) and

           A6: b = ((f | X) . a) by FUNCT_1:def 3;

          a in X by A5, RELAT_1: 57;

          then

           A7: ex s st a = s & ( x. s) in ( rng finSub);

          b = (f . a) & a in ( dom f) by A5, A6, FUNCT_1: 47, RELAT_1: 57;

          then ex s st s = a & b = ( x. s) by A3;

          hence thesis by A7;

        end;

        f is one-to-one

        proof

          let a1,a2 be object such that

           A8: a1 in ( dom f) & a2 in ( dom f) and

           A9: (f . a1) = (f . a2);

          (ex s st s = a1 & (f . a1) = ( x. s)) & ex t st t = a2 & (f . a2) = ( x. t) by A3, A8;

          hence thesis by A9, XTUPLE_0: 1;

        end;

        then (f | X) is one-to-one by FUNCT_1: 52;

        then

         A10: ( dom (f | X)) is finite by A4, CARD_1: 59;

        reconsider X as Subset of ( QC-symbols A) by A1;

        for a be object holds a in ( dom (f | X)) iff a in X & a in ( dom f) by RELAT_1: 57;

        then ( dom (f | X)) = (X /\ ( QC-symbols A)) by A3, XBOOLE_0:def 4;

        hence thesis by A10, XBOOLE_1: 28;

      end;

    end

    

     Lm2: for X,Y be set st ( card X) in ( card Y) holds (Y \ X) <> {}

    proof

      let X,Y be set;

      assume that

       A1: ( card X) in ( card Y) and

       A2: (Y \ X) = {} ;

      Y c= X by A2, XBOOLE_1: 37;

      then ( card Y) c= ( card X) by CARD_1: 11;

      hence contradiction by A1, CARD_1: 4;

    end;

    definition

      let A;

      let p, finSub;

      :: SUBSTUT1:def11

      func NSub (p,finSub) -> non empty Subset of ( QC-symbols A) equals ( NAT \ (( Dom_Bound_Vars p) \/ ( Sub_Var finSub)));

      coherence

      proof

        set X = (( Dom_Bound_Vars p) \/ ( Sub_Var finSub));

        ( card (( Dom_Bound_Vars p) \/ ( Sub_Var finSub))) in ( card NAT ) by CARD_3: 42;

        hence ( NAT \ (( Dom_Bound_Vars p) \/ ( Sub_Var finSub))) is non empty Subset of ( QC-symbols A) by Lm2, QC_LANG1: 3, XBOOLE_1: 109;

      end;

    end

    definition

      let A;

      let finSub, p;

      :: SUBSTUT1:def12

      func upVar (finSub,p) -> QC-symbol of A equals the Element of ( NSub (p,finSub));

      coherence ;

    end

    definition

      let A;

      let x, p, finSub;

      assume

       A1: ex Sub st finSub = ( RestrictSub (x,( All (x,p)),Sub));

      :: SUBSTUT1:def13

      func ExpandSub (x,p,finSub) -> CQC_Substitution of A equals (finSub \/ { [x, ( x. ( upVar (finSub,p)))]}) if x in ( rng finSub)

      otherwise (finSub \/ { [x, x]});

      coherence

      proof

         A2:

        now

          reconsider Z = { [x, x]} as Relation-like set;

          assume not x in ( rng finSub);

           A3:

          now

            consider Sub such that

             A4: finSub = ( RestrictSub (x,( All (x,p)),Sub)) by A1;

            set X = { y : y in ( still_not-bound_in ( All (x,p))) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) };

            

             A5: ( dom finSub) c= X by A4, RELAT_1: 58;

            given a such that

             A6: a in (( dom finSub) /\ ( dom Z));

            a in ( dom finSub) by A6, XBOOLE_0:def 4;

            then a in X by A5;

            then

             A7: ( dom Z) = {x} & ex y st a = y & y in ( still_not-bound_in ( All (x,p))) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) by RELAT_1: 9;

            a in ( dom Z) by A6, XBOOLE_0:def 4;

            hence contradiction by A7, TARSKI:def 1;

          end;

          reconsider Z as Function;

          for a be object st a in (( dom ( @ finSub)) /\ ( dom Z)) holds (( @ finSub) . a) = (Z . a) by A3;

          then

          reconsider h = (( @ finSub) \/ Z) as Function by PARTFUN1: 1;

          reconsider Z as Relation of ( bound_QC-variables A), ( bound_QC-variables A);

          (( @ finSub) \/ Z) = h;

          hence (finSub \/ { [x, x]}) is CQC_Substitution of A by PARTFUN1: 45;

        end;

        now

          reconsider Z = { [x, ( x. ( upVar (finSub,p)))]} as Relation-like set;

          assume x in ( rng finSub);

           A9:

          now

            consider Sub such that

             A10: finSub = ( RestrictSub (x,( All (x,p)),Sub)) by A1;

            set X = { y : y in ( still_not-bound_in ( All (x,p))) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) };

            

             A11: ( dom finSub) c= X by A10, RELAT_1: 58;

            given a such that

             A12: a in (( dom finSub) /\ ( dom Z));

            a in ( dom finSub) by A12, XBOOLE_0:def 4;

            then a in X by A11;

            then

             A13: ( dom Z) = {x} & ex y st a = y & y in ( still_not-bound_in ( All (x,p))) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y) by RELAT_1: 9;

            a in ( dom Z) by A12, XBOOLE_0:def 4;

            hence contradiction by A13, TARSKI:def 1;

          end;

          reconsider Z as Function;

          for a be object st a in (( dom ( @ finSub)) /\ ( dom Z)) holds (( @ finSub) . a) = (Z . a) by A9;

          then

          reconsider h = (( @ finSub) \/ Z) as Function by PARTFUN1: 1;

          reconsider Z as Relation of ( bound_QC-variables A), ( bound_QC-variables A);

          (( @ finSub) \/ Z) = h;

          hence (finSub \/ { [x, ( x. ( upVar (finSub,p)))]}) is CQC_Substitution of A by PARTFUN1: 45;

        end;

        hence thesis by A2;

      end;

      consistency ;

    end

    definition

      let A;

      let p, Sub;

      let b be object;

      :: SUBSTUT1:def14

      pred p,Sub PQSub b means (p is universal implies b = ( ExpandSub (( bound_in p),( the_scope_of p),( RestrictSub (( bound_in p),p,Sub))))) & ( not p is universal implies b = {} );

    end

    definition

      let A;

      :: SUBSTUT1:def15

      func QSub (A) -> Function means a in it iff ex p, Sub, b st a = [ [p, Sub], b] & (p,Sub) PQSub b;

      existence

      proof

        defpred P[ object, object] means ex p, Sub st $1 = [p, Sub] & (p,Sub) PQSub $2;

        

         A1: for a,b1,b2 be object st P[a, b1] & P[a, b2] holds b1 = b2

        proof

          let a,b1,b2 be object such that

           A2: ex p, Sub st a = [p, Sub] & (p,Sub) PQSub b1 and

           A3: ex p, Sub st a = [p, Sub] & (p,Sub) PQSub b2;

          consider p1 be QC-formula of A, Sub1 be CQC_Substitution of A such that

           A4: a = [p1, Sub1] and

           A5: (p1,Sub1) PQSub b1 by A2;

          consider p2 be QC-formula of A, Sub2 be CQC_Substitution of A such that

           A6: a = [p2, Sub2] and

           A7: (p2,Sub2) PQSub b2 by A3;

          

           A8: p1 = p2 by A4, A6, XTUPLE_0: 1;

          

           A9: Sub1 = Sub2 by A4, A6, XTUPLE_0: 1;

          per cases ;

            suppose

             A10: p1 is universal;

            then b1 = ( ExpandSub (( bound_in p1),( the_scope_of p1),( RestrictSub (( bound_in p1),p1,Sub1)))) by A5;

            hence thesis by A7, A8, A9, A10;

          end;

            suppose

             A11: not p1 is universal;

            then b1 = {} by A5;

            hence thesis by A7, A8, A11;

          end;

        end;

        consider f be Function such that

         A12: for a,b be object holds [a, b] in f iff a in [:( QC-WFF A), ( vSUB A):] & P[a, b] from FUNCT_1:sch 1( A1);

        take f;

        c in f iff ex p, Sub, b st c = [ [p, Sub], b] & (p,Sub) PQSub b

        proof

          thus c in f implies ex p, Sub, b st c = [ [p, Sub], b] & (p,Sub) PQSub b

          proof

            assume

             A13: c in f;

            then

            consider a,b be object such that

             A14: c = [a, b] by RELAT_1:def 1;

            ex p, Sub st a = [p, Sub] & (p,Sub) PQSub b by A12, A13, A14;

            hence thesis by A14;

          end;

          thus thesis by A12;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function;

        assume that

         A15: for a holds a in F1 iff ex p, Sub, b st a = [ [p, Sub], b] & (p,Sub) PQSub b and

         A16: for a holds a in F2 iff ex p, Sub, b st a = [ [p, Sub], b] & (p,Sub) PQSub b;

        now

          let a be object;

          a in F1 iff ex p, Sub, b st a = [ [p, Sub], b] & (p,Sub) PQSub b by A15;

          hence a in F1 iff a in F2 by A16;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    begin

    reserve e for Element of ( vSUB A);

    theorem :: SUBSTUT1:7

    

     Th7: [:( QC-WFF A), ( vSUB A):] is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & (for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in [:( QC-WFF A), ( vSUB A):]) & (for e be Element of ( vSUB A) holds [ <* [ 0 , 0 ]*>, e] in [:( QC-WFF A), ( vSUB A):]) & (for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] holds [( <* [1, 0 ]*> ^ p), e] in [:( QC-WFF A), ( vSUB A):]) & (for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] & [q, e] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in [:( QC-WFF A), ( vSUB A):]) & (for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in [:( QC-WFF A), ( vSUB A):])

    proof

      ( QC-WFF A) is A -closed by QC_LANG1: 7;

      then ( QC-WFF A) is Subset of ( [: NAT , ( QC-symbols A):] * );

      hence [:( QC-WFF A), ( vSUB A):] is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] by ZFMISC_1: 95;

      thus (for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in [:( QC-WFF A), ( vSUB A):])

      proof

        let k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A);

        (p ! ll) = ( <*p*> ^ ll) by QC_LANG1: 8;

        hence thesis by ZFMISC_1:def 2;

      end;

      ( VERUM A) in ( QC-WFF A);

      hence for e be Element of ( vSUB A) holds [ <* [ 0 , 0 ]*>, e] in [:( QC-WFF A), ( vSUB A):] by ZFMISC_1:def 2;

      thus for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] holds [( <* [1, 0 ]*> ^ p), e] in [:( QC-WFF A), ( vSUB A):]

      proof

        let p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A);

        assume [p, e] in [:( QC-WFF A), ( vSUB A):];

        then ex a,b be object st a in ( QC-WFF A) & b in ( vSUB A) & [p, e] = [a, b] by ZFMISC_1:def 2;

        then

        reconsider p9 = p as Element of ( QC-WFF A) by XTUPLE_0: 1;

        ( 'not' p9) = ( <* [1, 0 ]*> ^ ( @ p9));

        hence thesis by ZFMISC_1:def 2;

      end;

      thus for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] & [q, e] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in [:( QC-WFF A), ( vSUB A):]

      proof

        let p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A);

        assume that

         A1: [p, e] in [:( QC-WFF A), ( vSUB A):] and

         A2: [q, e] in [:( QC-WFF A), ( vSUB A):];

        ex c,d be object st c in ( QC-WFF A) & d in ( vSUB A) & [q, e] = [c, d] by A2, ZFMISC_1:def 2;

        then

        reconsider q9 = q as Element of ( QC-WFF A) by XTUPLE_0: 1;

        ex a,b be object st a in ( QC-WFF A) & b in ( vSUB A) & [p, e] = [a, b] by A1, ZFMISC_1:def 2;

        then

        reconsider p9 = p as Element of ( QC-WFF A) by XTUPLE_0: 1;

        (p9 '&' q9) = (( <* [2, 0 ]*> ^ ( @ p9)) ^ ( @ q9));

        hence thesis by ZFMISC_1:def 2;

      end;

      thus for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in [:( QC-WFF A), ( vSUB A):]

      proof

        let x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A);

        assume [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in [:( QC-WFF A), ( vSUB A):];

        then ex a,b be object st a in ( QC-WFF A) & b in ( vSUB A) & [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] = [a, b] by ZFMISC_1:def 2;

        then

        reconsider p9 = p as Element of ( QC-WFF A) by XTUPLE_0: 1;

        ( All (x,p9)) = (( <* [3, 0 ]*> ^ <*x*>) ^ ( @ p9));

        hence thesis by ZFMISC_1:def 2;

      end;

    end;

    definition

      let A;

      let IT be set;

      :: SUBSTUT1:def16

      attr IT is A -Sub-closed means

      : Def16: IT is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & (for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in IT) & (for e be Element of ( vSUB A) holds [ <* [ 0 , 0 ]*>, e] in IT) & (for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in IT holds [( <* [1, 0 ]*> ^ p), e] in IT) & (for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in IT & [q, e] in IT holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in IT) & (for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in IT holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in IT);

    end

    registration

      let A;

      cluster A -Sub-closed non empty for set;

      existence

      proof

        take [:( QC-WFF A), ( vSUB A):];

         [:( QC-WFF A), ( vSUB A):] is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & (for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in [:( QC-WFF A), ( vSUB A):]) & (for e be Element of ( vSUB A) holds [ <* [ 0 , 0 ]*>, e] in [:( QC-WFF A), ( vSUB A):]) & (for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] holds [( <* [1, 0 ]*> ^ p), e] in [:( QC-WFF A), ( vSUB A):]) & (for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] & [q, e] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in [:( QC-WFF A), ( vSUB A):]) & (for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in [:( QC-WFF A), ( vSUB A):]) by Th7;

        hence thesis;

      end;

    end

    

     Lm3: for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):] holds (( <* [3, 0 ]*> ^ <*x*>) ^ p) is FinSequence of [: NAT , ( QC-symbols A):]

    proof

       0 in ( QC-symbols A) by QC_LANG1: 3;

      then [3, 0 ] in [: NAT , ( QC-symbols A):] by ZFMISC_1: 87;

      then ( rng <* [3, 0 ]*>) = { [3, 0 ]} & { [3, 0 ]} c= [: NAT , ( QC-symbols A):] by FINSEQ_1: 39, ZFMISC_1: 31;

      then

      reconsider y = <* [3, 0 ]*> as FinSequence of [: NAT , ( QC-symbols A):] by FINSEQ_1:def 4;

      let x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):];

      ( QC-variables A) c= [: NAT , ( QC-symbols A):] by QC_LANG1: 4;

      then ( bound_QC-variables A) c= [: NAT , ( QC-symbols A):];

      then ( rng <*x*>) c= [: NAT , ( QC-symbols A):];

      then

      reconsider z = <*x*> as FinSequence of [: NAT , ( QC-symbols A):] by FINSEQ_1:def 4;

      ((y ^ z) ^ p) is FinSequence of [: NAT , ( QC-symbols A):];

      hence thesis;

    end;

    

     Lm4: for k be Nat, l be QC-symbol of A, e be Element of ( vSUB A) holds [ <* [k, l]*>, e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):]

    proof

      let k be Nat;

      

       A1: k in NAT by ORDINAL1:def 12;

      let l be QC-symbol of A;

      let e;

      reconsider kl = [k, l] as Element of [: NAT , ( QC-symbols A):] by A1, ZFMISC_1:def 2;

       <*kl*> in ( [: NAT , ( QC-symbols A):] * ) by FINSEQ_1:def 11;

      hence thesis by ZFMISC_1:def 2;

    end;

    

     Lm5: for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):]

    proof

      let k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A;

      ( QC-pred_symbols A) c= [: NAT , ( QC-symbols A):] by QC_LANG1: 6;

      then (k -ary_QC-pred_symbols A) c= [: NAT , ( QC-symbols A):];

      then

       A1: ( rng <*p*>) c= [: NAT , ( QC-symbols A):];

      ( QC-variables A) c= [: NAT , ( QC-symbols A):] by QC_LANG1: 4;

      then ( rng ll) c= [: NAT , ( QC-symbols A):];

      then (( rng <*p*>) \/ ( rng ll)) c= [: NAT , ( QC-symbols A):] by A1, XBOOLE_1: 8;

      then ( rng ( <*p*> ^ ll)) c= [: NAT , ( QC-symbols A):] by FINSEQ_1: 31;

      then ( <*p*> ^ ll) is FinSequence of [: NAT , ( QC-symbols A):] by FINSEQ_1:def 4;

      then ( <*p*> ^ ll) in ( [: NAT , ( QC-symbols A):] * ) by FINSEQ_1:def 11;

      hence thesis by ZFMISC_1:def 2;

    end;

    definition

      let A;

      :: SUBSTUT1:def17

      func QC-Sub-WFF (A) -> non empty set means

      : Def17: it is A -Sub-closed & for D be non empty set st D is A -Sub-closed holds it c= D;

      existence

      proof

        set e = the Element of ( vSUB A);

        defpred P[ object] means for D be non empty set st D is A -Sub-closed holds $1 in D;

        consider D0 be set such that

         A1: for x be object holds x in D0 iff x in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & P[x] from XBOOLE_0:sch 1;

         0 in ( QC-symbols A) by QC_LANG1: 3;

        then [ <* [ 0 , 0 ]*>, e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & for D be non empty set st D is A -Sub-closed holds [ <* [ 0 , 0 ]*>, e] in D by Lm4;

        then

        reconsider D0 as non empty set by A1;

        take D0;

        D0 c= [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] by A1;

        hence D0 is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):];

        thus for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in D0

        proof

          let k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A);

           [( <*p*> ^ ll), e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & for D be non empty set st D is A -Sub-closed holds [( <*p*> ^ ll), e] in D by Lm5;

          hence thesis by A1;

        end;

        thus for e holds [ <* [ 0 , 0 ]*>, e] in D0

        proof

          let e;

           0 in ( QC-symbols A) by QC_LANG1: 3;

          then [ <* [ 0 , 0 ]*>, e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & for D be non empty set st D is A -Sub-closed holds [ <* [ 0 , 0 ]*>, e] in D by Lm4;

          hence thesis by A1;

        end;

        thus for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in D0 holds [( <* [1, 0 ]*> ^ p), e] in D0

        proof

          let p be FinSequence of [: NAT , ( QC-symbols A):];

          let e be Element of ( vSUB A);

          assume

           A2: [p, e] in D0;

          

           A3: for D be non empty set st D is A -Sub-closed holds [( <* [1, 0 ]*> ^ p), e] in D

          proof

            let D be non empty set;

            assume

             A4: D is A -Sub-closed;

            then [p, e] in D by A1, A2;

            hence thesis by A4;

          end;

           0 in ( QC-symbols A) by QC_LANG1: 3;

          then [1, 0 ] in [: NAT , ( QC-symbols A):] by ZFMISC_1: 87;

          then ( rng <* [1, 0 ]*>) = { [1, 0 ]} & { [1, 0 ]} c= [: NAT , ( QC-symbols A):] by FINSEQ_1: 39, ZFMISC_1: 31;

          then

          reconsider y = <* [1, 0 ]*> as FinSequence of [: NAT , ( QC-symbols A):] by FINSEQ_1:def 4;

          (y ^ p) is FinSequence of [: NAT , ( QC-symbols A):];

          then ( <* [1, 0 ]*> ^ p) in ( [: NAT , ( QC-symbols A):] * ) by FINSEQ_1:def 11;

          then [( <* [1, 0 ]*> ^ p), e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] by ZFMISC_1:def 2;

          hence thesis by A1, A3;

        end;

        thus for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in D0 & [q, e] in D0 holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in D0

        proof

          let p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) such that

           A5: [p, e] in D0 & [q, e] in D0;

          

           A6: for D be non empty set st D is A -Sub-closed holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in D

          proof

            let D be non empty set;

            assume

             A7: D is A -Sub-closed;

            then [p, e] in D & [q, e] in D by A1, A5;

            hence thesis by A7;

          end;

           0 in ( QC-symbols A) by QC_LANG1: 3;

          then [2, 0 ] in [: NAT , ( QC-symbols A):] by ZFMISC_1: 87;

          then ( rng <* [2, 0 ]*>) = { [2, 0 ]} & { [2, 0 ]} c= [: NAT , ( QC-symbols A):] by FINSEQ_1: 39, ZFMISC_1: 31;

          then

          reconsider y = <* [2, 0 ]*> as FinSequence of [: NAT , ( QC-symbols A):] by FINSEQ_1:def 4;

          ((y ^ p) ^ q) is FinSequence of [: NAT , ( QC-symbols A):];

          then (( <* [2, 0 ]*> ^ p) ^ q) in ( [: NAT , ( QC-symbols A):] * ) by FINSEQ_1:def 11;

          then [(( <* [2, 0 ]*> ^ p) ^ q), e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] by ZFMISC_1:def 2;

          hence thesis by A1, A6;

        end;

        thus for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in D0 holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in D0

        proof

          let x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A);

          assume

           A8: [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in D0;

          

           A9: for D be non empty set st D is A -Sub-closed holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in D

          proof

            let D be non empty set;

            assume

             A10: D is A -Sub-closed;

            then [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in D by A1, A8;

            hence thesis by A10;

          end;

          (( <* [3, 0 ]*> ^ <*x*>) ^ p) is FinSequence of [: NAT , ( QC-symbols A):] by Lm3;

          then (( <* [3, 0 ]*> ^ <*x*>) ^ p) in ( [: NAT , ( QC-symbols A):] * ) by FINSEQ_1:def 11;

          then [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] by ZFMISC_1:def 2;

          hence thesis by A1, A9;

        end;

        let D be non empty set such that

         A11: D is A -Sub-closed;

        let x be object;

        assume x in D0;

        hence thesis by A1, A11;

      end;

      uniqueness

      proof

        let D1,D2 be non empty set;

        assume D1 is A -Sub-closed & (for D be non empty set st D is A -Sub-closed holds D1 c= D) & D2 is A -Sub-closed & for D be non empty set st D is A -Sub-closed holds D2 c= D;

        then D1 c= D2 & D2 c= D1;

        hence thesis by XBOOLE_0:def 10;

      end;

    end

    reserve S,S9,S1,S2,S19,S29,T1,T2 for Element of ( QC-Sub-WFF A);

    theorem :: SUBSTUT1:8

    

     Th8: ex p, e st S = [p, e]

    proof

       [:( QC-WFF A), ( vSUB A):] is Subset of [:( [: NAT , ( QC-symbols A):] * ), ( vSUB A):] & (for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds [( <*p*> ^ ll), e] in [:( QC-WFF A), ( vSUB A):]) & (for e be Element of ( vSUB A) holds [ <* [ 0 , 0 ]*>, e] in [:( QC-WFF A), ( vSUB A):]) & (for p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] holds [( <* [1, 0 ]*> ^ p), e] in [:( QC-WFF A), ( vSUB A):]) & (for p,q be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, e] in [:( QC-WFF A), ( vSUB A):] & [q, e] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in [:( QC-WFF A), ( vSUB A):]) & (for x be bound_QC-variable of A, p be FinSequence of [: NAT , ( QC-symbols A):], e be Element of ( vSUB A) st [p, (( QSub A) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in [:( QC-WFF A), ( vSUB A):] holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in [:( QC-WFF A), ( vSUB A):]) by Th7;

      then [:( QC-WFF A), ( vSUB A):] is A -Sub-closed;

      then ( QC-Sub-WFF A) c= [:( QC-WFF A), ( vSUB A):] by Def17;

      then S in [:( QC-WFF A), ( vSUB A):];

      then

      consider a,b be object such that

       A1: a in ( QC-WFF A) and

       A2: b in ( vSUB A) and

       A3: S = [a, b] by ZFMISC_1:def 2;

      reconsider e = b as Element of ( vSUB A) by A2;

      reconsider p = a as Element of ( QC-WFF A) by A1;

      take p, e;

      thus thesis by A3;

    end;

    registration

      let A;

      cluster ( QC-Sub-WFF A) -> A -Sub-closed;

      coherence by Def17;

    end

    definition

      let A;

      let P be QC-pred_symbol of A;

      let l be FinSequence of ( QC-variables A);

      let e;

      assume

       A1: ( the_arity_of P) = ( len l);

      :: SUBSTUT1:def18

      func Sub_P (P,l,e) -> Element of ( QC-Sub-WFF A) equals

      : Def18: [(P ! l), e];

      coherence

      proof

        set k = ( len l);

        set QCP = { QP where QP be QC-pred_symbol of A : ( the_arity_of QP) = k };

        P in QCP by A1;

        then

        reconsider P as QC-pred_symbol of k, A;

        reconsider l as QC-variable_list of k, A by CARD_1:def 7;

        (P ! l) = ( <*P*> ^ l) by QC_LANG1: 8;

        hence thesis by Def16;

      end;

    end

    theorem :: SUBSTUT1:9

    

     Th9: for k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A holds ( Sub_P (P,ll,e)) = [(P ! ll), e]

    proof

      let k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A;

      set QCP = { QP where QP be QC-pred_symbol of A : ( the_arity_of QP) = k };

      P in QCP;

      then

       A1: ex Q be QC-pred_symbol of A st P = Q & ( the_arity_of Q) = k;

      ( len ll) = k by CARD_1:def 7;

      hence thesis by A1, Def18;

    end;

    definition

      let A;

      let S;

      :: SUBSTUT1:def19

      attr S is A -Sub_VERUM means ex e st S = [( VERUM A), e];

    end

    definition

      let A;

      let S;

      :: original: `1

      redefine

      func S `1 -> Element of ( QC-WFF A) ;

      coherence

      proof

        ex p, e st S = [p, e] by Th8;

        hence thesis;

      end;

      :: original: `2

      redefine

      func S `2 -> Element of ( vSUB A) ;

      coherence

      proof

        ex p, e st S = [p, e] by Th8;

        hence thesis;

      end;

    end

    theorem :: SUBSTUT1:10

    

     Th10: S = [(S `1 ), (S `2 )]

    proof

      ex p, e st S = [p, e] by Th8;

      hence thesis;

    end;

    definition

      let A;

      let S;

      :: SUBSTUT1:def20

      func Sub_not S -> Element of ( QC-Sub-WFF A) equals [( 'not' (S `1 )), (S `2 )];

      coherence

      proof

         [(S `1 ), (S `2 )] is Element of ( QC-Sub-WFF A) by Th10;

        hence thesis by Def16;

      end;

    end

    definition

      let A;

      let S, S9;

      assume

       A1: (S `2 ) = (S9 `2 );

      :: SUBSTUT1:def21

      func Sub_& (S,S9) -> Element of ( QC-Sub-WFF A) equals

      : Def21: [((S `1 ) '&' (S9 `1 )), (S `2 )];

      coherence

      proof

         [(S `1 ), (S `2 )] is Element of ( QC-Sub-WFF A) & [(S9 `1 ), (S9 `2 )] is Element of ( QC-Sub-WFF A) by Th10;

        hence thesis by A1, Def16;

      end;

    end

    reserve B for Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):];

    definition

      let A;

      let B;

      :: original: `1

      redefine

      func B `1 -> Element of ( QC-Sub-WFF A) ;

      coherence by MCART_1: 10;

      :: original: `2

      redefine

      func B `2 -> Element of ( bound_QC-variables A) ;

      coherence by MCART_1: 10;

    end

    definition

      let A;

      let B;

      :: SUBSTUT1:def22

      attr B is quantifiable means ex e st ((B `1 ) `2 ) = (( QSub A) . [( All ((B `2 ),((B `1 ) `1 ))), e]);

    end

    definition

      let A;

      let B;

      assume

       A1: B is quantifiable;

      :: SUBSTUT1:def23

      mode second_Q_comp of B -> Element of ( vSUB A) means

      : Def23: ((B `1 ) `2 ) = (( QSub A) . [( All ((B `2 ),((B `1 ) `1 ))), it ]);

      existence by A1;

    end

    reserve SQ for second_Q_comp of B;

    definition

      let A;

      let B, SQ;

      assume

       A1: B is quantifiable;

      :: SUBSTUT1:def24

      func Sub_All (B,SQ) -> Element of ( QC-Sub-WFF A) equals

      : Def24: [( All ((B `2 ),((B `1 ) `1 ))), SQ];

      coherence

      proof

        ((B `1 ) `2 ) = (( QSub A) . [( All ((B `2 ),((B `1 ) `1 ))), SQ]) by A1, Def23;

        then (B `1 ) = [((B `1 ) `1 ), (( QSub A) . [( All ((B `2 ),((B `1 ) `1 ))), SQ])] by Th10;

        hence thesis by Def16;

      end;

    end

    definition

      let A;

      let S, x;

      :: original: [

      redefine

      func [S,x] -> Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):] ;

      coherence

      proof

         [S, x] in [:( QC-Sub-WFF A), ( bound_QC-variables A):];

        hence thesis;

      end;

    end

    scheme :: SUBSTUT1:sch1

    SubQCInd { Al() -> QC-alphabet , Pro[ Element of ( QC-Sub-WFF Al())] } :

for S be Element of ( QC-Sub-WFF Al()) holds Pro[S]

      provided

       A1: for k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al()) holds Pro[( Sub_P (P,ll,e))]

       and

       A2: for S be Element of ( QC-Sub-WFF Al()) st S is Al() -Sub_VERUM holds Pro[S]

       and

       A3: for S be Element of ( QC-Sub-WFF Al()) st Pro[S] holds Pro[( Sub_not S)]

       and

       A4: for S,S9 be Element of ( QC-Sub-WFF Al()) st (S `2 ) = (S9 `2 ) & Pro[S] & Pro[S9] holds Pro[( Sub_& (S,S9))]

       and

       A5: for x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x] st [S, x] is quantifiable & Pro[S] holds Pro[( Sub_All ( [S, x],SQ))];

      set X = { S where S be Element of ( QC-Sub-WFF Al()) : Pro[S] };

      X is non empty

      proof

        set e = the Element of ( vSUB Al());

        reconsider V = [( VERUM Al()), e] as Element of ( QC-Sub-WFF Al()) by Def16;

        V is Al() -Sub_VERUM;

        then Pro[V] by A2;

        then V in X;

        hence thesis;

      end;

      then

      reconsider X as non empty set;

      for e be Element of ( vSUB Al()) holds [( VERUM Al()), e] in X

      proof

        let e be Element of ( vSUB Al());

        reconsider V = [( VERUM Al()), e] as Element of ( QC-Sub-WFF Al()) by Def16;

        V is Al() -Sub_VERUM;

        then Pro[V] by A2;

        hence thesis;

      end;

      then

       A6: for e be Element of ( vSUB Al()) holds [ <* [ 0 , 0 ]*>, e] in X;

      

       A7: for p be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al()) st [p, e] in X holds [( <* [1, 0 ]*> ^ p), e] in X

      proof

        let p be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al());

        assume [p, e] in X;

        then

        consider S be Element of ( QC-Sub-WFF Al()) such that

         A8: S = [p, e] and

         A9: Pro[S];

        Pro[( Sub_not S)] by A3, A9;

        then ( Sub_not S) in X;

        hence thesis by A8;

      end;

      

       A10: for x be bound_QC-variable of Al(), p be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al()) st [p, (( QSub Al()) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in X holds [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e] in X

      proof

        let x be bound_QC-variable of Al(), p be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al());

        assume [p, (( QSub Al()) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] in X;

        then

        consider S be Element of ( QC-Sub-WFF Al()) such that

         A11: S = [p, (( QSub Al()) . [(( <* [3, 0 ]*> ^ <*x*>) ^ p), e])] and

         A12: Pro[S];

        consider B be set such that

         A13: B = [S, x];

        reconsider B as Element of [:( QC-Sub-WFF Al()), ( bound_QC-variables Al()):] by A13;

        

         A14: (B `1 ) = S & (B `2 ) = x by A13;

        

         A15: (S `2 ) = (( QSub Al()) . [( All (x,(S `1 ))), e]) by A11;

        then

         A16: B is quantifiable by A14;

        then

        reconsider e as second_Q_comp of B by A15, A14, Def23;

        Pro[( Sub_All (B,e))] by A5, A12, A13, A16;

        then ( Sub_All (B,e)) in X;

        then [( All ((B `2 ),((B `1 ) `1 ))), e] in X by A16, Def24;

        hence thesis by A11, A14;

      end;

      let F be Element of ( QC-Sub-WFF Al());

      

       A17: X c= [:( [: NAT , ( QC-symbols Al()):] * ), ( vSUB Al()):]

      proof

        let x be object;

        assume x in X;

        then ex S be Element of ( QC-Sub-WFF Al()) st x = S & Pro[S];

        then

        consider p be Element of ( QC-WFF Al()), e be Element of ( vSUB Al()) such that

         A18: x = [p, e] by Th8;

        p = ( @ p);

        then p in ( [: NAT , ( QC-symbols Al()):] * ) by FINSEQ_1:def 11;

        hence thesis by A18, ZFMISC_1:def 2;

      end;

      

       A19: for p,q be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al()) st [p, e] in X & [q, e] in X holds [(( <* [2, 0 ]*> ^ p) ^ q), e] in X

      proof

        let p,q be FinSequence of [: NAT , ( QC-symbols Al()):], e be Element of ( vSUB Al());

        assume [p, e] in X;

        then

        consider S1 be Element of ( QC-Sub-WFF Al()) such that

         A20: S1 = [p, e] and

         A21: Pro[S1];

        assume [q, e] in X;

        then

        consider S2 be Element of ( QC-Sub-WFF Al()) such that

         A22: S2 = [q, e] and

         A23: Pro[S2];

        consider p9 be Element of ( QC-WFF Al()), e1 be Element of ( vSUB Al()) such that

         A24: [p, e] = [p9, e1] by A20, Th8;

        

         A25: e = e1 by A24, XTUPLE_0: 1;

        then

         A26: (S1 `2 ) = e1 by A20;

        then

         A27: (S1 `2 ) = (S2 `2 ) by A22, A25;

        then Pro[( Sub_& (S1,S2))] by A4, A21, A23;

        then ( Sub_& (S1,S2)) in X;

        then

         A28: [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] in X by A27, Def21;

        

         A29: p = p9 by A24, XTUPLE_0: 1;

        then (S1 `1 ) = p9 by A20;

        hence thesis by A22, A29, A25, A26, A28;

      end;

      for k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al()) holds [( <*P*> ^ ll), e] in X

      proof

        let k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al());

        Pro[( Sub_P (P,ll,e))] & [(P ! ll), e] = ( Sub_P (P,ll,e)) by A1, Th9;

        then [(P ! ll), e] in X;

        hence thesis by QC_LANG1: 8;

      end;

      then X is Al() -Sub-closed by A17, A6, A7, A19, A10;

      then ( QC-Sub-WFF Al()) c= X by Def17;

      then F in X;

      then ex S be Element of ( QC-Sub-WFF Al()) st S = F & Pro[S];

      hence thesis;

    end;

    definition

      let A;

      let S;

      :: SUBSTUT1:def25

      attr S is Sub_atomic means ex k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) st S = ( Sub_P (P,ll,e));

    end

    theorem :: SUBSTUT1:11

    

     Th11: S is Sub_atomic implies (S `1 ) is atomic

    proof

      assume S is Sub_atomic;

      then

      consider k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) such that

       A1: S = ( Sub_P (P,ll,e));

      S = [(P ! ll), e] by A1, Th9;

      then (S `1 ) = (P ! ll);

      hence thesis;

    end;

    registration

      let A;

      let k be Nat;

      let P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A;

      let e be Element of ( vSUB A);

      cluster ( Sub_P (P,ll,e)) -> Sub_atomic;

      coherence ;

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def26

      attr S is Sub_negative means

      : Def26: ex S9 st S = ( Sub_not S9);

      :: SUBSTUT1:def27

      attr S is Sub_conjunctive means

      : Def27: ex S1, S2 st S = ( Sub_& (S1,S2)) & (S1 `2 ) = (S2 `2 );

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def28

      attr S is Sub_universal means

      : Def28: ex B, SQ st S = ( Sub_All (B,SQ)) & B is quantifiable;

    end

    theorem :: SUBSTUT1:12

    

     Th12: for S holds S is A -Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal

    proof

      defpred P[ Element of ( QC-Sub-WFF A)] means $1 is A -Sub_VERUM or $1 is Sub_atomic or $1 is Sub_negative or $1 is Sub_conjunctive or $1 is Sub_universal;

      

       A1: for k be Nat, p be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) holds P[( Sub_P (p,ll,e))];

      

       A2: for S be Element of ( QC-Sub-WFF A) st S is A -Sub_VERUM holds P[S];

      

       A3: for x be bound_QC-variable of A, S be Element of ( QC-Sub-WFF A), SQ be second_Q_comp of [S, x] st [S, x] is quantifiable & P[S] holds P[( Sub_All ( [S, x],SQ))] by Def28;

      

       A4: for S1,S2 be Element of ( QC-Sub-WFF A) st (S1 `2 ) = (S2 `2 ) & P[S1] & P[S2] holds P[( Sub_& (S1,S2))] by Def27;

      

       A5: for S be Element of ( QC-Sub-WFF A) st P[S] holds P[( Sub_not S)] by Def26;

      thus for S be Element of ( QC-Sub-WFF A) holds P[S] from SubQCInd( A1, A2, A5, A4, A3);

    end;

    definition

      let A;

      let S;

      :: SUBSTUT1:def29

      func Sub_the_arguments_of S -> FinSequence of ( QC-variables A) means

      : Def29: ex k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) st it = ll & S = ( Sub_P (P,ll,e));

      existence by A1;

      uniqueness

      proof

        let ll1,ll2 be FinSequence of ( QC-variables A);

        given k1 be Nat, P1 be QC-pred_symbol of k1, A, ll19 be QC-variable_list of k1, A, e1 be Element of ( vSUB A) such that

         A2: ll1 = ll19 and

         A3: S = ( Sub_P (P1,ll19,e1));

        

         A4: S = [(P1 ! ll19), e1] by A3, Th9;

        given k2 be Nat, P2 be QC-pred_symbol of k2, A, ll29 be QC-variable_list of k2, A, e2 be Element of ( vSUB A) such that

         A5: ll2 = ll29 and

         A6: S = ( Sub_P (P2,ll29,e2));

        

         A7: ( <*P2*> ^ ll29) = (P2 ! ll29) & (S `1 ) = ( <*P1*> ^ ll19) by A4, QC_LANG1: 8;

        

         A8: (S `1 ) is atomic by A1, Th11;

        

         A9: S = [(P2 ! ll29), e2] by A6, Th9;

        then

         A10: (S `1 ) = (P2 ! ll29);

        (S `1 ) = (P1 ! ll19) by A4;

        

        then P1 = ( the_pred_symbol_of (S `1 )) by A8, QC_LANG1:def 22

        .= P2 by A10, A8, QC_LANG1:def 22;

        hence ll1 = ll2 by A2, A5, A9, A7, FINSEQ_1: 33;

      end;

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def30

      func Sub_the_argument_of S -> Element of ( QC-Sub-WFF A) means

      : Def30: S = ( Sub_not it );

      existence by A1;

      uniqueness

      proof

        let S1, S2;

        

         A2: S1 = [(S1 `1 ), (S1 `2 )] & S2 = [(S2 `1 ), (S2 `2 )] by Th10;

        assume

         A3: S = ( Sub_not S1) & S = ( Sub_not S2);

        then ( 'not' (S1 `1 )) = ( 'not' (S2 `1 )) by XTUPLE_0: 1;

        then (S1 `1 ) = (S2 `1 ) by FINSEQ_1: 33;

        hence thesis by A3, A2, XTUPLE_0: 1;

      end;

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def31

      func Sub_the_left_argument_of S -> Element of ( QC-Sub-WFF A) means

      : Def31: ex S9 st S = ( Sub_& (it ,S9)) & (it `2 ) = (S9 `2 );

      existence by A1;

      uniqueness

      proof

        let S1, S2;

        given T1 be Element of ( QC-Sub-WFF A) such that

         A2: S = ( Sub_& (S1,T1)) & (S1 `2 ) = (T1 `2 );

        given T2 be Element of ( QC-Sub-WFF A) such that

         A3: S = ( Sub_& (S2,T2)) & (S2 `2 ) = (T2 `2 );

        

         A4: ( len ( @ (S1 `1 ))) <= ( len ( @ (S2 `1 ))) or ( len ( @ (S2 `1 ))) <= ( len ( @ (S1 `1 )));

        

         A5: S = [((S2 `1 ) '&' (T2 `1 )), (S2 `2 )] by A3, Def21;

        

         A6: S = [((S1 `1 ) '&' (T1 `1 )), (S1 `2 )] by A2, Def21;

        then ((S1 `1 ) '&' (T1 `1 )) = ((S2 `1 ) '&' (T2 `1 )) by A5, XTUPLE_0: 1;

        

        then ( <* [2, 0 ]*> ^ (( @ (S1 `1 )) ^ ( @ (T1 `1 )))) = ((S2 `1 ) '&' (T2 `1 )) by FINSEQ_1: 32

        .= ( <* [2, 0 ]*> ^ (( @ (S2 `1 )) ^ ( @ (T2 `1 )))) by FINSEQ_1: 32;

        then (( @ (S1 `1 )) ^ ( @ (T1 `1 ))) = (( @ (S2 `1 )) ^ ( @ (T2 `1 ))) by FINSEQ_1: 33;

        then

        consider a,b,c,d be FinSequence such that

         A7: a = ( @ (S1 `1 )) & b = ( @ (S2 `1 )) or a = ( @ (S2 `1 )) & b = ( @ (S1 `1 )) and

         A8: ( len a) <= ( len b) & (a ^ c) = (b ^ d) by A4;

        

         A9: S1 = [(S1 `1 ), (S1 `2 )] & S2 = [(S2 `1 ), (S2 `2 )] by Th10;

        ex t be FinSequence st (a ^ t) = b by A8, FINSEQ_1: 47;

        then (S1 `1 ) = (S2 `1 ) by A7, QC_LANG1: 13;

        hence thesis by A6, A5, A9, XTUPLE_0: 1;

      end;

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def32

      func Sub_the_right_argument_of S -> Element of ( QC-Sub-WFF A) means

      : Def32: ex S9 st S = ( Sub_& (S9,it )) & (S9 `2 ) = (it `2 );

      existence by A1;

      uniqueness

      proof

        let T1, T2;

        given S1 be Element of ( QC-Sub-WFF A) such that

         A2: S = ( Sub_& (S1,T1)) & (S1 `2 ) = (T1 `2 );

        

         A3: T1 = [(T1 `1 ), (T1 `2 )] & T2 = [(T2 `1 ), (T2 `2 )] by Th10;

        given S2 be Element of ( QC-Sub-WFF A) such that

         A4: S = ( Sub_& (S2,T2)) & (S2 `2 ) = (T2 `2 );

        

         A5: S = [((S1 `1 ) '&' (T1 `1 )), (T1 `2 )] by A2, Def21;

        

         A6: S = [((S2 `1 ) '&' (T2 `1 )), (T2 `2 )] by A4, Def21;

        then ((S1 `1 ) '&' (T1 `1 )) = ((S2 `1 ) '&' (T2 `1 )) by A5, XTUPLE_0: 1;

        

        then ( <* [2, 0 ]*> ^ (( @ (S1 `1 )) ^ ( @ (T1 `1 )))) = ((S2 `1 ) '&' (T2 `1 )) by FINSEQ_1: 32

        .= ( <* [2, 0 ]*> ^ (( @ (S2 `1 )) ^ ( @ (T2 `1 )))) by FINSEQ_1: 32;

        then

         A7: (( @ (S1 `1 )) ^ ( @ (T1 `1 ))) = (( @ (S2 `1 )) ^ ( @ (T2 `1 ))) by FINSEQ_1: 33;

        S1 = ( Sub_the_left_argument_of S) by A1, A2, Def31

        .= S2 by A1, A4, Def31;

        then ( @ (T1 `1 )) = ( @ (T2 `1 )) by A7, FINSEQ_1: 33;

        hence thesis by A5, A6, A3, XTUPLE_0: 1;

      end;

    end

    definition

      let A;

      let S;

      :: SUBSTUT1:def33

      func Sub_the_bound_of S -> bound_QC-variable of A means ex B, SQ st S = ( Sub_All (B,SQ)) & (B `2 ) = it & B is quantifiable;

      existence

      proof

        consider B, SQ such that

         A2: S = ( Sub_All (B,SQ)) & B is quantifiable by A1;

        take (B `2 );

        thus thesis by A2;

      end;

      uniqueness

      proof

        let x1, x2;

        assume that

         A3: ex B, SQ st S = ( Sub_All (B,SQ)) & (B `2 ) = x1 & B is quantifiable and

         A4: ex B, SQ st S = ( Sub_All (B,SQ)) & (B `2 ) = x2 & B is quantifiable;

        consider B1 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ1 be second_Q_comp of B1 such that

         A5: S = ( Sub_All (B1,SQ1)) and

         A6: (B1 `2 ) = x1 and

         A7: B1 is quantifiable by A3;

        consider B2 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ2 be second_Q_comp of B2 such that

         A8: S = ( Sub_All (B2,SQ2)) and

         A9: (B2 `2 ) = x2 and

         A10: B2 is quantifiable by A4;

        

         A11: [( All ((B2 `2 ),((B2 `1 ) `1 ))), SQ2] = S by A8, A10, Def24;

         [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1] = S by A5, A7, Def24;

        then ( All ((B1 `2 ),((B1 `1 ) `1 ))) = ( All ((B2 `2 ),((B2 `1 ) `1 ))) by A11, XTUPLE_0: 1;

        hence thesis by A6, A9, QC_LANG2: 5;

      end;

    end

    definition

      let A;

      let A2 be Element of ( QC-Sub-WFF A);

      :: SUBSTUT1:def34

      func Sub_the_scope_of A2 -> Element of ( QC-Sub-WFF A) means

      : Def34: ex B, SQ st A2 = ( Sub_All (B,SQ)) & (B `1 ) = it & B is quantifiable;

      existence

      proof

        consider B, SQ such that

         A2: A2 = ( Sub_All (B,SQ)) & B is quantifiable by A1;

        take (B `1 );

        thus thesis by A2;

      end;

      uniqueness

      proof

        let S1, S2;

        given B1 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ1 be second_Q_comp of B1 such that

         A3: A2 = ( Sub_All (B1,SQ1)) and

         A4: (B1 `1 ) = S1 and

         A5: B1 is quantifiable;

        

         A6: A2 = [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1] by A3, A5, Def24;

        

         A7: ((B1 `1 ) `2 ) = (( QSub A) . [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1]) by A5, Def23;

        given B2 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ2 be second_Q_comp of B2 such that

         A8: A2 = ( Sub_All (B2,SQ2)) and

         A9: (B2 `1 ) = S2 and

         A10: B2 is quantifiable;

        

         A11: (B1 `1 ) = [((B1 `1 ) `1 ), ((B1 `1 ) `2 )] & (B2 `1 ) = [((B2 `1 ) `1 ), ((B2 `1 ) `2 )] by Th10;

        

         A12: A2 = [( All ((B2 `2 ),((B2 `1 ) `1 ))), SQ2] by A8, A10, Def24;

        then ( All ((B1 `2 ),((B1 `1 ) `1 ))) = ( All ((B2 `2 ),((B2 `1 ) `1 ))) by A6, XTUPLE_0: 1;

        then ((B1 `1 ) `1 ) = ((B2 `1 ) `1 ) by QC_LANG2: 5;

        hence thesis by A4, A9, A10, A6, A12, A7, A11, Def23;

      end;

    end

    registration

      let A;

      let S;

      cluster ( Sub_not S) -> Sub_negative;

      coherence ;

    end

    theorem :: SUBSTUT1:13

    

     Th13: (S1 `2 ) = (S2 `2 ) implies ( Sub_& (S1,S2)) is Sub_conjunctive;

    theorem :: SUBSTUT1:14

    

     Th14: B is quantifiable implies ( Sub_All (B,SQ)) is Sub_universal;

    theorem :: SUBSTUT1:15

    ( Sub_not S) = ( Sub_not S9) implies S = S9

    proof

      assume ( Sub_not S) = ( Sub_not S9);

      then

       A1: ( 'not' (S `1 )) = ( 'not' (S9 `1 )) & (S `2 ) = (S9 `2 ) by XTUPLE_0: 1;

      S = [(S `1 ), (S `2 )] & S9 = [(S9 `1 ), (S9 `2 )] by Th10;

      hence thesis by A1, FINSEQ_1: 33;

    end;

    theorem :: SUBSTUT1:16

    ( Sub_the_argument_of ( Sub_not S)) = S by Def30;

    theorem :: SUBSTUT1:17

    (S1 `2 ) = (S2 `2 ) & (S19 `2 ) = (S29 `2 ) & ( Sub_& (S1,S2)) = ( Sub_& (S19,S29)) implies S1 = S19 & S2 = S29

    proof

      assume that

       A1: (S1 `2 ) = (S2 `2 ) and

       A2: (S19 `2 ) = (S29 `2 ) and

       A3: ( Sub_& (S1,S2)) = ( Sub_& (S19,S29));

      ( Sub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A1, Def21;

      then [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] = [((S19 `1 ) '&' (S29 `1 )), (S19 `2 )] by A2, A3, Def21;

      then

       A4: ((S1 `1 ) '&' (S2 `1 )) = ((S19 `1 ) '&' (S29 `1 )) & (S1 `2 ) = (S19 `2 ) by XTUPLE_0: 1;

      

       A5: S2 = [(S2 `1 ), (S2 `2 )] & S29 = [(S29 `1 ), (S29 `2 )] by Th10;

      S1 = [(S1 `1 ), (S1 `2 )] & S19 = [(S19 `1 ), (S19 `2 )] by Th10;

      hence thesis by A1, A2, A4, A5, QC_LANG2: 2;

    end;

    theorem :: SUBSTUT1:18

    

     Th18: (S1 `2 ) = (S2 `2 ) implies ( Sub_the_left_argument_of ( Sub_& (S1,S2))) = S1

    proof

      assume

       A1: (S1 `2 ) = (S2 `2 );

      then ( Sub_& (S1,S2)) is Sub_conjunctive;

      hence thesis by A1, Def31;

    end;

    theorem :: SUBSTUT1:19

    

     Th19: (S1 `2 ) = (S2 `2 ) implies ( Sub_the_right_argument_of ( Sub_& (S1,S2))) = S2

    proof

      assume

       A1: (S1 `2 ) = (S2 `2 );

      then ( Sub_& (S1,S2)) is Sub_conjunctive;

      hence thesis by A1, Def32;

    end;

    theorem :: SUBSTUT1:20

    for B1,B2 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ1 be second_Q_comp of B1, SQ2 be second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & ( Sub_All (B1,SQ1)) = ( Sub_All (B2,SQ2)) holds B1 = B2

    proof

      let B1,B2 be Element of [:( QC-Sub-WFF A), ( bound_QC-variables A):], SQ1 be second_Q_comp of B1, SQ2 be second_Q_comp of B2 such that

       A1: B1 is quantifiable and

       A2: B2 is quantifiable and

       A3: ( Sub_All (B1,SQ1)) = ( Sub_All (B2,SQ2));

      

       A4: ( Sub_All (B1,SQ1)) = [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1] & ( Sub_All (B2,SQ2)) = [( All ((B2 `2 ),((B2 `1 ) `1 ))), SQ2] by A1, A2, Def24;

      then ( All ((B1 `2 ),((B1 `1 ) `1 ))) = ( All ((B2 `2 ),((B2 `1 ) `1 ))) by A3, XTUPLE_0: 1;

      then

       A5: (B1 `2 ) = (B2 `2 ) & ((B1 `1 ) `1 ) = ((B2 `1 ) `1 ) by QC_LANG2: 5;

      ex a,b be object st a in ( QC-Sub-WFF A) & b in ( bound_QC-variables A) & B2 = [a, b] by ZFMISC_1:def 2;

      then

       A6: B2 = [(B2 `1 ), (B2 `2 )];

      ex a,b be object st a in ( QC-Sub-WFF A) & b in ( bound_QC-variables A) & B1 = [a, b] by ZFMISC_1:def 2;

      then

       A7: B1 = [(B1 `1 ), (B1 `2 )];

      

       A8: (B1 `1 ) = [((B1 `1 ) `1 ), ((B1 `1 ) `2 )] & (B2 `1 ) = [((B2 `1 ) `1 ), ((B2 `1 ) `2 )] by Th10;

      ((B1 `1 ) `2 ) = (( QSub A) . [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1]) by A1, Def23;

      hence thesis by A2, A3, A4, A5, A8, A7, A6, Def23;

    end;

    theorem :: SUBSTUT1:21

    

     Th21: B is quantifiable implies ( Sub_the_scope_of ( Sub_All (B,SQ))) = (B `1 )

    proof

      assume

       A1: B is quantifiable;

      then ( Sub_All (B,SQ)) is Sub_universal;

      hence thesis by A1, Def34;

    end;

    scheme :: SUBSTUT1:sch2

    SubQCInd2 { Al() -> QC-alphabet , Pro[ Element of ( QC-Sub-WFF Al())] } :

for S be Element of ( QC-Sub-WFF Al()) holds Pro[S]

      provided

       A1: for S be Element of ( QC-Sub-WFF Al()) holds (S is Sub_atomic implies Pro[S]) & (S is Al() -Sub_VERUM implies Pro[S]) & (S is Sub_negative & Pro[( Sub_the_argument_of S)] implies Pro[S]) & (S is Sub_conjunctive & Pro[( Sub_the_left_argument_of S)] & Pro[( Sub_the_right_argument_of S)] implies Pro[S]) & (S is Sub_universal & Pro[( Sub_the_scope_of S)] implies Pro[S]);

       A2:

      now

        let x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x] such that

         A3: [S, x] is quantifiable and

         A4: Pro[S];

        ( [S, x] `1 ) = ( Sub_the_scope_of ( Sub_All ( [S, x],SQ))) by A3, Th21;

        then

         A5: S = ( Sub_the_scope_of ( Sub_All ( [S, x],SQ)));

        ( Sub_All ( [S, x],SQ)) is Sub_universal by A3;

        hence Pro[( Sub_All ( [S, x],SQ))] by A1, A4, A5;

      end;

       A6:

      now

        let S1,S2 be Element of ( QC-Sub-WFF Al()) such that

         A7: (S1 `2 ) = (S2 `2 ) and

         A8: Pro[S1] & Pro[S2];

        

         A9: S2 = ( Sub_the_right_argument_of ( Sub_& (S1,S2))) by A7, Th19;

        ( Sub_& (S1,S2)) is Sub_conjunctive & S1 = ( Sub_the_left_argument_of ( Sub_& (S1,S2))) by A7, Th18;

        hence Pro[( Sub_& (S1,S2))] by A1, A8, A9;

      end;

       A10:

      now

        let S be Element of ( QC-Sub-WFF Al()) such that

         A11: Pro[S];

        S = ( Sub_the_argument_of ( Sub_not S)) by Def30;

        hence Pro[( Sub_not S)] by A1, A11;

      end;

      

       A12: for S be Element of ( QC-Sub-WFF Al()) st S is Al() -Sub_VERUM holds Pro[S] by A1;

      

       A13: for k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al()) holds Pro[( Sub_P (P,ll,e))] by A1;

      thus thesis from SubQCInd( A13, A12, A10, A6, A2);

    end;

    theorem :: SUBSTUT1:22

    

     Th22: S is Sub_negative implies ( len ( @ (( Sub_the_argument_of S) `1 ))) < ( len ( @ (S `1 )))

    proof

      assume S is Sub_negative;

      then

      consider S9 such that

       A1: S = ( Sub_not S9);

      

       A2: ( 'not' (S9 `1 )) is negative;

      (S `1 ) = ( 'not' (S9 `1 )) by A1;

      then

       A3: ( len ( @ ( the_argument_of ( 'not' (S9 `1 ))))) < ( len ( @ (S `1 ))) by A2, QC_LANG1: 14;

      (( Sub_the_argument_of S) `1 ) = (S9 `1 ) by A1, Def30;

      hence thesis by A3, QC_LANG2: 1;

    end;

    theorem :: SUBSTUT1:23

    

     Th23: S is Sub_conjunctive implies ( len ( @ (( Sub_the_left_argument_of S) `1 ))) < ( len ( @ (S `1 ))) & ( len ( @ (( Sub_the_right_argument_of S) `1 ))) < ( len ( @ (S `1 )))

    proof

      assume S is Sub_conjunctive;

      then

      consider S1, S2 such that

       A1: S = ( Sub_& (S1,S2)) & (S1 `2 ) = (S2 `2 );

      S = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A1, Def21;

      then

       A2: (S `1 ) = ((S1 `1 ) '&' (S2 `1 ));

      ((S1 `1 ) '&' (S2 `1 )) is conjunctive;

      then

       A3: ( len ( @ ( the_left_argument_of ((S1 `1 ) '&' (S2 `1 ))))) < ( len ( @ (S `1 ))) & ( len ( @ ( the_right_argument_of ((S1 `1 ) '&' (S2 `1 ))))) < ( len ( @ (S `1 ))) by A2, QC_LANG1: 15;

      (( Sub_the_right_argument_of S) `1 ) = (S2 `1 ) & (( Sub_the_left_argument_of S) `1 ) = (S1 `1 ) by A1, Th18, Th19;

      hence thesis by A3, QC_LANG2: 4;

    end;

    theorem :: SUBSTUT1:24

    

     Th24: S is Sub_universal implies ( len ( @ (( Sub_the_scope_of S) `1 ))) < ( len ( @ (S `1 )))

    proof

      assume S is Sub_universal;

      then

      consider B, SQ such that

       A1: S = ( Sub_All (B,SQ)) & B is quantifiable;

      S = [( All ((B `2 ),((B `1 ) `1 ))), SQ] by A1, Def24;

      then

       A2: (S `1 ) = ( All ((B `2 ),((B `1 ) `1 )));

      ( All ((B `2 ),((B `1 ) `1 ))) is universal;

      then

       A3: ( len ( @ ( the_scope_of ( All ((B `2 ),((B `1 ) `1 )))))) < ( len ( @ (S `1 ))) by A2, QC_LANG1: 16;

      (( Sub_the_scope_of S) `1 ) = ((B `1 ) `1 ) by A1, Th21;

      hence thesis by A3, QC_LANG2: 7;

    end;

    theorem :: SUBSTUT1:25

    

     Th25: (S is A -Sub_VERUM implies ((( @ (S `1 )) . 1) `1 ) = 0 ) & (S is Sub_atomic implies ex k be Nat st (( @ (S `1 )) . 1) is QC-pred_symbol of k, A) & (S is Sub_negative implies ((( @ (S `1 )) . 1) `1 ) = 1) & (S is Sub_conjunctive implies ((( @ (S `1 )) . 1) `1 ) = 2) & (S is Sub_universal implies ((( @ (S `1 )) . 1) `1 ) = 3)

    proof

      thus S is A -Sub_VERUM implies ((( @ (S `1 )) . 1) `1 ) = 0

      proof

        assume S is A -Sub_VERUM;

        then ex e st S = [( VERUM A), e];

        then (S `1 ) = ( VERUM A);

        

        hence ((( @ (S `1 )) . 1) `1 ) = ( [ 0 , 0 ] `1 ) by FINSEQ_1:def 8

        .= 0 ;

      end;

      thus S is Sub_atomic implies ex k be Nat st (( @ (S `1 )) . 1) is QC-pred_symbol of k, A

      proof

        assume S is Sub_atomic;

        then

        consider k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A, e be Element of ( vSUB A) such that

         A1: S = ( Sub_P (P,ll,e));

        S = [(P ! ll), e] by A1, Th9;

        then (S `1 ) = (P ! ll);

        then ( @ (S `1 )) = ( <*P*> ^ ll) by QC_LANG1: 8;

        then (( @ (S `1 )) . 1) = P by FINSEQ_1: 41;

        hence thesis;

      end;

      thus S is Sub_negative implies ((( @ (S `1 )) . 1) `1 ) = 1

      proof

        assume S is Sub_negative;

        then

        consider S9 such that

         A2: S = ( Sub_not S9);

        (S `1 ) = ( 'not' (S9 `1 )) by A2;

        then (( @ (S `1 )) . 1) = [1, 0 ] by FINSEQ_1: 41;

        hence thesis;

      end;

      thus S is Sub_conjunctive implies ((( @ (S `1 )) . 1) `1 ) = 2

      proof

        assume S is Sub_conjunctive;

        then

        consider S1, S2 such that

         A3: S = ( Sub_& (S1,S2)) & (S1 `2 ) = (S2 `2 );

        S = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A3, Def21;

        then (S `1 ) = ((S1 `1 ) '&' (S2 `1 ));

        then ( @ (S `1 )) = ( <* [2, 0 ]*> ^ (( @ (S1 `1 )) ^ ( @ (S2 `1 )))) by FINSEQ_1: 32;

        then (( @ (S `1 )) . 1) = [2, 0 ] by FINSEQ_1: 41;

        hence thesis;

      end;

      thus S is Sub_universal implies ((( @ (S `1 )) . 1) `1 ) = 3

      proof

        assume S is Sub_universal;

        then

        consider B, SQ such that

         A4: S = ( Sub_All (B,SQ)) & B is quantifiable;

        S = [( All ((B `2 ),((B `1 ) `1 ))), SQ] by A4, Def24;

        then (S `1 ) = ( All ((B `2 ),((B `1 ) `1 )));

        then ( @ (S `1 )) = ( <* [3, 0 ]*> ^ ( <*(B `2 )*> ^ ( @ ((B `1 ) `1 )))) by FINSEQ_1: 32;

        then (( @ (S `1 )) . 1) = [3, 0 ] by FINSEQ_1: 41;

        hence thesis;

      end;

    end;

    theorem :: SUBSTUT1:26

    

     Th26: S is Sub_atomic implies ((( @ (S `1 )) . 1) `1 ) <> 0 & ((( @ (S `1 )) . 1) `1 ) <> 1 & ((( @ (S `1 )) . 1) `1 ) <> 2 & ((( @ (S `1 )) . 1) `1 ) <> 3

    proof

      assume S is Sub_atomic;

      then ex k be Nat st (( @ (S `1 )) . 1) is QC-pred_symbol of k, A by Th25;

      hence thesis by QC_LANG1: 17;

    end;

    theorem :: SUBSTUT1:27

    

     Th27: not (ex S st S is Sub_atomic Sub_negative or S is Sub_atomic Sub_conjunctive or S is Sub_atomic Sub_universal or S is Sub_negative Sub_conjunctive or S is Sub_negative Sub_universal or S is Sub_conjunctive Sub_universal or S is A -Sub_VERUM Sub_atomic or S is A -Sub_VERUM Sub_negative or S is A -Sub_VERUM Sub_conjunctive or S is A -Sub_VERUM Sub_universal)

    proof

      let S;

      

       A1: S is Sub_negative implies ((( @ (S `1 )) . 1) `1 ) = 1 by Th25;

      

       A2: S is Sub_conjunctive implies ((( @ (S `1 )) . 1) `1 ) = 2 by Th25;

      

       A3: S is Sub_universal implies ((( @ (S `1 )) . 1) `1 ) = 3 by Th25;

      S is A -Sub_VERUM implies ((( @ (S `1 )) . 1) `1 ) = 0 by Th25;

      hence thesis by A1, A2, A3, Th26;

    end;

    scheme :: SUBSTUT1:sch3

    SubFuncEx { Al() -> QC-alphabet , D() -> non empty set , V() -> Element of D() , A( Element of ( QC-Sub-WFF Al())) -> Element of D() , N( Element of D()) -> Element of D() , C( Element of D(), Element of D()) -> Element of D() , R( set, Element of ( QC-Sub-WFF Al()), Element of D()) -> Element of D() } :

ex F be Function of ( QC-Sub-WFF Al()), D() st for S be Element of ( QC-Sub-WFF Al()) holds for d1,d2 be Element of D() holds (S is Al() -Sub_VERUM implies (F . S) = V()) & (S is Sub_atomic implies (F . S) = A(S)) & (S is Sub_negative & d1 = (F . ( Sub_the_argument_of S)) implies (F . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F . ( Sub_the_left_argument_of S)) & d2 = (F . ( Sub_the_right_argument_of S)) implies (F . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F . ( Sub_the_scope_of S)) implies (F . S) = R(Al,S,d1));

      defpred Pfn[ Function of ( QC-Sub-WFF Al()), D(), Nat] means for S be Element of ( QC-Sub-WFF Al()) st ( len ( @ (S `1 ))) <= $2 holds (S is Al() -Sub_VERUM implies ($1 . S) = V()) & (S is Sub_atomic implies ($1 . S) = A(S)) & (S is Sub_negative implies ($1 . S) = N(.)) & (S is Sub_conjunctive implies ($1 . S) = C(.,.)) & (S is Sub_universal implies ($1 . S) = R(Al,S,.));

      defpred Pfgp[ Element of D(), Function of ( QC-Sub-WFF Al()), D(), Element of ( QC-Sub-WFF Al())] means ($3 is Al() -Sub_VERUM implies $1 = V()) & ($3 is Sub_atomic implies $1 = A($3)) & ($3 is Sub_negative implies $1 = N(.)) & ($3 is Sub_conjunctive implies $1 = C(.,.)) & ($3 is Sub_universal implies $1 = R(Al,$3,.));

      defpred S[ Nat] means ex F be Function of ( QC-Sub-WFF Al()), D() st Pfn[F, $1];

      defpred Qfn[ object, object] means ex S be Element of ( QC-Sub-WFF Al()) st S = $1 & for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S `1 ))) qua Nat] holds $2 = (g . S);

      

       A1: for n be Nat st S[n] holds S[(n + 1)]

      proof

        let n be Nat;

        given F be Function of ( QC-Sub-WFF Al()), D() such that

         A2: Pfn[F, n];

        defpred R[ Element of ( QC-Sub-WFF Al()), Element of D()] means (( len ( @ ($1 `1 ))) <> (n + 1) implies $2 = (F . $1)) & (( len ( @ ($1 `1 ))) = (n + 1) implies Pfgp[$2, F, $1]);

        

         A3: for S be Element of ( QC-Sub-WFF Al()) holds ex y be Element of D() st R[S, y]

        proof

          let S be Element of ( QC-Sub-WFF Al());

          now

            per cases by Th12;

              case ( len ( @ (S `1 ))) <> (n + 1);

              take y = (F . S);

              thus y = (F . S);

            end;

              case

               A4: ( len ( @ (S `1 ))) = (n + 1) & S is Al() -Sub_VERUM;

              take y = V();

              thus Pfgp[y, F, S] by A4, Th27;

            end;

              case

               A5: ( len ( @ (S `1 ))) = (n + 1) & S is Sub_atomic;

              take y = A(S);

              thus Pfgp[y, F, S] by A5, Th27;

            end;

              case

               A6: ( len ( @ (S `1 ))) = (n + 1) & S is Sub_negative;

              take y = N(.);

              thus Pfgp[y, F, S] by A6, Th27;

            end;

              case

               A7: ( len ( @ (S `1 ))) = (n + 1) & S is Sub_conjunctive;

              take y = C(.,.);

              thus Pfgp[y, F, S] by A7, Th27;

            end;

              case

               A8: ( len ( @ (S `1 ))) = (n + 1) & S is Sub_universal;

              take y = R(Al,S,.);

              thus Pfgp[y, F, S] by A8, Th27;

            end;

          end;

          hence thesis;

        end;

        consider G be Function of ( QC-Sub-WFF Al()), D() such that

         A9: for S be Element of ( QC-Sub-WFF Al()) holds R[S, (G . S)] from FUNCT_2:sch 3( A3);

        take H = G;

        thus Pfn[H, (n + 1)]

        proof

          let S be Element of ( QC-Sub-WFF Al()) such that

           A10: ( len ( @ (S `1 ))) <= (n + 1);

          thus S is Al() -Sub_VERUM implies (H . S) = V()

          proof

            now

              per cases ;

                suppose ( len ( @ (S `1 ))) <> (n + 1);

                then ( len ( @ (S `1 ))) <= n & (H . S) = (F . S) by A9, A10, NAT_1: 8;

                hence thesis by A2;

              end;

                suppose ( len ( @ (S `1 ))) = (n + 1);

                hence thesis by A9;

              end;

            end;

            hence thesis;

          end;

          thus S is Sub_atomic implies (H . S) = A(S)

          proof

            now

              per cases ;

                suppose ( len ( @ (S `1 ))) <> (n + 1);

                then ( len ( @ (S `1 ))) <= n & (H . S) = (F . S) by A9, A10, NAT_1: 8;

                hence thesis by A2;

              end;

                suppose ( len ( @ (S `1 ))) = (n + 1);

                hence thesis by A9;

              end;

            end;

            hence thesis;

          end;

          thus S is Sub_negative implies (H . S) = N(.)

          proof

            assume

             A11: S is Sub_negative;

            then ( len ( @ (( Sub_the_argument_of S) `1 ))) <> (n + 1) by A10, Th22;

            then

             A12: (H . ( Sub_the_argument_of S)) = (F . ( Sub_the_argument_of S)) by A9;

            now

              per cases ;

                suppose ( len ( @ (S `1 ))) <> (n + 1);

                then ( len ( @ (S `1 ))) <= n & (H . S) = (F . S) by A9, A10, NAT_1: 8;

                hence thesis by A2, A11, A12;

              end;

                suppose ( len ( @ (S `1 ))) = (n + 1);

                hence thesis by A9, A11, A12;

              end;

            end;

            hence thesis;

          end;

          thus S is Sub_conjunctive implies (H . S) = C(.,.)

          proof

            assume

             A13: S is Sub_conjunctive;

            then ( len ( @ (( Sub_the_right_argument_of S) `1 ))) <> (n + 1) by A10, Th23;

            then

             A14: (H . ( Sub_the_right_argument_of S)) = (F . ( Sub_the_right_argument_of S)) by A9;

            ( len ( @ (( Sub_the_left_argument_of S) `1 ))) <> (n + 1) by A10, A13, Th23;

            then

             A15: (H . ( Sub_the_left_argument_of S)) = (F . ( Sub_the_left_argument_of S)) by A9;

            now

              per cases ;

                suppose ( len ( @ (S `1 ))) <> (n + 1);

                then ( len ( @ (S `1 ))) <= n & (H . S) = (F . S) by A9, A10, NAT_1: 8;

                hence thesis by A2, A13, A15, A14;

              end;

                suppose ( len ( @ (S `1 ))) = (n + 1);

                hence thesis by A9, A13, A15, A14;

              end;

            end;

            hence thesis;

          end;

          thus S is Sub_universal implies (H . S) = R(Al,S,.)

          proof

            assume

             A16: S is Sub_universal;

            then ( len ( @ (( Sub_the_scope_of S) `1 ))) <> (n + 1) by A10, Th24;

            then

             A17: (H . ( Sub_the_scope_of S)) = (F . ( Sub_the_scope_of S)) by A9;

            now

              per cases ;

                suppose ( len ( @ (S `1 ))) <> (n + 1);

                then ( len ( @ (S `1 ))) <= n & (H . S) = (F . S) by A9, A10, NAT_1: 8;

                hence thesis by A2, A16, A17;

              end;

                suppose ( len ( @ (S `1 ))) = (n + 1);

                hence thesis by A9, A16, A17;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      

       A18: S[ 0 ]

      proof

        set F = the Function of ( QC-Sub-WFF Al()), D();

        take F;

        let S be Element of ( QC-Sub-WFF Al());

        assume ( len ( @ (S `1 ))) <= 0 ;

        hence thesis by QC_LANG1: 10;

      end;

      

       A19: for n be Nat holds S[n] from NAT_1:sch 2( A18, A1);

      

       A20: for x be object st x in ( QC-Sub-WFF Al()) holds ex y be object st Qfn[x, y]

      proof

        let x be object;

        assume x in ( QC-Sub-WFF Al());

        then

        reconsider x9 = x as Element of ( QC-Sub-WFF Al());

        consider F be Function of ( QC-Sub-WFF Al()), D() such that

         A21: Pfn[F, ( len ( @ (x9 `1 ))) qua Nat] by A19;

        take (F . x), x9;

        thus x9 = x;

        let G be Function of ( QC-Sub-WFF Al()), D() such that

         A22: Pfn[G, ( len ( @ (x9 `1 ))) qua Nat];

        defpred Pro[ Element of ( QC-Sub-WFF Al())] means ( len ( @ ($1 `1 ))) <= ( len ( @ (x9 `1 ))) implies (F . $1) = (G . $1);

         A23:

        now

          let S be Element of ( QC-Sub-WFF Al());

          thus S is Sub_atomic implies Pro[S]

          proof

            assume

             A24: S is Sub_atomic & ( len ( @ (S `1 ))) <= ( len ( @ (x9 `1 )));

            

            hence (F . S) = A(S) by A21

            .= (G . S) by A22, A24;

          end;

          thus S is Al() -Sub_VERUM implies Pro[S]

          proof

            assume

             A25: S is Al() -Sub_VERUM & ( len ( @ (S `1 ))) <= ( len ( @ (x9 `1 )));

            

            hence (F . S) = V() by A21

            .= (G . S) by A22, A25;

          end;

          thus S is Sub_negative & Pro[( Sub_the_argument_of S)] implies Pro[S]

          proof

            assume that

             A26: S is Sub_negative and

             A27: Pro[( Sub_the_argument_of S)] and

             A28: ( len ( @ (S `1 ))) <= ( len ( @ (x9 `1 )));

            ( len ( @ (( Sub_the_argument_of S) `1 ))) < ( len ( @ (S `1 ))) by A26, Th22;

            

            hence (F . S) = N(.) by A21, A26, A27, A28, XXREAL_0: 2

            .= (G . S) by A22, A26, A28;

          end;

          thus S is Sub_conjunctive & Pro[( Sub_the_left_argument_of S)] & Pro[( Sub_the_right_argument_of S)] implies Pro[S]

          proof

            assume that

             A29: S is Sub_conjunctive and

             A30: Pro[( Sub_the_left_argument_of S)] & Pro[( Sub_the_right_argument_of S)] and

             A31: ( len ( @ (S `1 ))) <= ( len ( @ (x9 `1 )));

            ( len ( @ (( Sub_the_left_argument_of S) `1 ))) < ( len ( @ (S `1 ))) & ( len ( @ (( Sub_the_right_argument_of S) `1 ))) < ( len ( @ (S `1 ))) by A29, Th23;

            

            hence (F . S) = C(.,.) by A21, A29, A30, A31, XXREAL_0: 2

            .= (G . S) by A22, A29, A31;

          end;

          thus S is Sub_universal & Pro[( Sub_the_scope_of S)] implies Pro[S]

          proof

            assume that

             A32: S is Sub_universal and

             A33: Pro[( Sub_the_scope_of S)] and

             A34: ( len ( @ (S `1 ))) <= ( len ( @ (x9 `1 )));

            ( len ( @ (( Sub_the_scope_of S) `1 ))) < ( len ( @ (S `1 ))) by A32, Th24;

            

            hence (F . S) = R(Al,S,.) by A21, A32, A33, A34, XXREAL_0: 2

            .= (G . S) by A22, A32, A34;

          end;

        end;

        for S be Element of ( QC-Sub-WFF Al()) holds Pro[S] from SubQCInd2( A23);

        hence thesis;

      end;

      consider F be Function such that

       A35: ( dom F) = ( QC-Sub-WFF Al()) and

       A36: for x be object st x in ( QC-Sub-WFF Al()) holds Qfn[x, (F . x)] from CLASSES1:sch 1( A20);

      ( rng F) c= D()

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A37: x in ( QC-Sub-WFF Al()) & y = (F . x) by A35, FUNCT_1:def 3;

        consider S be Element of ( QC-Sub-WFF Al()) such that S = x and

         A38: for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S `1 ))) qua Nat] holds y = (g . S) by A36, A37;

        consider G be Function of ( QC-Sub-WFF Al()), D() such that

         A39: Pfn[G, ( len ( @ (S `1 ))) qua Nat] by A19;

        y = (G . S) by A38, A39;

        hence thesis;

      end;

      then

      reconsider F as Function of ( QC-Sub-WFF Al()), D() by A35, FUNCT_2:def 1, RELSET_1: 4;

      take F;

      let S be Element of ( QC-Sub-WFF Al());

      consider S1 be Element of ( QC-Sub-WFF Al()) such that

       A40: S1 = S and

       A41: for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S1 `1 ))) qua Nat] holds (F . S) = (g . S1) by A36;

      let d1,d2 be Element of D();

      consider G be Function of ( QC-Sub-WFF Al()), D() such that

       A42: Pfn[G, ( len ( @ (S1 `1 ))) qua Nat] by A19;

      set S9 = ( Sub_the_scope_of S);

      

       A43: ex S1 be Element of ( QC-Sub-WFF Al()) st S1 = S9 & for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S1 `1 ))) qua Nat] holds (F . S9) = (g . S1) by A36;

      

       A44: (F . S) = (G . S) by A40, A41, A42;

      hence S is Al() -Sub_VERUM implies (F . S) = V() by A40, A42;

      thus S is Sub_atomic implies (F . S) = A(S) by A40, A42, A44;

      

       A45: for k be Nat st k < ( len ( @ (S `1 ))) holds Pfn[G, k]

      proof

        let k be Nat;

        assume

         A46: k < ( len ( @ (S `1 )));

        let S9 be Element of ( QC-Sub-WFF Al());

        assume ( len ( @ (S9 `1 ))) <= k;

        then ( len ( @ (S9 `1 ))) <= ( len ( @ (S `1 ))) by A46, XXREAL_0: 2;

        hence thesis by A40, A42;

      end;

      thus S is Sub_negative & d1 = (F . ( Sub_the_argument_of S)) implies (F . S) = N(d1)

      proof

        set S9 = ( Sub_the_argument_of S);

        set k = ( len ( @ (S9 `1 )));

        

         A47: ex S1 be Element of ( QC-Sub-WFF Al()) st S1 = S9 & for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S1 `1 ))) qua Nat] holds (F . S9) = (g . S1) by A36;

        assume

         A48: S is Sub_negative;

        then k < ( len ( @ (S `1 ))) by Th22;

        then Pfn[G, k qua Nat] by A45;

        then (F . S9) = (G . S9) by A47;

        hence thesis by A40, A42, A44, A48;

      end;

      thus S is Sub_conjunctive & d1 = (F . ( Sub_the_left_argument_of S)) & d2 = (F . ( Sub_the_right_argument_of S)) implies (F . S) = C(d1,d2)

      proof

        set S99 = ( Sub_the_right_argument_of S);

        set S9 = ( Sub_the_left_argument_of S);

        set k9 = ( len ( @ (S9 `1 )));

        set k99 = ( len ( @ (S99 `1 )));

        

         A49: ex S2 be Element of ( QC-Sub-WFF Al()) st S2 = S99 & for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S2 `1 ))) qua Nat] holds (F . S99) = (g . S2) by A36;

        assume

         A50: S is Sub_conjunctive;

        then k9 < ( len ( @ (S `1 ))) by Th23;

        then

         A51: Pfn[G, k9 qua Nat] by A45;

        k99 < ( len ( @ (S `1 ))) by A50, Th23;

        then Pfn[G, k99 qua Nat] by A45;

        then

         A52: (F . S99) = (G . S99) by A49;

        ex S1 be Element of ( QC-Sub-WFF Al()) st S1 = S9 & for g be Function of ( QC-Sub-WFF Al()), D() st Pfn[g, ( len ( @ (S1 `1 ))) qua Nat] holds (F . S9) = (g . S1) by A36;

        then (F . S9) = (G . S9) by A51;

        hence thesis by A40, A42, A44, A50, A52;

      end;

      set k = ( len ( @ (S9 `1 )));

      assume

       A53: S is Sub_universal;

      then k < ( len ( @ (S `1 ))) by Th24;

      then Pfn[G, k qua Nat] by A45;

      then (F . S9) = (G . S9) by A43;

      hence thesis by A40, A42, A44, A53;

    end;

    scheme :: SUBSTUT1:sch4

    SubQCFuncUniq { Al() -> QC-alphabet , D() -> non empty set , F1() -> Function of ( QC-Sub-WFF Al()), D() , F2() -> Function of ( QC-Sub-WFF Al()), D() , V() -> Element of D() , A( set) -> Element of D() , N( set) -> Element of D() , C( set, set) -> Element of D() , R( set, set, set) -> Element of D() } :

F1() = F2()

      provided

       A1: for S be Element of ( QC-Sub-WFF Al()) holds for d1,d2 be Element of D() holds (S is Al() -Sub_VERUM implies (F1() . S) = V()) & (S is Sub_atomic implies (F1() . S) = A(S)) & (S is Sub_negative & d1 = (F1() . ( Sub_the_argument_of S)) implies (F1() . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F1() . ( Sub_the_left_argument_of S)) & d2 = (F1() . ( Sub_the_right_argument_of S)) implies (F1() . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F1() . ( Sub_the_scope_of S)) implies (F1() . S) = R(Al,S,d1))

       and

       A2: for S be Element of ( QC-Sub-WFF Al()) holds for d1,d2 be Element of D() holds (S is Al() -Sub_VERUM implies (F2() . S) = V()) & (S is Sub_atomic implies (F2() . S) = A(S)) & (S is Sub_negative & d1 = (F2() . ( Sub_the_argument_of S)) implies (F2() . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F2() . ( Sub_the_left_argument_of S)) & d2 = (F2() . ( Sub_the_right_argument_of S)) implies (F2() . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F2() . ( Sub_the_scope_of S)) implies (F2() . S) = R(Al,S,d1));

      defpred Pro[ Element of ( QC-Sub-WFF Al())] means (F1() . $1) = (F2() . $1);

      

       A3: for k holds for P be QC-pred_symbol of k, Al(), l be QC-variable_list of k, Al(), e be Element of ( vSUB Al()) holds Pro[( Sub_P (P,l,e))]

      proof

        let k;

        let P be QC-pred_symbol of k, Al(), l be QC-variable_list of k, Al();

        let e be Element of ( vSUB Al());

        

        thus (F1() . ( Sub_P (P,l,e))) = A(Sub_P) by A1

        .= (F2() . ( Sub_P (P,l,e))) by A2;

      end;

      

       A4: for x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x] st [S, x] is quantifiable & Pro[S] holds Pro[( Sub_All ( [S, x],SQ))]

      proof

        let x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x] such that

         A5: [S, x] is quantifiable and

         A6: (F1() . S) = (F2() . S);

        

         A7: ( Sub_All ( [S, x],SQ)) is Sub_universal by A5;

        ( Sub_the_scope_of ( Sub_All ( [S, x],SQ))) = ( [S, x] `1 ) by A5, Th21;

        then ( Sub_the_scope_of ( Sub_All ( [S, x],SQ))) = S;

        

        hence (F1() . ( Sub_All ( [S, x],SQ))) = R(Al,Sub_All,.) by A1, A6, A7

        .= (F2() . ( Sub_All ( [S, x],SQ))) by A2, A7;

      end;

      

       A8: for S be Element of ( QC-Sub-WFF Al()) st S is Al() -Sub_VERUM holds Pro[S]

      proof

        let S be Element of ( QC-Sub-WFF Al());

        assume

         A9: S is Al() -Sub_VERUM;

        then (F1() . S) = V() by A1;

        hence thesis by A2, A9;

      end;

      

       A10: for S1,S2 be Element of ( QC-Sub-WFF Al()) st (S1 `2 ) = (S2 `2 ) & Pro[S1] & Pro[S2] holds Pro[( Sub_& (S1,S2))]

      proof

        let S1,S2 be Element of ( QC-Sub-WFF Al()) such that

         A11: (S1 `2 ) = (S2 `2 ) and

         A12: (F1() . S1) = (F2() . S1) & (F1() . S2) = (F2() . S2);

        

         A13: ( Sub_the_right_argument_of ( Sub_& (S1,S2))) = S2 by A11, Th19;

        

         A14: ( Sub_& (S1,S2)) is Sub_conjunctive & ( Sub_the_left_argument_of ( Sub_& (S1,S2))) = S1 by A11, Th18;

        

        hence (F1() . ( Sub_& (S1,S2))) = C(.,.) by A1, A12, A13

        .= (F2() . ( Sub_& (S1,S2))) by A2, A14, A13;

      end;

      

       A15: for S be Element of ( QC-Sub-WFF Al()) st Pro[S] holds Pro[( Sub_not S)]

      proof

        let S be Element of ( QC-Sub-WFF Al()) such that

         A16: (F1() . S) = (F2() . S);

        

         A17: ( Sub_the_argument_of ( Sub_not S)) = S by Def30;

        

        hence (F1() . ( Sub_not S)) = N(.) by A1, A16

        .= (F2() . ( Sub_not S)) by A2, A17;

      end;

      for S be Element of ( QC-Sub-WFF Al()) holds Pro[S] from SubQCInd( A3, A8, A15, A10, A4);

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let A;

      let S;

      :: SUBSTUT1:def35

      func @ S -> Element of [:( QC-WFF A), ( vSUB A):] equals S;

      coherence

      proof

        ex p, e st S = [p, e] by Th8;

        hence thesis;

      end;

    end

    reserve Z for Element of [:( QC-WFF A), ( vSUB A):];

    definition

      let A;

      let Z;

      :: original: `1

      redefine

      func Z `1 -> Element of ( QC-WFF A) ;

      coherence

      proof

        ex a,b be object st a in ( QC-WFF A) & b in ( vSUB A) & [a, b] = Z by ZFMISC_1:def 2;

        hence thesis;

      end;

      :: original: `2

      redefine

      func Z `2 -> CQC_Substitution of A ;

      coherence

      proof

        ex a,b be object st a in ( QC-WFF A) & b in ( vSUB A) & [a, b] = Z by ZFMISC_1:def 2;

        hence thesis;

      end;

    end

    definition

      let A;

      let Z;

      :: SUBSTUT1:def36

      func S_Bound (Z) -> bound_QC-variable of A equals ( x. ( upVar (( RestrictSub (( bound_in (Z `1 )),(Z `1 ),(Z `2 ))),( the_scope_of (Z `1 ))))) if ( bound_in (Z `1 )) in ( rng ( RestrictSub (( bound_in (Z `1 )),(Z `1 ),(Z `2 ))))

      otherwise ( bound_in (Z `1 ));

      coherence ;

      consistency ;

    end

    definition

      let A;

      let S, p;

      :: SUBSTUT1:def37

      func Quant (S,p) -> Element of ( QC-WFF A) equals ( All (( S_Bound ( @ S)),p));

      coherence ;

    end

    

     Lm6: for F1,F2 be Function of ( QC-Sub-WFF A), ( QC-WFF A) st (for S be Element of ( QC-Sub-WFF A) holds (S is A -Sub_VERUM implies (F1 . S) = ( VERUM A)) & (S is Sub_atomic implies (F1 . S) = (( the_pred_symbol_of (S `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S),(S `2 ))))) & (S is Sub_negative implies (F1 . S) = ( 'not' (F1 . ( Sub_the_argument_of S)))) & (S is Sub_conjunctive implies (F1 . S) = ((F1 . ( Sub_the_left_argument_of S)) '&' (F1 . ( Sub_the_right_argument_of S)))) & (S is Sub_universal implies (F1 . S) = ( Quant (S,(F1 . ( Sub_the_scope_of S)))))) & (for S be Element of ( QC-Sub-WFF A) holds (S is A -Sub_VERUM implies (F2 . S) = ( VERUM A)) & (S is Sub_atomic implies (F2 . S) = (( the_pred_symbol_of (S `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S),(S `2 ))))) & (S is Sub_negative implies (F2 . S) = ( 'not' (F2 . ( Sub_the_argument_of S)))) & (S is Sub_conjunctive implies (F2 . S) = ((F2 . ( Sub_the_left_argument_of S)) '&' (F2 . ( Sub_the_right_argument_of S)))) & (S is Sub_universal implies (F2 . S) = ( Quant (S,(F2 . ( Sub_the_scope_of S)))))) holds F1 = F2

    proof

      let F1,F2 be Function of ( QC-Sub-WFF A), ( QC-WFF A);

      deffunc C( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ($1 '&' $2);

      deffunc N( Element of ( QC-WFF A)) = ( 'not' $1);

      deffunc A2( Element of ( QC-Sub-WFF A)) = (( the_pred_symbol_of ($1 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of $1),($1 `2 ))));

      assume for S be Element of ( QC-Sub-WFF A) holds (S is A -Sub_VERUM implies (F1 . S) = ( VERUM A)) & (S is Sub_atomic implies (F1 . S) = A2(S)) & (S is Sub_negative implies (F1 . S) = N(.)) & (S is Sub_conjunctive implies (F1 . S) = C(.,.)) & (S is Sub_universal implies (F1 . S) = ( Quant (S,(F1 . ( Sub_the_scope_of S)))));

      then

       A1: for S be Element of ( QC-Sub-WFF A) holds for d1,d2 be Element of ( QC-WFF A) holds (S is A -Sub_VERUM implies (F1 . S) = ( VERUM A)) & (S is Sub_atomic implies (F1 . S) = A2(S)) & (S is Sub_negative & d1 = (F1 . ( Sub_the_argument_of S)) implies (F1 . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F1 . ( Sub_the_left_argument_of S)) & d2 = (F1 . ( Sub_the_right_argument_of S)) implies (F1 . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F1 . ( Sub_the_scope_of S)) implies (F1 . S) = ( Quant (S,d1)));

      assume for S be Element of ( QC-Sub-WFF A) holds (S is A -Sub_VERUM implies (F2 . S) = ( VERUM A)) & (S is Sub_atomic implies (F2 . S) = A2(S)) & (S is Sub_negative implies (F2 . S) = N(.)) & (S is Sub_conjunctive implies (F2 . S) = C(.,.)) & (S is Sub_universal implies (F2 . S) = ( Quant (S,(F2 . ( Sub_the_scope_of S)))));

      then

       A2: for S be Element of ( QC-Sub-WFF A) holds for d1,d2 be Element of ( QC-WFF A) holds (S is A -Sub_VERUM implies (F2 . S) = ( VERUM A)) & (S is Sub_atomic implies (F2 . S) = A2(S)) & (S is Sub_negative & d1 = (F2 . ( Sub_the_argument_of S)) implies (F2 . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F2 . ( Sub_the_left_argument_of S)) & d2 = (F2 . ( Sub_the_right_argument_of S)) implies (F2 . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F2 . ( Sub_the_scope_of S)) implies (F2 . S) = ( Quant (S,d1)));

      thus F1 = F2 from SubQCFuncUniq( A1, A2);

    end;

    begin

    definition

      let A;

      let S be Element of ( QC-Sub-WFF A);

      :: SUBSTUT1:def38

      func CQC_Sub (S) -> Element of ( QC-WFF A) means

      : Def38: ex F be Function of ( QC-Sub-WFF A), ( QC-WFF A) st it = (F . S) & for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9)))));

      existence

      proof

        deffunc C( Element of ( QC-WFF A), Element of ( QC-WFF A)) = ($1 '&' $2);

        deffunc N( Element of ( QC-WFF A)) = ( 'not' $1);

        deffunc A2( Element of ( QC-Sub-WFF A)) = (( the_pred_symbol_of ($1 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of $1),($1 `2 ))));

        consider F be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

         A1: for S be Element of ( QC-Sub-WFF A) holds for d1,d2 be Element of ( QC-WFF A) holds (S is A -Sub_VERUM implies (F . S) = ( VERUM A)) & (S is Sub_atomic implies (F . S) = A2(S)) & (S is Sub_negative & d1 = (F . ( Sub_the_argument_of S)) implies (F . S) = N(d1)) & (S is Sub_conjunctive & d1 = (F . ( Sub_the_left_argument_of S)) & d2 = (F . ( Sub_the_right_argument_of S)) implies (F . S) = C(d1,d2)) & (S is Sub_universal & d1 = (F . ( Sub_the_scope_of S)) implies (F . S) = ( Quant (S,d1))) from SubFuncEx;

        take (F . S), F;

        thus (F . S) = (F . S);

        thus thesis by A1;

      end;

      uniqueness by Lm6;

    end

    theorem :: SUBSTUT1:28

    

     Th28: S is Sub_negative implies ( CQC_Sub S) = ( 'not' ( CQC_Sub ( Sub_the_argument_of S)))

    proof

      consider F be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A1: ( CQC_Sub S) = (F . S) and

       A2: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9))))) by Def38;

      consider G be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A3: ( CQC_Sub ( Sub_the_argument_of S)) = (G . ( Sub_the_argument_of S)) and

       A4: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (G . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (G . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (G . S9) = ( 'not' (G . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (G . S9) = ((G . ( Sub_the_left_argument_of S9)) '&' (G . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (G . S9) = ( Quant (S9,(G . ( Sub_the_scope_of S9))))) by Def38;

      F = G by A2, A4, Lm6;

      hence thesis by A1, A2, A3;

    end;

    theorem :: SUBSTUT1:29

    

     Th29: ( CQC_Sub ( Sub_not S)) = ( 'not' ( CQC_Sub S))

    proof

      set 9S = ( Sub_not S);

      ( Sub_the_argument_of 9S) = S by Def30;

      hence thesis by Th28;

    end;

    theorem :: SUBSTUT1:30

    

     Th30: S is Sub_conjunctive implies ( CQC_Sub S) = (( CQC_Sub ( Sub_the_left_argument_of S)) '&' ( CQC_Sub ( Sub_the_right_argument_of S)))

    proof

      consider F be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A1: ( CQC_Sub S) = (F . S) and

       A2: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9))))) by Def38;

      consider F2 be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A3: ( CQC_Sub ( Sub_the_right_argument_of S)) = (F2 . ( Sub_the_right_argument_of S)) and

       A4: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F2 . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F2 . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F2 . S9) = ( 'not' (F2 . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F2 . S9) = ((F2 . ( Sub_the_left_argument_of S9)) '&' (F2 . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F2 . S9) = ( Quant (S9,(F2 . ( Sub_the_scope_of S9))))) by Def38;

      

       A5: F2 = F by A2, A4, Lm6;

      consider F1 be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A6: ( CQC_Sub ( Sub_the_left_argument_of S)) = (F1 . ( Sub_the_left_argument_of S)) and

       A7: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F1 . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F1 . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F1 . S9) = ( 'not' (F1 . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F1 . S9) = ((F1 . ( Sub_the_left_argument_of S9)) '&' (F1 . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F1 . S9) = ( Quant (S9,(F1 . ( Sub_the_scope_of S9))))) by Def38;

      F1 = F by A2, A7, Lm6;

      hence thesis by A1, A2, A6, A3, A5;

    end;

    theorem :: SUBSTUT1:31

    

     Th31: (S1 `2 ) = (S2 `2 ) implies ( CQC_Sub ( Sub_& (S1,S2))) = (( CQC_Sub S1) '&' ( CQC_Sub S2))

    proof

      set S = ( Sub_& (S1,S2));

      assume

       A1: (S1 `2 ) = (S2 `2 );

      then ( Sub_the_left_argument_of S) = S1 & ( Sub_the_right_argument_of S) = S2 by Th18, Th19;

      hence thesis by A1, Th13, Th30;

    end;

    theorem :: SUBSTUT1:32

    

     Th32: S is Sub_universal implies ( CQC_Sub S) = ( Quant (S,( CQC_Sub ( Sub_the_scope_of S))))

    proof

      consider F be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A1: ( CQC_Sub S) = (F . S) and

       A2: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9))))) by Def38;

      consider G be Function of ( QC-Sub-WFF A), ( QC-WFF A) such that

       A3: ( CQC_Sub ( Sub_the_scope_of S)) = (G . ( Sub_the_scope_of S)) and

       A4: for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (G . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (G . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (G . S9) = ( 'not' (G . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (G . S9) = ((G . ( Sub_the_left_argument_of S9)) '&' (G . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (G . S9) = ( Quant (S9,(G . ( Sub_the_scope_of S9))))) by Def38;

      F = G by A2, A4, Lm6;

      hence thesis by A1, A2, A3;

    end;

    definition

      let A;

      :: SUBSTUT1:def39

      func CQC-Sub-WFF (A) -> Subset of ( QC-Sub-WFF A) equals { S : (S `1 ) is Element of ( CQC-WFF A) };

      coherence

      proof

        set X = { S : (S `1 ) is Element of ( CQC-WFF A) };

        X c= ( QC-Sub-WFF A)

        proof

          let a be object;

          assume a in X;

          then ex S st a = S & (S `1 ) is Element of ( CQC-WFF A);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( CQC-Sub-WFF A) -> non empty;

      coherence

      proof

        set e = the Element of ( vSUB A);

        reconsider S = [( VERUM A), e] as Element of ( QC-Sub-WFF A) by Def16;

        (S `1 ) = ( VERUM A);

        then [( VERUM A), e] in ( CQC-Sub-WFF A);

        hence thesis;

      end;

    end

    theorem :: SUBSTUT1:33

    

     Th33: S is A -Sub_VERUM implies ( CQC_Sub S) is Element of ( CQC-WFF A)

    proof

      assume

       A1: S is A -Sub_VERUM;

      ex F be Function of ( QC-Sub-WFF A), ( QC-WFF A) st ( CQC_Sub S) = (F . S) & for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9))))) by Def38;

      hence thesis by A1;

    end;

    

     Lm7: ( the_pred_symbol_of (P ! ll)) = P

    proof

      

       A1: (( <*P*> ^ ll) . 1) = P by FINSEQ_1: 41;

      (P ! ll) is atomic;

      then

      consider k be Nat, ll9 be QC-variable_list of k, A, P9 be QC-pred_symbol of k, A such that

       A2: ( the_pred_symbol_of (P ! ll)) = P9 & (P ! ll) = (P9 ! ll9) by QC_LANG1:def 22;

      (P ! ll) = ( <*P*> ^ ll) & (P9 ! ll9) = ( <*P9*> ^ ll9) by QC_LANG1: 8;

      hence thesis by A2, A1, FINSEQ_1: 41;

    end;

    theorem :: SUBSTUT1:34

    

     Th34: for h be FinSequence holds h is CQC-variable_list of k, A iff h is FinSequence of ( bound_QC-variables A) & ( len h) = k

    proof

      let h be FinSequence;

      thus h is CQC-variable_list of k, A implies h is FinSequence of ( bound_QC-variables A) & ( len h) = k

      proof

        assume

         A1: h is CQC-variable_list of k, A;

        then ( rng h) c= ( bound_QC-variables A) by RELAT_1:def 19;

        hence h is FinSequence of ( bound_QC-variables A) by FINSEQ_1:def 4;

        thus thesis by A1, CARD_1:def 7;

      end;

      thus h is FinSequence of ( bound_QC-variables A) & ( len h) = k implies h is CQC-variable_list of k, A

      proof

        assume that

         A2: h is FinSequence of ( bound_QC-variables A) and

         A3: ( len h) = k;

        ( rng h) c= ( bound_QC-variables A) by A2, FINSEQ_1:def 4;

        then ( rng h) c= ( QC-variables A) by XBOOLE_1: 1;

        hence thesis by A2, A3, CARD_1:def 7, FINSEQ_1:def 4;

      end;

    end;

    theorem :: SUBSTUT1:35

    

     Th35: ( CQC_Sub ( Sub_P (P,ll,e))) is Element of ( CQC-WFF A)

    proof

      set l = ( Sub_the_arguments_of ( Sub_P (P,ll,e)));

      

       A1: l is CQC-variable_list of k, A by Def29;

      then

      reconsider l as FinSequence of ( bound_QC-variables A) by Th34;

      reconsider s = ( CQC_Subst (l,(( Sub_P (P,ll,e)) `2 ))) as FinSequence of ( bound_QC-variables A);

      ( len l) = k by A1, CARD_1:def 7;

      then

       A2: ( len s) = k by Def3;

      ( Sub_P (P,ll,e)) = [(P ! ll), e] by Th9;

      then (( Sub_P (P,ll,e)) `1 ) = (P ! ll);

      then

      reconsider P9 = ( the_pred_symbol_of (( Sub_P (P,ll,e)) `1 )) as QC-pred_symbol of k, A by Lm7;

      reconsider s as CQC-variable_list of k, A by A2, Th34;

      ex F be Function of ( QC-Sub-WFF A), ( QC-WFF A) st ( CQC_Sub ( Sub_P (P,ll,e))) = (F . ( Sub_P (P,ll,e))) & for S9 be Element of ( QC-Sub-WFF A) holds (S9 is A -Sub_VERUM implies (F . S9) = ( VERUM A)) & (S9 is Sub_atomic implies (F . S9) = (( the_pred_symbol_of (S9 `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S9),(S9 `2 ))))) & (S9 is Sub_negative implies (F . S9) = ( 'not' (F . ( Sub_the_argument_of S9)))) & (S9 is Sub_conjunctive implies (F . S9) = ((F . ( Sub_the_left_argument_of S9)) '&' (F . ( Sub_the_right_argument_of S9)))) & (S9 is Sub_universal implies (F . S9) = ( Quant (S9,(F . ( Sub_the_scope_of S9))))) by Def38;

      then ( CQC_Sub ( Sub_P (P,ll,e))) = (P9 ! s);

      hence thesis;

    end;

    theorem :: SUBSTUT1:36

    

     Th36: ( CQC_Sub S) is Element of ( CQC-WFF A) implies ( CQC_Sub ( Sub_not S)) is Element of ( CQC-WFF A)

    proof

      set S9 = ( Sub_not S);

      assume

       A1: ( CQC_Sub S) is Element of ( CQC-WFF A);

      ( CQC_Sub S9) = ( 'not' ( CQC_Sub S)) by Th29;

      hence thesis by A1, CQC_LANG: 8;

    end;

    theorem :: SUBSTUT1:37

    

     Th37: (S1 `2 ) = (S2 `2 ) & ( CQC_Sub S1) is Element of ( CQC-WFF A) & ( CQC_Sub S2) is Element of ( CQC-WFF A) implies ( CQC_Sub ( Sub_& (S1,S2))) is Element of ( CQC-WFF A)

    proof

      assume

       A1: (S1 `2 ) = (S2 `2 ) & ( CQC_Sub S1) is Element of ( CQC-WFF A) & ( CQC_Sub S2) is Element of ( CQC-WFF A);

      (S1 `2 ) = (S2 `2 ) implies ( CQC_Sub ( Sub_& (S1,S2))) = (( CQC_Sub S1) '&' ( CQC_Sub S2)) by Th31;

      hence thesis by A1, CQC_LANG: 9;

    end;

    reserve xSQ for second_Q_comp of [S, x];

    theorem :: SUBSTUT1:38

    

     Th38: ( CQC_Sub S) is Element of ( CQC-WFF A) & [S, x] is quantifiable implies ( CQC_Sub ( Sub_All ( [S, x],xSQ))) is Element of ( CQC-WFF A)

    proof

      set S9 = ( Sub_All ( [S, x],xSQ));

      assume that

       A1: ( CQC_Sub S) is Element of ( CQC-WFF A) and

       A2: [S, x] is quantifiable;

      ( Sub_the_scope_of S9) = ( [S, x] `1 ) by A2, Th21;

      then ( Quant (S9,( CQC_Sub ( Sub_the_scope_of S9)))) = ( All (( S_Bound ( @ S9)),( CQC_Sub S)));

      then ( Quant (S9,( CQC_Sub ( Sub_the_scope_of S9)))) is Element of ( CQC-WFF A) by A1, CQC_LANG: 13;

      hence thesis by A2, Th14, Th32;

    end;

    reserve S for Element of ( CQC-Sub-WFF A);

    scheme :: SUBSTUT1:sch5

    SubCQCInd { Al() -> QC-alphabet , Pro[ set] } :

for S be Element of ( CQC-Sub-WFF Al()) holds Pro[S]

      provided

       A1: for S,S9 be Element of ( CQC-Sub-WFF Al()), x be bound_QC-variable of Al(), SQ be second_Q_comp of [S, x], k be Nat, ll be CQC-variable_list of k, Al(), P be QC-pred_symbol of k, Al(), e be Element of ( vSUB Al()) holds Pro[( Sub_P (P,ll,e))] & (S is Al() -Sub_VERUM implies Pro[S]) & (Pro[S] implies Pro[( Sub_not S)]) & ((S `2 ) = (S9 `2 ) & Pro[S] & Pro[S9] implies Pro[( Sub_& (S,S9))]) & ( [S, x] is quantifiable & Pro[S] implies Pro[( Sub_All ( [S, x],SQ))]);

      defpred Pro1[ Element of ( QC-Sub-WFF Al())] means $1 is Element of ( CQC-Sub-WFF Al()) implies Pro[$1];

      

       A2: for S be Element of ( QC-Sub-WFF Al()) st Pro1[S] holds Pro1[( Sub_not S)]

      proof

        let S be Element of ( QC-Sub-WFF Al());

        assume

         A3: Pro1[S];

        assume ( Sub_not S) is Element of ( CQC-Sub-WFF Al());

        then ( Sub_not S) in ( CQC-Sub-WFF Al());

        then

        consider S9 be Element of ( QC-Sub-WFF Al()) such that

         A4: ( Sub_not S) = S9 and

         A5: (S9 `1 ) is Element of ( CQC-WFF Al());

        (S9 `1 ) = ( 'not' (S `1 )) by A4;

        then (S `1 ) is Element of ( CQC-WFF Al()) by A5, CQC_LANG: 8;

        then S in ( CQC-Sub-WFF Al());

        hence thesis by A1, A3;

      end;

      

       A6: for k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al()) holds Pro1[( Sub_P (P,ll,e))]

      proof

        let k be Nat, P be QC-pred_symbol of k, Al(), ll be QC-variable_list of k, Al(), e be Element of ( vSUB Al());

        assume ( Sub_P (P,ll,e)) is Element of ( CQC-Sub-WFF Al());

        then ( Sub_P (P,ll,e)) in ( CQC-Sub-WFF Al());

        then

         A7: ex S1 be Element of ( QC-Sub-WFF Al()) st ( Sub_P (P,ll,e)) = S1 & (S1 `1 ) is Element of ( CQC-WFF Al());

        ( Sub_P (P,ll,e)) = [(P ! ll), e] by Th9;

        then

         A8: (P ! ll) is Element of ( CQC-WFF Al()) by A7;

        then

         A9: { (ll . j) : 1 <= j & j <= ( len ll) & (ll . j) in ( fixed_QC-variables Al()) } = {} by CQC_LANG: 7;

        { (ll . i) : 1 <= i & i <= ( len ll) & (ll . i) in ( free_QC-variables Al()) } = {} by A8, CQC_LANG: 7;

        then ll is CQC-variable_list of k, Al() by A9, CQC_LANG: 5;

        hence thesis by A1;

      end;

      

       A10: for S1,S2 be Element of ( QC-Sub-WFF Al()) st (S1 `2 ) = (S2 `2 ) & Pro1[S1] & Pro1[S2] holds Pro1[( Sub_& (S1,S2))]

      proof

        let S1,S2 be Element of ( QC-Sub-WFF Al());

        assume that

         A11: (S1 `2 ) = (S2 `2 ) and

         A12: Pro1[S1] & Pro1[S2];

        assume ( Sub_& (S1,S2)) is Element of ( CQC-Sub-WFF Al());

        then ( Sub_& (S1,S2)) in ( CQC-Sub-WFF Al());

        then

        consider S9 be Element of ( QC-Sub-WFF Al()) such that

         A13: ( Sub_& (S1,S2)) = S9 and

         A14: (S9 `1 ) is Element of ( CQC-WFF Al());

        ( Sub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A11, Def21;

        then

         A15: (S9 `1 ) = ((S1 `1 ) '&' (S2 `1 )) by A13;

        then (S2 `1 ) is Element of ( CQC-WFF Al()) by A14, CQC_LANG: 9;

        then

         A16: S2 in ( CQC-Sub-WFF Al());

        (S1 `1 ) is Element of ( CQC-WFF Al()) by A14, A15, CQC_LANG: 9;

        then S1 in ( CQC-Sub-WFF Al());

        hence thesis by A1, A11, A12, A16;

      end;

      

       A17: for x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x] st [S, x] is quantifiable & Pro1[S] holds Pro1[( Sub_All ( [S, x],SQ))]

      proof

        let x be bound_QC-variable of Al(), S be Element of ( QC-Sub-WFF Al()), SQ be second_Q_comp of [S, x];

        assume that

         A18: [S, x] is quantifiable and

         A19: Pro1[S];

        assume ( Sub_All ( [S, x],SQ)) is Element of ( CQC-Sub-WFF Al());

        then ( Sub_All ( [S, x],SQ)) in ( CQC-Sub-WFF Al());

        then

        consider S9 be Element of ( QC-Sub-WFF Al()) such that

         A20: ( Sub_All ( [S, x],SQ)) = S9 and

         A21: (S9 `1 ) is Element of ( CQC-WFF Al());

        ( Sub_All ( [S, x],SQ)) = [( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))), SQ] by A18, Def24;

        then (S9 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A20;

        then (( [S, x] `1 ) `1 ) is Element of ( CQC-WFF Al()) by A21, CQC_LANG: 13;

        then S in ( CQC-Sub-WFF Al());

        hence thesis by A1, A18, A19;

      end;

      

       A22: for S be Element of ( QC-Sub-WFF Al()) st S is Al() -Sub_VERUM holds Pro1[S] by A1;

      for S be Element of ( QC-Sub-WFF Al()) holds Pro1[S] from SubQCInd( A6, A22, A2, A10, A17);

      hence thesis;

    end;

    definition

      let A;

      let S;

      :: original: CQC_Sub

      redefine

      func CQC_Sub (S) -> Element of ( CQC-WFF A) ;

      coherence

      proof

        defpred P[ Element of ( QC-Sub-WFF A)] means ( CQC_Sub $1) is Element of ( CQC-WFF A);

        

         A1: for S,S9 be Element of ( CQC-Sub-WFF A), x be bound_QC-variable of A, SQ be second_Q_comp of [S, x], k be Nat, ll be CQC-variable_list of k, A, P be QC-pred_symbol of k, A, e be Element of ( vSUB A) holds P[( Sub_P (P,ll,e))] & (S is A -Sub_VERUM implies P[S]) & ( P[S] implies P[( Sub_not S)]) & ((S `2 ) = (S9 `2 ) & P[S] & P[S9] implies P[( Sub_& (S,S9))]) & ( [S, x] is quantifiable & P[S] implies P[( Sub_All ( [S, x],SQ))]) by Th33, Th35, Th36, Th37, Th38;

        for S holds P[S] from SubCQCInd( A1);

        hence thesis;

      end;

    end

    theorem :: SUBSTUT1:39

    ( rng ( @ Sub)) c= ( bound_QC-variables A);