sublemma.miz



    begin

    reserve Al for QC-alphabet;

    reserve a,b,c,d for object,

i,k,n for Nat,

p,q for Element of ( CQC-WFF Al),

x,y,y1 for bound_QC-variable of Al,

A for non empty set,

J for interpretation of Al, A,

v,w for Element of ( Valuations_in (Al,A)),

f,g for Function,

P,P9 for QC-pred_symbol of k, Al,

ll,ll9 for CQC-variable_list of k, Al,

l1 for FinSequence of ( QC-variables Al),

Sub,Sub9,Sub1 for CQC_Substitution of Al,

S,S9,S1,S2 for Element of ( CQC-Sub-WFF Al),

s for QC-symbol of Al;

    theorem :: SUBLEMMA:1

    

     Th1: for f,g,h,h1,h2 be Function st ( dom h1) c= ( dom h) & ( dom h2) c= ( dom h) holds ((f +* g) +* h) = (((f +* h1) +* (g +* h2)) +* h)

    proof

      let f,g,h,h1,h2 be Function such that

       A1: ( dom h1) c= ( dom h) and

       A2: ( dom h2) c= ( dom h);

      ( dom (f +* h1)) = (( dom f) \/ ( dom h1)) & ( dom (g +* h2)) = (( dom g) \/ ( dom h2)) by FUNCT_4:def 1;

      then ( dom ((f +* h1) +* (g +* h2))) = ((( dom f) \/ ( dom h1)) \/ (( dom g) \/ ( dom h2))) by FUNCT_4:def 1;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = (((( dom f) \/ ( dom h1)) \/ (( dom g) \/ ( dom h2))) \/ ( dom h)) by FUNCT_4:def 1;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = ((( dom f) \/ ( dom h1)) \/ ((( dom g) \/ ( dom h2)) \/ ( dom h))) by XBOOLE_1: 4;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = ((( dom f) \/ ( dom h1)) \/ (( dom g) \/ (( dom h2) \/ ( dom h)))) by XBOOLE_1: 4;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = ((( dom f) \/ ( dom h1)) \/ (( dom g) \/ ( dom h))) by A2, XBOOLE_1: 12;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = (((( dom f) \/ ( dom h1)) \/ ( dom h)) \/ ( dom g)) by XBOOLE_1: 4;

      then ( dom (((f +* h1) +* (g +* h2)) +* h)) = ((( dom f) \/ (( dom h1) \/ ( dom h))) \/ ( dom g)) by XBOOLE_1: 4;

      then

       A3: ( dom (((f +* h1) +* (g +* h2)) +* h)) = ((( dom f) \/ ( dom h)) \/ ( dom g)) by A1, XBOOLE_1: 12;

      

       A4: for b be object st b in ( dom ((f +* g) +* h)) holds (((f +* g) +* h) . b) = ((((f +* h1) +* (g +* h2)) +* h) . b)

      proof

        let b be object such that b in ( dom ((f +* g) +* h));

         A5:

        now

          assume

           A6: not b in ( dom h);

          then

           A7: ((((f +* h1) +* (g +* h2)) +* h) . b) = (((f +* h1) +* (g +* h2)) . b) by FUNCT_4: 11;

          

           A8: (((f +* g) +* h) . b) = ((f +* g) . b) by A6, FUNCT_4: 11;

           A9:

          now

            

             A10: not b in ( dom h2) by A2, A6;

            assume

             A11: b in ( dom g);

            ( dom g) c= (( dom g) \/ ( dom h2)) by XBOOLE_1: 7;

            then b in (( dom g) \/ ( dom h2)) by A11;

            then b in ( dom (g +* h2)) by FUNCT_4:def 1;

            then

             A12: ((((f +* h1) +* (g +* h2)) +* h) . b) = ((g +* h2) . b) by A7, FUNCT_4: 13;

            (((f +* g) +* h) . b) = (g . b) by A8, A11, FUNCT_4: 13;

            hence thesis by A12, A10, FUNCT_4: 11;

          end;

          now

            

             A13: not b in ( dom h1) by A1, A6;

            assume

             A14: not b in ( dom g);

             not b in ( dom h2) by A2, A6;

            then not b in (( dom g) \/ ( dom h2)) by A14, XBOOLE_0:def 3;

            then not b in ( dom (g +* h2)) by FUNCT_4:def 1;

            then

             A15: ((((f +* h1) +* (g +* h2)) +* h) . b) = ((f +* h1) . b) by A7, FUNCT_4: 11;

            (((f +* g) +* h) . b) = (f . b) by A8, A14, FUNCT_4: 11;

            hence thesis by A15, A13, FUNCT_4: 11;

          end;

          hence thesis by A9;

        end;

        now

          assume

           A16: b in ( dom h);

          then (((f +* g) +* h) . b) = (h . b) by FUNCT_4: 13;

          hence thesis by A16, FUNCT_4: 13;

        end;

        hence thesis by A5;

      end;

      ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

      then ( dom ((f +* g) +* h)) = ((( dom f) \/ ( dom g)) \/ ( dom h)) by FUNCT_4:def 1;

      hence thesis by A3, A4, FUNCT_1: 2, XBOOLE_1: 4;

    end;

    theorem :: SUBLEMMA:2

    

     Th2: for vS1 be Function st x in ( dom vS1) holds ((vS1 | (( dom vS1) \ {x})) +* (x .--> (vS1 . x))) = vS1

    proof

      let vS1 be Function;

      assume x in ( dom vS1);

      then ((( dom vS1) \ {x}) \/ {x}) = (( dom vS1) \/ {x}) & {x} c= ( dom vS1) by XBOOLE_1: 39, ZFMISC_1: 31;

      then ((( dom vS1) \ {x}) \/ {x}) = ( dom vS1) by XBOOLE_1: 12;

      hence thesis by FUNCT_7: 14;

    end;

    definition

      let Al, A;

      mode Val_Sub of A,Al is PartFunc of ( bound_QC-variables Al), A;

    end

    reserve vS,vS1,vS2 for Val_Sub of A, Al;

    notation

      let Al, A, v, vS;

      synonym v . vS for v +* vS;

    end

    definition

      let Al, A, v, vS;

      :: original: .

      redefine

      func v . vS -> Element of ( Valuations_in (Al,A)) ;

      coherence

      proof

        v is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

        then ex f st v = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

        then ( dom (v +* vS)) = (( bound_QC-variables Al) \/ ( dom vS)) by FUNCT_4:def 1;

        then

         A1: ( dom (v +* vS)) = ( bound_QC-variables Al) by XBOOLE_1: 12;

        ( rng (v +* vS)) c= (( rng v) \/ ( rng vS)) by FUNCT_4: 17;

        then (v +* vS) in ( Funcs (( bound_QC-variables Al),A)) by A1, FUNCT_2:def 2;

        hence thesis by VALUAT_1:def 1;

      end;

    end

    definition

      let Al, S;

      :: original: `1

      redefine

      func S `1 -> Element of ( CQC-WFF Al) ;

      coherence

      proof

        S in ( CQC-Sub-WFF Al);

        then S in { S1 where S1 be Element of ( QC-Sub-WFF Al) : (S1 `1 ) is Element of ( CQC-WFF Al) } by SUBSTUT1:def 39;

        then ex S1 be Element of ( QC-Sub-WFF Al) st S = S1 & (S1 `1 ) is Element of ( CQC-WFF Al);

        hence thesis;

      end;

    end

    definition

      let Al, S, A, v;

      :: SUBLEMMA:def1

      func Val_S (v,S) -> Val_Sub of A, Al equals (( @ (S `2 )) * v);

      coherence ;

    end

    theorem :: SUBLEMMA:3

    

     Th3: S is Al -Sub_VERUM implies ( CQC_Sub S) = ( VERUM Al)

    proof

      ex F be Function of ( QC-Sub-WFF Al), ( QC-WFF Al) st ( CQC_Sub S) = (F . S) & for S9 be Element of ( QC-Sub-WFF Al) holds (S9 is Al -Sub_VERUM implies (F . S9) = ( VERUM Al)) & (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 SUBSTUT1:def 38;

      hence thesis;

    end;

    definition

      let Al, S, A, v, J;

      :: SUBLEMMA:def2

      pred J,v |= S means

      : Def2: (J,v) |= (S `1 );

    end

    theorem :: SUBLEMMA:4

    

     Th4: S is Al -Sub_VERUM implies for v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S)

    proof

      assume

       A1: S is Al -Sub_VERUM;

      let v;

      ex Sub st S = [( VERUM Al), Sub] by A1, SUBSTUT1:def 19;

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

      then (J,(v . ( Val_S (v,S)))) |= ( VERUM Al) iff (J,(v . ( Val_S (v,S)))) |= S;

      hence (J,v) |= ( CQC_Sub S) implies (J,(v . ( Val_S (v,S)))) |= S by VALUAT_1: 32;

      (J,(v . ( Val_S (v,S)))) |= S implies (J,v) |= ( VERUM Al) by VALUAT_1: 32;

      hence thesis by A1, Th3;

    end;

    theorem :: SUBLEMMA:5

    

     Th5: i in ( dom ll) implies (ll . i) is bound_QC-variable of Al

    proof

      assume i in ( dom ll);

      then

       A1: (ll . i) in ( rng ll) by FUNCT_1: 3;

      ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

      hence thesis by A1;

    end;

    theorem :: SUBLEMMA:6

    

     Th6: S is Sub_atomic implies ( CQC_Sub S) = (( the_pred_symbol_of (S `1 )) ! ( CQC_Subst (( Sub_the_arguments_of S),(S `2 ))))

    proof

      ex F be Function of ( QC-Sub-WFF Al), ( QC-WFF Al) st ( CQC_Sub S) = (F . S) & for S9 be Element of ( QC-Sub-WFF Al) holds (S9 is Al -Sub_VERUM implies (F . S9) = ( VERUM Al)) & (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 SUBSTUT1:def 38;

      hence thesis;

    end;

    theorem :: SUBLEMMA:7

    ( Sub_the_arguments_of ( Sub_P (P,ll,Sub))) = ( Sub_the_arguments_of ( Sub_P (P9,ll9,Sub9))) implies ll = ll9

    proof

      assume

       A1: ( Sub_the_arguments_of ( Sub_P (P,ll,Sub))) = ( Sub_the_arguments_of ( Sub_P (P9,ll9,Sub9)));

      consider k1 be Nat, P1 be QC-pred_symbol of k1, Al, ll1 be QC-variable_list of k1, Al, e1 be Element of ( vSUB Al) such that

       A2: ( Sub_the_arguments_of ( Sub_P (P,ll,Sub))) = ll1 and

       A3: ( Sub_P (P,ll,Sub)) = ( Sub_P (P1,ll1,e1)) by SUBSTUT1:def 29;

      

       A4: (P ! ll) = ( <*P*> ^ ll) & (P1 ! ll1) = ( <*P1*> ^ ll1) by QC_LANG1: 8;

      ( Sub_P (P,ll,Sub)) = [(P ! ll), Sub] by SUBSTUT1: 9;

      then [(P ! ll), Sub] = [(P1 ! ll1), e1] by A3, SUBSTUT1: 9;

      then

       A5: ( <*P1*> ^ ll1) = ( <*P*> ^ ll) by A4, XTUPLE_0: 1;

      (( <*P1*> ^ ll1) . 1) = P1 & (( <*P*> ^ ll) . 1) = P by FINSEQ_1: 41;

      then

       A6: ll1 = ll by A5, FINSEQ_1: 33;

      consider k2 be Nat, P2 be QC-pred_symbol of k2, Al, ll2 be QC-variable_list of k2, Al, e2 be Element of ( vSUB Al) such that

       A7: ( Sub_the_arguments_of ( Sub_P (P9,ll9,Sub9))) = ll2 and

       A8: ( Sub_P (P9,ll9,Sub9)) = ( Sub_P (P2,ll2,e2)) by SUBSTUT1:def 29;

      

       A9: (P9 ! ll9) = ( <*P9*> ^ ll9) & (P2 ! ll2) = ( <*P2*> ^ ll2) by QC_LANG1: 8;

      ( Sub_P (P9,ll9,Sub9)) = [(P9 ! ll9), Sub9] by SUBSTUT1: 9;

      then [(P9 ! ll9), Sub9] = [(P2 ! ll2), e2] by A8, SUBSTUT1: 9;

      then

       A10: ( <*P2*> ^ ll2) = ( <*P9*> ^ ll9) by A9, XTUPLE_0: 1;

      (( <*P2*> ^ ll2) . 1) = P2 & (( <*P9*> ^ ll9) . 1) = P9 by FINSEQ_1: 41;

      hence thesis by A1, A2, A7, A6, A10, FINSEQ_1: 33;

    end;

    definition

      let k, Al, P, ll, Sub;

      :: original: Sub_P

      redefine

      func Sub_P (P,ll,Sub) -> Element of ( CQC-Sub-WFF Al) ;

      coherence

      proof

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        then

         A1: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

        ( Sub_P (P,ll,Sub)) = [(P ! ll), Sub] by SUBSTUT1: 9;

        then (( Sub_P (P,ll,Sub)) `1 ) = (P ! ll) & (P ! ll) in ( CQC-WFF Al);

        hence thesis by A1;

      end;

    end

    theorem :: SUBLEMMA:8

    

     Th8: ( CQC_Sub ( Sub_P (P,ll,Sub))) = (P ! ( CQC_Subst (ll,Sub)))

    proof

      

       A1: (P ! ll) is atomic by QC_LANG1:def 18;

      

       A2: ( Sub_P (P,ll,Sub)) = [(P ! ll), Sub] by SUBSTUT1: 9;

      then

       A3: (( Sub_P (P,ll,Sub)) `2 ) = Sub;

      (( Sub_P (P,ll,Sub)) `1 ) = (P ! ll) by A2;

      then ( Sub_the_arguments_of ( Sub_P (P,ll,Sub))) = ll & ( the_pred_symbol_of (( Sub_P (P,ll,Sub)) `1 )) = P by A1, QC_LANG1:def 22, SUBSTUT1:def 29;

      hence thesis by A3, Th6;

    end;

    theorem :: SUBLEMMA:9

    (P ! ( CQC_Subst (ll,Sub))) is Element of ( CQC-WFF Al)

    proof

      ( CQC_Sub ( Sub_P (P,ll,Sub))) = (P ! ( CQC_Subst (ll,Sub))) by Th8;

      hence thesis;

    end;

    theorem :: SUBLEMMA:10

    

     Th10: ( CQC_Subst (ll,Sub)) is CQC-variable_list of k, Al

    proof

      reconsider ll as FinSequence of ( bound_QC-variables Al) by SUBSTUT1: 34;

      reconsider s = ( CQC_Subst (ll,Sub)) as FinSequence of ( bound_QC-variables Al);

      

       A1: s = ( CQC_Subst (( @ ll),Sub)) by SUBSTUT1:def 5;

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

      then ( len ( @ ll)) = k by SUBSTUT1:def 4;

      then ( len s) = k by A1, SUBSTUT1:def 3;

      then s is CQC-variable_list of k, Al by SUBSTUT1: 34;

      hence thesis by A1, SUBSTUT1:def 4;

    end;

    registration

      let Al;

      let k, ll, Sub;

      cluster ( CQC_Subst (ll,Sub)) -> ( bound_QC-variables Al) -valuedk -element;

      coherence by Th10;

    end

    theorem :: SUBLEMMA:11

    

     Th11: not x in ( dom (S `2 )) implies ((v . ( Val_S (v,S))) . x) = (v . x)

    proof

      assume not x in ( dom (S `2 ));

      then

       A1: not x in ( dom ( @ (S `2 ))) by SUBSTUT1:def 2;

      ( dom (( @ (S `2 )) * v)) c= ( dom ( @ (S `2 ))) by RELAT_1: 25;

      then not x in ( dom ( Val_S (v,S))) by A1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SUBLEMMA:12

    

     Th12: x in ( dom (S `2 )) implies ((v . ( Val_S (v,S))) . x) = (( Val_S (v,S)) . x)

    proof

      assume x in ( dom (S `2 ));

      then

       A1: x in ( dom ( @ (S `2 ))) by SUBSTUT1:def 2;

      ( rng ( @ (S `2 ))) c= ( bound_QC-variables Al) & ( dom v) = ( bound_QC-variables Al) by FUNCT_2:def 1;

      then x in ( dom ( Val_S (v,S))) by A1, RELAT_1: 27;

      hence thesis by FUNCT_4: 13;

    end;

    theorem :: SUBLEMMA:13

    

     Th13: ((v . ( Val_S (v,( Sub_P (P,ll,Sub))))) *' ll) = (v *' ( CQC_Subst (ll,Sub)))

    proof

      set S9 = ( Sub_P (P,ll,Sub));

      set ll9 = ( CQC_Subst (ll,Sub));

      

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

      S9 = [(P ! ll), Sub] by SUBSTUT1: 9;

      then

       A2: (S9 `2 ) = Sub;

      

       A3: ( len ((v . ( Val_S (v,S9))) *' ll)) = k by VALUAT_1:def 3;

      then

       A4: ( dom ((v . ( Val_S (v,S9))) *' ll)) = ( Seg k) by FINSEQ_1:def 3;

      

       A5: for j be Nat st j in ( dom ((v . ( Val_S (v,S9))) *' ll)) holds (((v . ( Val_S (v,S9))) *' ll) . j) = ((v *' ( CQC_Subst (ll,Sub))) . j)

      proof

        let j be Nat such that

         A6: j in ( dom ((v . ( Val_S (v,S9))) *' ll));

        

         A7: 1 <= j & j <= k by A4, A6, FINSEQ_1: 1;

        reconsider j as Nat;

        j in ( Seg ( len ll)) by A4, A6, CARD_1:def 7;

        then j in ( dom ll) by FINSEQ_1:def 3;

        then

        reconsider x = (ll . j) as bound_QC-variable of Al by Th5;

         A8:

        now

          assume

           A9: (ll . j) in ( dom Sub);

          then ((v . ( Val_S (v,S9))) . (ll . j)) = (( Val_S (v,S9)) . x) & (ll . j) in ( dom ( @ (S9 `2 ))) by A2, Th12, SUBSTUT1:def 2;

          then ((v . ( Val_S (v,S9))) . (ll . j)) = (v . (( @ (S9 `2 )) . (ll . j))) by FUNCT_1: 13;

          then

           A10: ((v . ( Val_S (v,S9))) . (ll . j)) = (v . ((S9 `2 ) . (ll . j))) by SUBSTUT1:def 2;

          

           A11: (((v . ( Val_S (v,S9))) *' ll) . j) = ((v . ( Val_S (v,S9))) . (ll . j)) by A7, VALUAT_1:def 3;

          (v . (ll9 . j)) = (v . ((S9 `2 ) . (ll . j))) by A2, A1, A7, A9, SUBSTUT1:def 3;

          hence thesis by A7, A10, A11, VALUAT_1:def 3;

        end;

        now

          assume not (ll . j) in ( dom Sub);

          then

           A12: (v . (ll9 . j)) = (v . (ll . j)) & ((v . ( Val_S (v,S9))) . (ll . j)) = (v . x) by A2, A1, A7, Th11, SUBSTUT1:def 3;

          ((v *' ll9) . j) = (v . (ll9 . j)) by A7, VALUAT_1:def 3;

          hence thesis by A7, A12, VALUAT_1:def 3;

        end;

        hence thesis by A8;

      end;

      ( len (v *' ll9)) = k by VALUAT_1:def 3;

      hence thesis by A3, A5, FINSEQ_2: 9;

    end;

    theorem :: SUBLEMMA:14

    

     Th14: (( Sub_P (P,ll,Sub)) `1 ) = (P ! ll)

    proof

      ( Sub_P (P,ll,Sub)) = [(P ! ll), Sub] by SUBSTUT1: 9;

      hence thesis;

    end;

    theorem :: SUBLEMMA:15

    

     Th15: for v holds ((J,v) |= ( CQC_Sub ( Sub_P (P,ll,Sub))) iff (J,(v . ( Val_S (v,( Sub_P (P,ll,Sub)))))) |= ( Sub_P (P,ll,Sub)))

    proof

      set S9 = ( Sub_P (P,ll,Sub));

      set ll9 = ( CQC_Subst (ll,Sub));

      reconsider p = (P ! ll9) as Element of ( CQC-WFF Al);

      reconsider ll9 as CQC-variable_list of k, Al;

      let v;

      

       A1: (( Valid (p,J)) . v) = TRUE iff (v *' ll9) in (J . P) by VALUAT_1: 7;

      

       A2: ((v . ( Val_S (v,S9))) *' ll) in (J . P) iff (( Valid ((P ! ll),J)) . (v . ( Val_S (v,S9)))) = TRUE by VALUAT_1: 7;

      

       A3: (J,(v . ( Val_S (v,S9)))) |= (P ! ll) iff (J,(v . ( Val_S (v,S9)))) |= (( Sub_P (P,ll,Sub)) `1 ) by Th14;

      (J,v) |= ( CQC_Sub ( Sub_P (P,ll,Sub))) iff (J,v) |= p by Th8;

      hence thesis by A1, A2, A3, Th13, VALUAT_1:def 7;

    end;

    theorem :: SUBLEMMA:16

    

     Th16: (( Sub_not S) `1 ) = ( 'not' (S `1 )) & (( Sub_not S) `2 ) = (S `2 )

    proof

      ( Sub_not S) = [( 'not' (S `1 )), (S `2 )] by SUBSTUT1:def 20;

      hence thesis;

    end;

    definition

      let Al, S;

      :: original: Sub_not

      redefine

      func Sub_not S -> Element of ( CQC-Sub-WFF Al) ;

      coherence

      proof

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        then

         A1: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

        ( 'not' (S `1 )) in ( CQC-WFF Al);

        then (( Sub_not S) `1 ) in ( CQC-WFF Al) by Th16;

        hence thesis by A1;

      end;

    end

    theorem :: SUBLEMMA:17

    

     Th17: not (J,(v . ( Val_S (v,S)))) |= S iff (J,(v . ( Val_S (v,S)))) |= ( Sub_not S)

    proof

      

       A1: not (J,(v . ( Val_S (v,S)))) |= (S `1 ) iff (J,(v . ( Val_S (v,S)))) |= ( 'not' (S `1 )) by VALUAT_1: 17;

      (J,(v . ( Val_S (v,S)))) |= ( 'not' (S `1 )) iff (J,(v . ( Val_S (v,S)))) |= (( Sub_not S) `1 ) by Th16;

      hence thesis by A1;

    end;

    theorem :: SUBLEMMA:18

    

     Th18: ( Val_S (v,S)) = ( Val_S (v,( Sub_not S)))

    proof

      ( Sub_not S) = [( 'not' (S `1 )), (S `2 )] by SUBSTUT1:def 20;

      hence thesis;

    end;

    theorem :: SUBLEMMA:19

    

     Th19: (for v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S)) implies for v holds ((J,v) |= ( CQC_Sub ( Sub_not S)) iff (J,(v . ( Val_S (v,( Sub_not S))))) |= ( Sub_not S))

    proof

      assume

       A1: for v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S);

      let v;

      

       A2: (J,v) |= ( 'not' ( CQC_Sub S)) iff not (J,v) |= ( CQC_Sub S) by VALUAT_1: 17;

       not (J,(v . ( Val_S (v,S)))) |= S iff (J,(v . ( Val_S (v,S)))) |= ( Sub_not S) by Th17;

      hence thesis by A1, A2, Th18, SUBSTUT1: 29;

    end;

    definition

      let Al, S1, S2;

      assume

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

      :: SUBLEMMA:def3

      func CQCSub_& (S1,S2) -> Element of ( CQC-Sub-WFF Al) equals

      : Def3: ( Sub_& (S1,S2));

      coherence

      proof

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        then

         A2: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

        ( Sub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A1, SUBSTUT1:def 21;

        then (( Sub_& (S1,S2)) `1 ) = ((S1 `1 ) '&' (S2 `1 ));

        hence thesis by A2;

      end;

    end

    theorem :: SUBLEMMA:20

    

     Th20: (S1 `2 ) = (S2 `2 ) implies (( CQCSub_& (S1,S2)) `1 ) = ((S1 `1 ) '&' (S2 `1 )) & (( CQCSub_& (S1,S2)) `2 ) = (S1 `2 )

    proof

      assume

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

      then ( Sub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by SUBSTUT1:def 21;

      then ( CQCSub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A1, Def3;

      hence thesis;

    end;

    theorem :: SUBLEMMA:21

    

     Th21: (S1 `2 ) = (S2 `2 ) implies (( CQCSub_& (S1,S2)) `2 ) = (S1 `2 )

    proof

      assume

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

      then ( CQCSub_& (S1,S2)) = ( Sub_& (S1,S2)) by Def3;

      then ( CQCSub_& (S1,S2)) = [((S1 `1 ) '&' (S2 `1 )), (S1 `2 )] by A1, SUBSTUT1:def 21;

      hence thesis;

    end;

    theorem :: SUBLEMMA:22

    (S1 `2 ) = (S2 `2 ) implies ( Val_S (v,S1)) = ( Val_S (v,( CQCSub_& (S1,S2)))) & ( Val_S (v,S2)) = ( Val_S (v,( CQCSub_& (S1,S2)))) by Th21;

    theorem :: SUBLEMMA:23

    

     Th23: (S1 `2 ) = (S2 `2 ) implies ( CQC_Sub ( CQCSub_& (S1,S2))) = (( CQC_Sub S1) '&' ( CQC_Sub S2))

    proof

      assume

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

      then ( CQCSub_& (S1,S2)) = ( Sub_& (S1,S2)) by Def3;

      hence thesis by A1, SUBSTUT1: 31;

    end;

    theorem :: SUBLEMMA:24

    

     Th24: (S1 `2 ) = (S2 `2 ) implies ((J,(v . ( Val_S (v,S1)))) |= S1 & (J,(v . ( Val_S (v,S2)))) |= S2 iff (J,(v . ( Val_S (v,( CQCSub_& (S1,S2)))))) |= ( CQCSub_& (S1,S2)))

    proof

      assume

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

      then ( Val_S (v,S1)) = ( Val_S (v,( CQCSub_& (S1,S2)))) by Th21;

      then

       A2: (J,(v . ( Val_S (v,S1)))) |= (S1 `1 ) & (J,(v . ( Val_S (v,S1)))) |= (S2 `1 ) iff (J,(v . ( Val_S (v,( CQCSub_& (S1,S2)))))) |= ((S1 `1 ) '&' (S2 `1 )) by VALUAT_1: 18;

      (J,(v . ( Val_S (v,( CQCSub_& (S1,S2)))))) |= ((S1 `1 ) '&' (S2 `1 )) iff (J,(v . ( Val_S (v,( CQCSub_& (S1,S2)))))) |= (( CQCSub_& (S1,S2)) `1 ) by A1, Th20;

      hence thesis by A1, A2;

    end;

    theorem :: SUBLEMMA:25

    

     Th25: (S1 `2 ) = (S2 `2 ) & (for v holds ((J,v) |= ( CQC_Sub S1) iff (J,(v . ( Val_S (v,S1)))) |= S1)) & (for v holds ((J,v) |= ( CQC_Sub S2) iff (J,(v . ( Val_S (v,S2)))) |= S2)) implies for v holds ((J,v) |= ( CQC_Sub ( CQCSub_& (S1,S2))) iff (J,(v . ( Val_S (v,( CQCSub_& (S1,S2)))))) |= ( CQCSub_& (S1,S2)))

    proof

      assume that

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

       A2: (for v holds ((J,v) |= ( CQC_Sub S1) iff (J,(v . ( Val_S (v,S1)))) |= S1)) & for v holds ((J,v) |= ( CQC_Sub S2) iff (J,(v . ( Val_S (v,S2)))) |= S2);

      let v;

      

       A3: (J,v) |= ( CQC_Sub S1) & (J,v) |= ( CQC_Sub S2) iff (J,(v . ( Val_S (v,S1)))) |= S1 & (J,(v . ( Val_S (v,S2)))) |= S2 by A2;

      (J,v) |= ( CQC_Sub ( CQCSub_& (S1,S2))) iff (J,v) |= (( CQC_Sub S1) '&' ( CQC_Sub S2)) by A1, Th23;

      hence thesis by A1, A3, Th24, VALUAT_1: 18;

    end;

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

SQ for second_Q_comp of B;

    theorem :: SUBLEMMA:26

    

     Th26: B is quantifiable implies (( Sub_All (B,SQ)) `1 ) = ( All ((B `2 ),((B `1 ) `1 ))) & (( Sub_All (B,SQ)) `2 ) = SQ

    proof

      assume B is quantifiable;

      then ( Sub_All (B,SQ)) = [( All ((B `2 ),((B `1 ) `1 ))), SQ] by SUBSTUT1:def 24;

      hence thesis;

    end;

    definition

      let Al;

      let B be Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):];

      :: SUBLEMMA:def4

      attr B is CQC-WFF-like means

      : Def4: (B `1 ) in ( CQC-Sub-WFF Al);

    end

    registration

      let Al;

      cluster CQC-WFF-like for Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):];

      existence

      proof

        set Sub = the CQC_Substitution of Al, x = the bound_QC-variable of Al;

        set B = [ [( VERUM Al), Sub], x];

        

         A1: ( VERUM Al) = <* [ 0 , 0 ]*> by QC_LANG1:def 14;

        

         A2: [ <* [ 0 , 0 ]*>, Sub] in ( QC-Sub-WFF Al) by SUBSTUT1:def 16;

        reconsider S = [( VERUM Al), Sub] as Element of ( QC-Sub-WFF Al) by A1, SUBSTUT1:def 16;

         [( VERUM Al), Sub] in ( QC-Sub-WFF Al) by A2, QC_LANG1:def 14;

        then

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

        take B;

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        

         A3: X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        (S `1 ) is Element of ( CQC-WFF Al);

        then S in ( CQC-Sub-WFF Al) by A3;

        then (B `1 ) in ( CQC-Sub-WFF Al);

        hence thesis;

      end;

    end

    definition

      let Al, S, x;

      :: original: [

      redefine

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

      coherence

      proof

        ( [S, x] `1 ) = S;

        hence thesis by Def4;

      end;

    end

    reserve B for CQC-WFF-like Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):],

xSQ for second_Q_comp of [S, x],

SQ for second_Q_comp of B;

    definition

      let Al, B;

      :: original: `1

      redefine

      func B `1 -> Element of ( CQC-Sub-WFF Al) ;

      coherence by Def4;

    end

    definition

      let Al, B, SQ;

      assume

       A1: B is quantifiable;

      :: SUBLEMMA:def5

      func CQCSub_All (B,SQ) -> Element of ( CQC-Sub-WFF Al) equals

      : Def5: ( Sub_All (B,SQ));

      coherence

      proof

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        then

         A2: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

        ( All ((B `2 ),((B `1 ) `1 ))) in ( CQC-WFF Al);

        then (( Sub_All (B,SQ)) `1 ) in ( CQC-WFF Al) by A1, Th26;

        hence thesis by A2;

      end;

    end

    theorem :: SUBLEMMA:27

    

     Th27: B is quantifiable implies ( CQCSub_All (B,SQ)) is Sub_universal

    proof

      assume

       A1: B is quantifiable;

      then ( Sub_All (B,SQ)) is Sub_universal by SUBSTUT1: 14;

      hence thesis by A1, Def5;

    end;

    definition

      let Al;

      let S;

      :: SUBLEMMA:def6

      func CQCSub_the_scope_of S -> Element of ( CQC-Sub-WFF Al) equals

      : Def6: ( Sub_the_scope_of S);

      coherence

      proof

        consider B be Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):], SQ be second_Q_comp of B such that

         A2: S = ( Sub_All (B,SQ)) and

         A3: (B `1 ) = ( Sub_the_scope_of S) and

         A4: B is quantifiable by A1, SUBSTUT1:def 34;

        set X = { G where G be Element of ( QC-Sub-WFF Al) : (G `1 ) is Element of ( CQC-WFF Al) };

        X = ( CQC-Sub-WFF Al) by SUBSTUT1:def 39;

        then

         A5: for G be Element of ( QC-Sub-WFF Al) holds (G `1 ) is Element of ( CQC-WFF Al) implies G in ( CQC-Sub-WFF Al);

        (S `1 ) = ( All ((B `2 ),((B `1 ) `1 ))) by A2, A4, Th26;

        then ((B `1 ) `1 ) is Element of ( CQC-WFF Al) by CQC_LANG: 13;

        hence thesis by A5, A3;

      end;

    end

    definition

      let Al, S1, p;

      assume that

       A1: S1 is Sub_universal and

       A2: p = ( CQC_Sub ( CQCSub_the_scope_of S1));

      :: SUBLEMMA:def7

      func CQCQuant (S1,p) -> Element of ( CQC-WFF Al) equals

      : Def7: ( Quant (S1,p));

      coherence

      proof

        ( CQCSub_the_scope_of S1) = ( Sub_the_scope_of S1) by A1, Def6;

        then ( CQC_Sub S1) = ( Quant (S1,p)) by A1, A2, SUBSTUT1: 32;

        hence thesis;

      end;

    end

    theorem :: SUBLEMMA:28

    

     Th28: S is Sub_universal implies ( CQC_Sub S) = ( CQCQuant (S,( CQC_Sub ( CQCSub_the_scope_of S))))

    proof

      assume

       A1: S is Sub_universal;

      then ( CQCSub_the_scope_of S) = ( Sub_the_scope_of S) by Def6;

      then ( CQCQuant (S,( CQC_Sub ( CQCSub_the_scope_of S)))) = ( Quant (S,( CQC_Sub ( Sub_the_scope_of S)))) by A1, Def7;

      hence thesis by A1, SUBSTUT1: 32;

    end;

    theorem :: SUBLEMMA:29

    

     Th29: B is quantifiable implies ( CQCSub_the_scope_of ( CQCSub_All (B,SQ))) = (B `1 )

    proof

      assume

       A1: B is quantifiable;

      then

       A2: ( CQCSub_All (B,SQ)) = ( Sub_All (B,SQ)) by Def5;

      then ( CQCSub_All (B,SQ)) is Sub_universal by A1, SUBSTUT1: 14;

      then ( CQCSub_the_scope_of ( CQCSub_All (B,SQ))) = ( Sub_the_scope_of ( Sub_All (B,SQ))) by A2, Def6;

      hence thesis by A1, SUBSTUT1: 21;

    end;

    begin

    theorem :: SUBLEMMA:30

    

     Th30: [S, x] is quantifiable implies ( CQCSub_the_scope_of ( CQCSub_All ( [S, x],xSQ))) = S & ( CQCQuant (( CQCSub_All ( [S, x],xSQ)),( CQC_Sub ( CQCSub_the_scope_of ( CQCSub_All ( [S, x],xSQ)))))) = ( CQCQuant (( CQCSub_All ( [S, x],xSQ)),( CQC_Sub S)))

    proof

      assume [S, x] is quantifiable;

      then ( CQCSub_the_scope_of ( CQCSub_All ( [S, x],xSQ))) = ( [S, x] `1 ) by Th29;

      hence thesis;

    end;

    theorem :: SUBLEMMA:31

    

     Th31: [S, x] is quantifiable implies ( CQCQuant (( CQCSub_All ( [S, x],xSQ)),( CQC_Sub S))) = ( All (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))),( CQC_Sub S)))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set p = ( CQC_Sub ( CQCSub_the_scope_of S1));

      

       A1: ( Quant (S1,p)) = ( All (( S_Bound ( @ S1)),p)) by SUBSTUT1:def 37;

      assume

       A2: [S, x] is quantifiable;

      then ( CQCSub_All ( [S, x],xSQ)) = ( Sub_All ( [S, x],xSQ)) by Def5;

      then ( CQCSub_All ( [S, x],xSQ)) is Sub_universal by A2, SUBSTUT1: 14;

      then

       A3: ( CQCQuant (S1,p)) = ( Quant (S1,p)) by Def7;

      ( CQCQuant (S1,( CQC_Sub S))) = ( CQCQuant (S1,p)) by A2, Th30;

      hence thesis by A2, A3, A1, Th30;

    end;

    theorem :: SUBLEMMA:32

    x in ( dom (S `2 )) implies (v . (( @ (S `2 )) . x)) = ((v . ( Val_S (v,S))) . x)

    proof

      assume x in ( dom (S `2 ));

      then ((v . ( Val_S (v,S))) . x) = (( Val_S (v,S)) . x) & x in ( dom ( @ (S `2 ))) by Th12, SUBSTUT1:def 2;

      hence thesis by FUNCT_1: 13;

    end;

    theorem :: SUBLEMMA:33

    x in ( dom ( @ (S `2 ))) implies (( @ (S `2 )) . x) is bound_QC-variable of Al

    proof

      assume x in ( dom ( @ (S `2 )));

      then (( @ (S `2 )) . x) in ( rng ( @ (S `2 ))) by FUNCT_1: 3;

      hence thesis;

    end;

    theorem :: SUBLEMMA:34

    

     Th34: [:( QC-WFF Al), ( vSUB Al):] c= ( dom ( QSub Al))

    proof

      let a be object;

      assume a in [:( QC-WFF Al), ( vSUB Al):];

      then

      consider b,c be object such that

       A1: b in ( QC-WFF Al) and

       A2: c in ( vSUB Al) and

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

      reconsider Sub = c as CQC_Substitution of Al by A2;

      reconsider p = b as Element of ( QC-WFF Al) by A1;

       A4:

      now

        set b = {} ;

        set a = [ [p, Sub], b];

        assume not p is universal;

        then (p,Sub) PQSub b by SUBSTUT1:def 14;

        then a in ( QSub Al) by SUBSTUT1:def 15;

        hence thesis by A3, FUNCT_1: 1;

      end;

      now

        set b = ( ExpandSub (( bound_in p),( the_scope_of p),( RestrictSub (( bound_in p),p,Sub))));

        set a = [ [p, Sub], b];

        assume p is universal;

        then (p,Sub) PQSub b by SUBSTUT1:def 14;

        then a in ( QSub Al) by SUBSTUT1:def 15;

        hence thesis by A3, FUNCT_1: 1;

      end;

      hence thesis by A4;

    end;

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

    reserve SQ1 for second_Q_comp of B1;

    theorem :: SUBLEMMA:35

    

     Th35: B is quantifiable & B1 is quantifiable & ( Sub_All (B,SQ)) = ( Sub_All (B1,SQ1)) implies (B `2 ) = (B1 `2 ) & SQ = SQ1

    proof

      assume that

       A1: B is quantifiable and

       A2: B1 is quantifiable & ( Sub_All (B,SQ)) = ( Sub_All (B1,SQ1));

      ( Sub_All (B,SQ)) = [( All ((B `2 ),((B `1 ) `1 ))), SQ] by A1, SUBSTUT1:def 24;

      then

       A3: [( All ((B `2 ),((B `1 ) `1 ))), SQ] = [( All ((B1 `2 ),((B1 `1 ) `1 ))), SQ1] by A2, SUBSTUT1:def 24;

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

      hence thesis by A3, QC_LANG2: 5, XTUPLE_0: 1;

    end;

    theorem :: SUBLEMMA:36

    

     Th36: B is quantifiable & B1 is quantifiable & ( CQCSub_All (B,SQ)) = ( Sub_All (B1,SQ1)) implies (B `2 ) = (B1 `2 ) & SQ = SQ1

    proof

      assume that

       A1: B is quantifiable and

       A2: B1 is quantifiable and

       A3: ( CQCSub_All (B,SQ)) = ( Sub_All (B1,SQ1));

      ( Sub_All (B,SQ)) = ( Sub_All (B1,SQ1)) by A1, A3, Def5;

      hence thesis by A1, A2, Th35;

    end;

    theorem :: SUBLEMMA:37

     [S, x] is quantifiable implies ( Sub_the_bound_of ( CQCSub_All ( [S, x],xSQ))) = x

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume

       A1: [S, x] is quantifiable;

      then S1 = ( Sub_All ( [S, x],xSQ)) by Def5;

      then S1 is Sub_universal by A1, SUBSTUT1: 14;

      then

      consider B be Element of [:( QC-Sub-WFF Al), ( bound_QC-variables Al):], SQ be second_Q_comp of B such that

       A2: S1 = ( Sub_All (B,SQ)) and

       A3: (B `2 ) = ( Sub_the_bound_of S1) and

       A4: B is quantifiable by SUBSTUT1:def 33;

      ( [S, x] `2 ) = (B `2 ) by A1, A2, A4, Th36;

      hence thesis by A3;

    end;

    theorem :: SUBLEMMA:38

    

     Th38: [S, x] is quantifiable & x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) implies not ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) & not ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) in ( Bound_Vars (S `1 ))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume that

       A1: [S, x] is quantifiable and

       A2: x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)));

      

       A3: S1 = ( Sub_All ( [S, x],xSQ)) by A1, Def5;

      then (S1 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A1, Th26;

      then

       A4: (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 )));

      then

       A5: ( bound_in (S1 `1 )) = x by QC_LANG2: 7;

      set finSub = ( RestrictSub (( bound_in (S1 `1 )),(S1 `1 ),(S1 `2 )));

      

       A6: ( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) = { s : ( x. s) in ( Bound_Vars ( the_scope_of (S1 `1 ))) } by SUBSTUT1:def 9;

      (S1 `2 ) = xSQ by A1, A3, Th26;

      then

       A7: finSub = ( RestrictSub (x,( All (x,(S `1 ))),xSQ)) by A4, A5;

      set Y = (( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) \/ ( Sub_Var finSub));

      set n = ( upVar (finSub,( the_scope_of (S1 `1 ))));

      ( NSub (( the_scope_of (S1 `1 )),finSub)) = ( NAT \ Y) by SUBSTUT1:def 11;

      then

      reconsider X = ( NAT \ Y) as non empty Subset of ( QC-symbols Al);

      

       A8: n in ( NSub (( the_scope_of (S1 `1 )),finSub))

      proof

        ( upVar (finSub,( the_scope_of (S1 `1 )))) = the Element of ( NSub (( the_scope_of (S1 `1 )),finSub)) by SUBSTUT1:def 12;

        hence thesis;

      end;

      ( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) c= (( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) \/ ( Sub_Var finSub)) & n in ( NAT \ (( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) \/ ( Sub_Var finSub))) by A8, SUBSTUT1:def 11, XBOOLE_1: 7;

      then not n in ( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) by XBOOLE_0:def 5;

      then

       A9: not ( x. n) in ( Bound_Vars ( the_scope_of (S1 `1 ))) by A6;

      (S1 `1 ) = ( All (x,(S `1 ))) by A4;

      then

       A10: not ( x. ( upVar (finSub,( the_scope_of (S1 `1 ))))) in ( Bound_Vars (S `1 )) by A9, QC_LANG2: 7;

      ( Sub_Var finSub) c= Y & n in ( NAT \ (( Dom_Bound_Vars ( the_scope_of (S1 `1 ))) \/ ( Sub_Var finSub))) by A8, SUBSTUT1:def 11, XBOOLE_1: 7;

      then

       A11: not n in ( Sub_Var finSub) by XBOOLE_0:def 5;

      ( Sub_Var finSub) = { s : ( x. s) in ( rng finSub) } by SUBSTUT1:def 10;

      then

       A12: not ( x. ( upVar (finSub,( the_scope_of (S1 `1 ))))) in ( rng finSub) by A11;

      S1 = ( @ S1) by SUBSTUT1:def 35;

      hence thesis by A2, A5, A7, A12, A10, SUBSTUT1:def 36;

    end;

    theorem :: SUBLEMMA:39

    

     Th39: [S, x] is quantifiable & not x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) implies not ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume that

       A1: [S, x] is quantifiable and

       A2: not x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)));

      

       A3: S1 = ( Sub_All ( [S, x],xSQ)) by A1, Def5;

      then

       A4: (S1 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A1, Th26;

      then

       A5: (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 )));

      set finSub = ( RestrictSub (( bound_in (S1 `1 )),(S1 `1 ),(S1 `2 )));

      

       A6: S1 = ( @ S1) by SUBSTUT1:def 35;

      (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 ))) by A4;

      then

       A7: ( bound_in (S1 `1 )) = x by QC_LANG2: 7;

      (S1 `2 ) = xSQ by A1, A3, Th26;

      then not ( bound_in (S1 `1 )) in ( rng finSub) by A2, A7, A5;

      hence thesis by A2, A7, A6, SUBSTUT1:def 36;

    end;

    theorem :: SUBLEMMA:40

    

     Th40: [S, x] is quantifiable implies not ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))

    proof

      assume

       A1: [S, x] is quantifiable;

      then x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) implies thesis by Th38;

      hence thesis by A1, Th39;

    end;

    theorem :: SUBLEMMA:41

    

     Th41: [S, x] is quantifiable implies (S `2 ) = ( ExpandSub (x,(S `1 ),( RestrictSub (x,( All (x,(S `1 ))),xSQ))))

    proof

      set Z = [( All (x,(S `1 ))), xSQ];

      set q = ( All (x,(S `1 )));

      assume [S, x] is quantifiable;

      then

       A1: (( [S, x] `1 ) `2 ) = (( QSub Al) . [( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))), xSQ]) by SUBSTUT1:def 23;

      

       A2: Z in [:( QC-WFF Al), ( vSUB Al):] by ZFMISC_1:def 2;

       [:( QC-WFF Al), ( vSUB Al):] c= ( dom ( QSub Al)) by Th34;

      then [Z, (( [S, x] `1 ) `2 )] in ( QSub Al) by A2, A1, FUNCT_1: 1;

      then [Z, (S `2 )] in ( QSub Al);

      then

      consider p be QC-formula of Al, Sub1, b such that

       A3: [Z, (S `2 )] = [ [p, Sub1], b] and

       A4: (p,Sub1) PQSub b by SUBSTUT1:def 15;

      Z = [p, Sub1] by A3, XTUPLE_0: 1;

      then

       A5: ( All (x,(S `1 ))) = p & xSQ = Sub1 by XTUPLE_0: 1;

      

       A6: q is universal by QC_LANG1:def 21;

      then

       A7: ( bound_in q) = x by QC_LANG1:def 27;

      (S `2 ) = b by A3, XTUPLE_0: 1;

      then (S `2 ) = ( ExpandSub (( bound_in q),( the_scope_of q),( RestrictSub (( bound_in q),q,xSQ)))) by A4, A5, A6, SUBSTUT1:def 14;

      hence thesis by A6, A7, QC_LANG1:def 28;

    end;

    theorem :: SUBLEMMA:42

    ( still_not-bound_in ( VERUM Al)) c= ( Bound_Vars ( VERUM Al)) by QC_LANG3: 3;

    theorem :: SUBLEMMA:43

    

     Th43: ( still_not-bound_in (P ! ll)) = ( Bound_Vars (P ! ll))

    proof

      set l1 = ( the_arguments_of (P ! ll));

      

       A1: (P ! ll) is atomic by QC_LANG1:def 18;

      then

      consider n be Nat, P9 be QC-pred_symbol of n, Al, ll9 be QC-variable_list of n, Al such that

       A2: l1 = ll9 and

       A3: (P ! ll) = (P9 ! ll9) by QC_LANG1:def 23;

      ( Bound_Vars (P ! ll)) = ( Bound_Vars l1) by A1, SUBSTUT1: 3;

      then

       A4: ( Bound_Vars (P ! ll)) = { (l1 . i) : 1 <= i & i <= ( len l1) & (l1 . i) in ( bound_QC-variables Al) } by SUBSTUT1:def 7;

      ( still_not-bound_in (P ! ll)) = ( still_not-bound_in ll) by QC_LANG3: 5;

      then

       A5: ( still_not-bound_in (P ! ll)) = ( variables_in (ll,( bound_QC-variables Al))) by QC_LANG3: 2;

      

       A6: (( <*P9*> ^ ll9) . 1) = P9 & (( <*P*> ^ ll) . 1) = P by FINSEQ_1: 41;

      (P ! ll) = ( <*P*> ^ ll) & (P9 ! ll9) = ( <*P9*> ^ ll9) by QC_LANG1: 8;

      then ll9 = ll by A3, A6, FINSEQ_1: 33;

      hence thesis by A4, A5, A2, QC_LANG3:def 1;

    end;

    theorem :: SUBLEMMA:44

    

     Th44: ( still_not-bound_in p) c= ( Bound_Vars p) implies ( still_not-bound_in ( 'not' p)) c= ( Bound_Vars ( 'not' p))

    proof

      ( 'not' p) is negative by QC_LANG1:def 19;

      then ( Bound_Vars ( 'not' p)) = ( Bound_Vars ( the_argument_of ( 'not' p))) by SUBSTUT1: 4;

      then

       A1: ( Bound_Vars ( 'not' p)) = ( Bound_Vars p) by QC_LANG2: 1;

      assume ( still_not-bound_in p) c= ( Bound_Vars p);

      hence thesis by A1, QC_LANG3: 7;

    end;

    theorem :: SUBLEMMA:45

    

     Th45: ( still_not-bound_in p) c= ( Bound_Vars p) & ( still_not-bound_in q) c= ( Bound_Vars q) implies ( still_not-bound_in (p '&' q)) c= ( Bound_Vars (p '&' q))

    proof

      

       A1: ( still_not-bound_in (p '&' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q)) by QC_LANG3: 10;

      (p '&' q) is conjunctive by QC_LANG1:def 20;

      then ( Bound_Vars (p '&' q)) = (( Bound_Vars ( the_left_argument_of (p '&' q))) \/ ( Bound_Vars ( the_right_argument_of (p '&' q)))) by SUBSTUT1: 5;

      then ( Bound_Vars (p '&' q)) = (( Bound_Vars p) \/ ( Bound_Vars ( the_right_argument_of (p '&' q)))) by QC_LANG2: 4;

      then

       A2: ( Bound_Vars (p '&' q)) = (( Bound_Vars p) \/ ( Bound_Vars q)) by QC_LANG2: 4;

      assume ( still_not-bound_in p) c= ( Bound_Vars p) & ( still_not-bound_in q) c= ( Bound_Vars q);

      hence thesis by A2, A1, XBOOLE_1: 13;

    end;

    theorem :: SUBLEMMA:46

    

     Th46: ( still_not-bound_in p) c= ( Bound_Vars p) implies ( still_not-bound_in ( All (x,p))) c= ( Bound_Vars ( All (x,p)))

    proof

      

       A1: ( still_not-bound_in ( All (x,p))) = (( still_not-bound_in p) \ {x}) by QC_LANG3: 12;

      ( All (x,p)) is universal by QC_LANG1:def 21;

      then ( Bound_Vars ( All (x,p))) = (( Bound_Vars ( the_scope_of ( All (x,p)))) \/ {( bound_in ( All (x,p)))}) by SUBSTUT1: 6;

      then ( Bound_Vars ( All (x,p))) = (( Bound_Vars p) \/ {( bound_in ( All (x,p)))}) by QC_LANG2: 7;

      then (( Bound_Vars p) \ {x}) c= ( Bound_Vars p) & ( Bound_Vars p) c= ( Bound_Vars ( All (x,p))) by XBOOLE_1: 7, XBOOLE_1: 36;

      then

       A2: (( Bound_Vars p) \ {x}) c= ( Bound_Vars ( All (x,p)));

      assume ( still_not-bound_in p) c= ( Bound_Vars p);

      then ( still_not-bound_in ( All (x,p))) c= (( Bound_Vars p) \ {x}) by A1, XBOOLE_1: 33;

      hence thesis by A2;

    end;

    theorem :: SUBLEMMA:47

    

     Th47: for p holds ( still_not-bound_in p) c= ( Bound_Vars p)

    proof

      defpred P[ Element of ( QC-WFF Al)] means ( still_not-bound_in $1) c= ( Bound_Vars $1);

      ( Bound_Vars ( VERUM Al)) = {} by SUBSTUT1: 2;

      then

       A1: for p, q, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[p] implies P[( 'not' p)]) & ( P[p] & P[q] implies P[(p '&' q)]) & ( P[p] implies P[( All (x,p))]) by Th43, Th44, Th45, Th46, QC_LANG3: 3;

      thus for p holds P[p] from CQC_LANG:sch 1( A1);

    end;

    notation

      let Al, A, x;

      let a be Element of A;

      synonym x | a for x .--> a;

    end

    definition

      let Al, A, x;

      let a be Element of A;

      :: original: |

      redefine

      func x | a -> Val_Sub of A, Al ;

      coherence

      proof

        ( dom (x .--> a)) = {x} & ( rng (x .--> a)) = {a} by FUNCOP_1: 8;

        hence thesis by RELSET_1: 4;

      end;

    end

    reserve a for Element of A;

    theorem :: SUBLEMMA:48

    

     Th48: x <> b implies ((v . (x | a)) . b) = (v . b)

    proof

      assume x <> b;

      then not b in ( dom ( {x} --> a)) by TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: SUBLEMMA:49

    

     Th49: x = y implies ((v . (x | a)) . y) = a

    proof

      assume

       A1: x = y;

      then y in {x} by TARSKI:def 1;

      then

       A2: y in ( dom (x .--> a));

      ((x .--> a) . y) = a by A1, FUNCOP_1: 72;

      hence thesis by A2, FUNCT_4: 13;

    end;

    theorem :: SUBLEMMA:50

    

     Th50: (J,v) |= ( All (x,p)) iff for a holds (J,(v . (x | a))) |= p

    proof

      thus (J,v) |= ( All (x,p)) implies for a holds (J,(v . (x | a))) |= p

      proof

        assume

         A1: (J,v) |= ( All (x,p));

        let a;

        for y st x <> y holds ((v . (x | a)) . y) = (v . y) by Th48;

        hence thesis by A1, VALUAT_1: 29;

      end;

      thus (for a holds (J,(v . (x | a))) |= p) implies (J,v) |= ( All (x,p))

      proof

        assume

         A2: for a holds (J,(v . (x | a))) |= p;

        for w st for y st x <> y holds (w . y) = (v . y) holds (J,w) |= p

        proof

          let w such that

           A3: for y st x <> y holds (w . y) = (v . y);

          set c = (w . x);

          

           A4: for b be object st b in ( dom w) holds (w . b) = ((v . (x | c)) . b)

          proof

            let b be object;

            assume b in ( dom w);

            then

            reconsider y = b as bound_QC-variable of Al;

            now

              assume

               A5: x <> y;

              then (w . y) = (v . y) by A3;

              hence thesis by A5, Th48;

            end;

            hence thesis by Th49;

          end;

          (v . (x | c)) is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

          then

           A6: ex f st (v . (x | c)) = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

          w is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

          then ex f st w = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

          then (v . (x | c)) = w by A4, A6, FUNCT_1: 2;

          hence thesis by A2;

        end;

        hence thesis by VALUAT_1: 29;

      end;

    end;

    definition

      let Al, S, x, xSQ, A, v;

      :: SUBLEMMA:def8

      func NEx_Val (v,S,x,xSQ) -> Val_Sub of A, Al equals (( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) * v);

      coherence ;

    end

    definition

      let Al, A;

      let v,w be Val_Sub of A, Al;

      :: original: +*

      redefine

      func v +* w -> Val_Sub of A, Al ;

      coherence

      proof

        ( dom (v +* w)) = (( dom v) \/ ( dom w)) & ( rng (v +* w)) c= A by FUNCT_4:def 1;

        hence thesis;

      end;

    end

    theorem :: SUBLEMMA:51

    

     Th51: [S, x] is quantifiable & x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) implies ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) = ( x. ( upVar (( RestrictSub (x,( All (x,(S `1 ))),xSQ)),(S `1 ))))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume that

       A1: [S, x] is quantifiable and

       A2: x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)));

      

       A3: S1 = ( Sub_All ( [S, x],xSQ)) by A1, Def5;

      then

       A4: (S1 `2 ) = xSQ by A1, Th26;

      

       A5: (S1 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A1, A3, Th26;

      then

       A6: (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 )));

      then

       A7: (S1 `1 ) = ( All (x,(S `1 ))) & x = ( bound_in (S1 `1 )) by QC_LANG2: 7;

      set finSub = ( RestrictSub (( bound_in (S1 `1 )),(S1 `1 ),(S1 `2 )));

      

       A8: ( @ S1) = S1 by SUBSTUT1:def 35;

      (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 ))) by A5;

      then ( bound_in (S1 `1 )) = x by QC_LANG2: 7;

      then ( bound_in (S1 `1 )) in ( rng finSub) by A2, A4, A6;

      then ( S_Bound ( @ S1)) = ( x. ( upVar (finSub,( the_scope_of (S1 `1 ))))) by A8, SUBSTUT1:def 36;

      hence thesis by A4, A7, QC_LANG2: 7;

    end;

    theorem :: SUBLEMMA:52

    

     Th52: [S, x] is quantifiable & not x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) implies ( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) = x

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume that

       A1: [S, x] is quantifiable and

       A2: not x in ( rng ( RestrictSub (x,( All (x,(S `1 ))),xSQ)));

      

       A3: S1 = ( Sub_All ( [S, x],xSQ)) by A1, Def5;

      then

       A4: (S1 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A1, Th26;

      then

       A5: (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 )));

      set finSub = ( RestrictSub (( bound_in (S1 `1 )),(S1 `1 ),(S1 `2 )));

      

       A6: ( @ S1) = S1 by SUBSTUT1:def 35;

      (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 ))) by A4;

      then

       A7: ( bound_in (S1 `1 )) = x by QC_LANG2: 7;

      (S1 `2 ) = xSQ by A1, A3, Th26;

      then not ( bound_in (S1 `1 )) in ( rng finSub) by A2, A7, A5;

      hence thesis by A7, A6, SUBSTUT1:def 36;

    end;

    theorem :: SUBLEMMA:53

    

     Th53: [S, x] is quantifiable implies for a holds ( Val_S ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S)) = (( NEx_Val ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) & ( dom ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) misses {x}

    proof

      assume

       A1: [S, x] is quantifiable;

      set finSub = ( RestrictSub (x,( All (x,(S `1 ))),xSQ));

      let a;

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      

       A2: (S `2 ) = ( ExpandSub (x,(S `1 ),( RestrictSub (x,( All (x,(S `1 ))),xSQ)))) by A1, Th41;

       A3:

      now

        reconsider F = { [x, x]} as Function;

        assume

         A4: not x in ( rng finSub);

        then (S `2 ) = (finSub \/ F) by A2, SUBSTUT1:def 13;

        then

         A5: ( @ (S `2 )) = (finSub \/ F) by SUBSTUT1:def 2;

         A6:

        now

          set q = ( All (x,(S `1 )));

          set X = { y1 : y1 in ( still_not-bound_in q) & y1 is Element of ( dom xSQ) & y1 <> x & y1 <> (xSQ . y1) };

          assume not ( dom finSub) misses {x};

          then (( dom finSub) /\ {x}) <> {} ;

          then

          consider b be object such that

           A7: b in (( dom finSub) /\ {x}) by XBOOLE_0:def 1;

          finSub = (xSQ | X) by SUBSTUT1:def 6;

          then finSub = (( @ xSQ) | X) by SUBSTUT1:def 2;

          then ( @ finSub) = (( @ xSQ) | X) by SUBSTUT1:def 2;

          then ( dom ( @ finSub)) = (( dom ( @ xSQ)) /\ X) by RELAT_1: 61;

          then

           A8: ( dom ( @ finSub)) c= X by XBOOLE_1: 17;

          b in ( dom finSub) by A7, XBOOLE_0:def 4;

          then b in ( dom ( @ finSub)) by SUBSTUT1:def 2;

          then b in X by A8;

          then

           A9: ex y st y = b & y in ( still_not-bound_in q) & y is Element of ( dom xSQ) & y <> x & y <> (xSQ . y);

          b in {x} by A7, XBOOLE_0:def 4;

          hence contradiction by A9, TARSKI:def 1;

        end;

        hence ( dom finSub) misses {x};

        ( dom { [x, x]}) = {x} by RELAT_1: 9;

        then ( dom ( @ finSub)) misses ( dom F) by A6, SUBSTUT1:def 2;

        then

         A10: (( @ finSub) \/ F) = (( @ finSub) +* F) by FUNCT_4: 31;

        (v . (z | a)) is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

        then

         A11: ex f st (v . (z | a)) = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

        

         A12: ( rng F) = {x} by RELAT_1: 9;

        then ( dom (F * (v . (z | a)))) = ( dom F) by A11, RELAT_1: 27;

        then

         A13: ( dom (F * (v . (z | a)))) = {x} by RELAT_1: 9;

        

         A14: { [x, x]} = (x .--> x) by FUNCT_4: 82;

        for b be object st b in ( dom (x | a)) holds ((x | a) . b) = ((F * (v . (z | a))) . b)

        proof

          let b be object such that

           A15: b in ( dom (x | a));

          

           A16: ((F * (v . (z | a))) . b) = ((v . (z | a)) . (F . b)) by A13, A15, FUNCT_1: 12;

          b = x by A15, TARSKI:def 1;

          then ((x | a) . b) = a & (F . b) = x by A14, FUNCOP_1: 72;

          hence thesis by A1, A4, A16, Th49, Th52;

        end;

        then

         A17: (x | a) = (F * (v . (z | a))) by A13, FUNCT_1: 2;

        ((( @ finSub) +* F) * (v . (z | a))) = ((( @ finSub) * (v . (z | a))) +* (F * (v . (z | a)))) by A11, A12, FUNCT_7: 9;

        hence ( Val_S ((v . (z | a)),S)) = (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)) by A10, A5, A17, SUBSTUT1:def 2;

      end;

      now

        reconsider F = { [x, ( x. ( upVar (finSub,(S `1 ))))]} as Function;

        assume

         A18: x in ( rng finSub);

         A19:

        now

          set q = ( All (x,(S `1 )));

          set X = { y1 : y1 in ( still_not-bound_in q) & y1 is Element of ( dom xSQ) & y1 <> x & y1 <> (xSQ . y1) };

          assume ( dom finSub) meets {x};

          then

          consider b be object such that

           A20: b in ( dom finSub) and

           A21: b in {x} by XBOOLE_0: 3;

          finSub = (xSQ | X) by SUBSTUT1:def 6;

          then finSub = (( @ xSQ) | X) by SUBSTUT1:def 2;

          then ( @ finSub) = (( @ xSQ) | X) by SUBSTUT1:def 2;

          then ( dom ( @ finSub)) = (( dom ( @ xSQ)) /\ X) by RELAT_1: 61;

          then

           A22: ( dom ( @ finSub)) c= X by XBOOLE_1: 17;

          b in ( dom ( @ finSub)) by A20, SUBSTUT1:def 2;

          then b in X by A22;

          then ex y st y = b & y in ( still_not-bound_in q) & y is Element of ( dom xSQ) & y <> x & y <> (xSQ . y);

          hence contradiction by A21, TARSKI:def 1;

        end;

        hence ( dom finSub) misses {x};

        ( dom { [x, ( x. ( upVar (finSub,(S `1 ))))]}) = {x} by RELAT_1: 9;

        then ( dom ( @ finSub)) misses ( dom F) by A19, SUBSTUT1:def 2;

        then

         A23: (( @ finSub) \/ F) = (( @ finSub) +* F) by FUNCT_4: 31;

        (v . (z | a)) is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

        then

         A24: ex f st (v . (z | a)) = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

        ( rng F) = {( x. ( upVar (finSub,(S `1 ))))} by RELAT_1: 9;

        then ( dom (F * (v . (z | a)))) = ( dom F) by A24, RELAT_1: 27;

        then

         A25: ( dom (F * (v . (z | a)))) = {x} by RELAT_1: 9;

        

         A26: { [x, ( x. ( upVar (finSub,(S `1 ))))]} = (x .--> ( x. ( upVar (finSub,(S `1 ))))) by FUNCT_4: 82;

        for b be object st b in ( dom (x | a)) holds ((x | a) . b) = ((F * (v . (z | a))) . b)

        proof

          let b be object such that

           A27: b in ( dom (x | a));

          

           A28: ((F * (v . (z | a))) . b) = ((v . (z | a)) . (F . b)) by A25, A27, FUNCT_1: 12;

          b = x by A27, TARSKI:def 1;

          then ((x | a) . b) = a & (F . b) = ( x. ( upVar (finSub,(S `1 )))) by A26, FUNCOP_1: 72;

          hence thesis by A1, A18, A28, Th49, Th51;

        end;

        then

         A29: (x | a) = (F * (v . (z | a))) by A25, FUNCT_1: 2;

        ( rng F) = {( x. ( upVar (finSub,(S `1 ))))} by RELAT_1: 9;

        then

         A30: ((( @ finSub) +* F) * (v . (z | a))) = ((( @ finSub) * (v . (z | a))) +* (F * (v . (z | a)))) by A24, FUNCT_7: 9;

        (S `2 ) = (finSub \/ F) by A2, A18, SUBSTUT1:def 13;

        then ( @ (S `2 )) = (finSub \/ F) by SUBSTUT1:def 2;

        hence ( Val_S ((v . (z | a)),S)) = (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)) by A23, A30, A29, SUBSTUT1:def 2;

      end;

      hence thesis by A3;

    end;

    theorem :: SUBLEMMA:54

    

     Th54: [S, x] is quantifiable implies ((for a holds (J,((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . ( Val_S ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S)))) |= S) iff for a holds (J,((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . (( NEx_Val ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)))) |= S)

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      assume

       A1: [S, x] is quantifiable;

      thus (for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S) implies for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S

      proof

        assume

         A2: for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S;

        let a;

        ( Val_S ((v . (z | a)),S)) = (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)) by A1, Th53;

        hence thesis by A2;

      end;

      thus (for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S

      proof

        assume

         A3: for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        ( Val_S ((v . (z | a)),S)) = (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)) by A1, Th53;

        hence thesis by A3;

      end;

    end;

    theorem :: SUBLEMMA:55

    

     Th55: [S, x] is quantifiable implies for a holds ( NEx_Val ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S,x,xSQ)) = ( NEx_Val (v,S,x,xSQ))

    proof

      assume

       A1: [S, x] is quantifiable;

      set finSub = ( RestrictSub (x,( All (x,(S `1 ))),xSQ));

      set NF1 = ( NEx_Val (v,S,x,xSQ));

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      let a;

      set z = ( S_Bound ( @ S1));

      set NF = ( NEx_Val ((v . (z | a)),S,x,xSQ));

      v is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

      then ex f st v = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

      then ( rng ( @ finSub)) c= ( dom v);

      then

       A2: ( dom NF1) = ( dom ( @ finSub)) by RELAT_1: 27;

      (v . (z | a)) is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

      then ex f st (v . (z | a)) = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

      then

       A3: ( rng ( @ finSub)) c= ( dom (v . (z | a)));

      then

       A4: ( dom NF) = ( dom ( @ finSub)) by RELAT_1: 27;

      for b be object st b in ( dom NF) holds (NF . b) = (NF1 . b)

      proof

        let b be object such that

         A5: b in ( dom NF);

        

         A6: (( @ finSub) . b) in ( rng ( @ finSub)) by A4, A5, FUNCT_1: 3;

        then

        reconsider x = (( @ finSub) . b) as bound_QC-variable of Al;

         not z in ( rng finSub) by A1, Th40;

        then z <> x by A6, SUBSTUT1:def 2;

        then

         A7: ((v . (z | a)) . x) = (v . x) by Th48;

        (NF . b) = ((v . (z | a)) . x) by A5, FUNCT_1: 12;

        hence thesis by A4, A2, A5, A7, FUNCT_1: 12;

      end;

      hence thesis by A3, A2, FUNCT_1: 2, RELAT_1: 27;

    end;

    theorem :: SUBLEMMA:56

    

     Th56: [S, x] is quantifiable implies ((for a holds (J,((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . (( NEx_Val ((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)))) |= S) iff for a holds (J,((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S)

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      assume

       A1: [S, x] is quantifiable;

      thus (for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S

      proof

        assume

         A2: for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        ( NEx_Val ((v . (z | a)),S,x,xSQ)) = ( NEx_Val (v,S,x,xSQ)) by A1, Th55;

        hence thesis by A2;

      end;

      thus (for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S

      proof

        assume

         A3: for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        ( NEx_Val ((v . (z | a)),S,x,xSQ)) = ( NEx_Val (v,S,x,xSQ)) by A1, Th55;

        hence thesis by A3;

      end;

    end;

    begin

    theorem :: SUBLEMMA:57

    

     Th57: ( rng l1) c= ( bound_QC-variables Al) implies ( still_not-bound_in l1) = ( rng l1)

    proof

      

       A1: ( variables_in (l1,( bound_QC-variables Al))) = { (l1 . k) : 1 <= k & k <= ( len l1) & (l1 . k) in ( bound_QC-variables Al) } by QC_LANG3:def 1;

      assume

       A2: ( rng l1) c= ( bound_QC-variables Al);

      

       A3: ( rng l1) c= ( variables_in (l1,( bound_QC-variables Al)))

      proof

        let b be object;

        assume

         A4: b in ( rng l1);

        then

        consider k be Nat such that

         A5: k in ( dom l1) and

         A6: (l1 . k) = b by FINSEQ_2: 10;

        k in ( Seg ( len l1)) by A5, FINSEQ_1:def 3;

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

        hence thesis by A2, A1, A4, A6;

      end;

      ( variables_in (l1,( bound_QC-variables Al))) c= ( rng l1)

      proof

        let b be object;

        assume b in ( variables_in (l1,( bound_QC-variables Al)));

        then

        consider k such that

         A7: b = (l1 . k) and

         A8: 1 <= k & k <= ( len l1) and (l1 . k) in ( bound_QC-variables Al) by A1;

        k in ( Seg ( len l1)) by A8, FINSEQ_1: 1;

        then k in ( dom l1) by FINSEQ_1:def 3;

        hence thesis by A7, FUNCT_1: 3;

      end;

      then ( variables_in (l1,( bound_QC-variables Al))) = ( rng l1) by A3;

      hence thesis by QC_LANG3: 2;

    end;

    theorem :: SUBLEMMA:58

    

     Th58: ( dom v) = ( bound_QC-variables Al) & ( dom (x | a)) = {x}

    proof

      v is Element of ( Funcs (( bound_QC-variables Al),A)) by VALUAT_1:def 1;

      then ex f st v = f & ( dom f) = ( bound_QC-variables Al) & ( rng f) c= A by FUNCT_2:def 2;

      hence ( dom v) = ( bound_QC-variables Al);

      thus thesis;

    end;

    theorem :: SUBLEMMA:59

    

     Th59: (v *' ll) = (ll * (v | ( still_not-bound_in ll)))

    proof

      ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

      then

       A1: ( rng ll) = ( still_not-bound_in ll) by Th57;

      ( dom (v | ( still_not-bound_in ll))) = (( dom v) /\ ( still_not-bound_in ll)) by RELAT_1: 61;

      then ( dom (v | ( still_not-bound_in ll))) = (( bound_QC-variables Al) /\ ( still_not-bound_in ll)) by Th58;

      then ( rng ll) = ( dom (v | ( still_not-bound_in ll))) by A1, XBOOLE_1: 28;

      then

       A2: ( dom (ll * (v | ( still_not-bound_in ll)))) = ( dom ll) by RELAT_1: 27;

      then

       A3: ( dom (ll * (v | ( still_not-bound_in ll)))) = ( Seg ( len ll)) by FINSEQ_1:def 3;

      then

      reconsider f = (ll * (v | ( still_not-bound_in ll))) as FinSequence by FINSEQ_1:def 2;

      ( len f) = ( len ll) by A3, FINSEQ_1:def 3;

      then

       A4: ( len f) = k by SUBSTUT1: 34;

      then

       A5: ( dom f) = ( Seg k) by FINSEQ_1:def 3;

      

       A6: for j be Nat st j in ( dom f) holds (f . j) = ((v *' ll) . j)

      proof

        

         A7: ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

        let j be Nat such that

         A8: j in ( dom f);

        reconsider j as Nat;

        (ll . j) in ( rng ll) by A2, A8, FUNCT_1: 3;

        then (ll . j) in ( bound_QC-variables Al) by A7;

        then

         A9: (ll . j) in ( dom v) by Th58;

        (ll . j) in ( still_not-bound_in ll) by A1, A2, A8, FUNCT_1: 3;

        then (ll . j) in (( dom v) /\ ( still_not-bound_in ll)) by A9, XBOOLE_0:def 4;

        then

         A10: ((v | ( still_not-bound_in ll)) . (ll . j)) = (v . (ll . j)) by FUNCT_1: 48;

        1 <= j & j <= k by A5, A8, FINSEQ_1: 1;

        then ((v | ( still_not-bound_in ll)) . (ll . j)) = ((v *' ll) . j) by A10, VALUAT_1:def 3;

        hence thesis by A2, A8, FUNCT_1: 13;

      end;

      ( len (v *' ll)) = k by VALUAT_1:def 3;

      hence thesis by A4, A6, FINSEQ_2: 9;

    end;

    theorem :: SUBLEMMA:60

    

     Th60: for v, w holds ((v | ( still_not-bound_in (P ! ll))) = (w | ( still_not-bound_in (P ! ll))) implies ((J,v) |= (P ! ll) iff (J,w) |= (P ! ll)))

    proof

      let v, w;

      assume

       A1: (v | ( still_not-bound_in (P ! ll))) = (w | ( still_not-bound_in (P ! ll)));

      

       A2: ( still_not-bound_in (P ! ll)) = ( still_not-bound_in ll) by QC_LANG3: 5;

      

       A3: (w *' ll) in (J . P) iff (( Valid ((P ! ll),J)) . w) = TRUE by VALUAT_1: 7;

      

       A4: (( Valid ((P ! ll),J)) . v) = TRUE iff (v *' ll) in (J . P) by VALUAT_1: 7;

      (ll * (w | ( still_not-bound_in ll))) in (J . P) iff (w *' ll) in (J . P) by Th59;

      hence thesis by A1, A2, A4, A3, Th59, VALUAT_1:def 7;

    end;

    theorem :: SUBLEMMA:61

    

     Th61: (for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p)) implies for v, w holds (v | ( still_not-bound_in ( 'not' p))) = (w | ( still_not-bound_in ( 'not' p))) implies ((J,v) |= ( 'not' p) iff (J,w) |= ( 'not' p))

    proof

      assume

       A1: for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p);

      let v, w;

      

       A2: ( still_not-bound_in ( 'not' p)) = ( still_not-bound_in p) by QC_LANG3: 7;

      assume (v | ( still_not-bound_in ( 'not' p))) = (w | ( still_not-bound_in ( 'not' p)));

      then not (J,v) |= p iff not (J,w) |= p by A1, A2;

      hence thesis by VALUAT_1: 17;

    end;

    theorem :: SUBLEMMA:62

    

     Th62: (for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p)) & (for v, w holds (v | ( still_not-bound_in q)) = (w | ( still_not-bound_in q)) implies ((J,v) |= q iff (J,w) |= q)) implies for v, w holds (v | ( still_not-bound_in (p '&' q))) = (w | ( still_not-bound_in (p '&' q))) implies ((J,v) |= (p '&' q) iff (J,w) |= (p '&' q))

    proof

      assume

       A1: (for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p)) & for v, w holds (v | ( still_not-bound_in q)) = (w | ( still_not-bound_in q)) implies ((J,v) |= q iff (J,w) |= q);

      set X = (( still_not-bound_in p) \/ ( still_not-bound_in q));

      let v, w;

      

       A2: ( still_not-bound_in (p '&' q)) = X by QC_LANG3: 10;

      assume (v | ( still_not-bound_in (p '&' q))) = (w | ( still_not-bound_in (p '&' q)));

      then (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) & (v | ( still_not-bound_in q)) = (w | ( still_not-bound_in q)) by A2, RELAT_1: 153, XBOOLE_1: 7;

      then (J,v) |= p & (J,v) |= q iff (J,w) |= p & (J,w) |= q by A1;

      hence thesis by VALUAT_1: 18;

    end;

    theorem :: SUBLEMMA:63

    

     Th63: for X be set st X c= ( bound_QC-variables Al) holds ( dom (v | X)) = ( dom ((v . (x | a)) | X)) & ( dom (v | X)) = X

    proof

      let X be set;

      

       A1: ( dom ((v . (x | a)) | X)) = (( dom (v . (x | a))) /\ X) by RELAT_1: 61;

      ( dom (v | X)) = (( dom v) /\ X) by RELAT_1: 61;

      then

       A2: ( dom (v | X)) = (( bound_QC-variables Al) /\ X) by Th58;

      assume X c= ( bound_QC-variables Al);

      hence thesis by A2, A1, Th58, XBOOLE_1: 28;

    end;

    theorem :: SUBLEMMA:64

    (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((v . (x | a)) | ( still_not-bound_in p)) = ((w . (x | a)) | ( still_not-bound_in p))

    proof

      assume

       A1: (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p));

      ( dom (v | ( still_not-bound_in p))) = ( dom ((v . (x | a)) | ( still_not-bound_in p))) by Th63;

      then

       A2: ( dom ((v . (x | a)) | ( still_not-bound_in p))) = ( dom ((w . (x | a)) | ( still_not-bound_in p))) by A1, Th63;

      for b be object st b in ( dom ((v . (x | a)) | ( still_not-bound_in p))) holds (((v . (x | a)) | ( still_not-bound_in p)) . b) = (((w . (x | a)) | ( still_not-bound_in p)) . b)

      proof

        let b be object such that

         A3: b in ( dom ((v . (x | a)) | ( still_not-bound_in p)));

        

         A4: (((v . (x | a)) | ( still_not-bound_in p)) . b) = ((v . (x | a)) . b) & (((w . (x | a)) | ( still_not-bound_in p)) . b) = ((w . (x | a)) . b) by A2, A3, FUNCT_1: 47;

        b in ( dom (v | ( still_not-bound_in p))) by A3, Th63;

        then

         A5: ((v | ( still_not-bound_in p)) . b) = (v . b) by FUNCT_1: 47;

        b in ( dom (w | ( still_not-bound_in p))) by A1, A3, Th63;

        then

         A6: (v . b) = (w . b) by A1, A5, FUNCT_1: 47;

         A7:

        now

          assume

           A8: b <> x;

          then ((v . (x | a)) . b) = (v . b) by Th48;

          hence thesis by A4, A6, A8, Th48;

        end;

        now

          assume

           A9: b = x;

          then ((v . (x | a)) . b) = a by Th49;

          hence thesis by A4, A9, Th49;

        end;

        hence thesis by A7;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: SUBLEMMA:65

    ( still_not-bound_in p) c= (( still_not-bound_in ( All (x,p))) \/ {x})

    proof

      set X = (( still_not-bound_in p) \ {x});

      ( still_not-bound_in ( All (x,p))) = X & ( {x} \/ X) = ( {x} \/ ( still_not-bound_in p)) by QC_LANG3: 12, XBOOLE_1: 39;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: SUBLEMMA:66

    

     Th66: (v | (( still_not-bound_in p) \ {x})) = (w | (( still_not-bound_in p) \ {x})) implies ((v . (x | a)) | ( still_not-bound_in p)) = ((w . (x | a)) | ( still_not-bound_in p))

    proof

      

       A1: ( dom ((w . (x | a)) | ( still_not-bound_in p))) = ( still_not-bound_in p) by Th63;

      then

       A2: ( dom ((v . (x | a)) | ( still_not-bound_in p))) = ( dom ((w . (x | a)) | ( still_not-bound_in p))) by Th63;

      assume

       A3: (v | (( still_not-bound_in p) \ {x})) = (w | (( still_not-bound_in p) \ {x}));

      for b be object st b in ( dom ((v . (x | a)) | ( still_not-bound_in p))) holds (((v . (x | a)) | ( still_not-bound_in p)) . b) = (((w . (x | a)) | ( still_not-bound_in p)) . b)

      proof

        let b be object such that

         A4: b in ( dom ((v . (x | a)) | ( still_not-bound_in p)));

        

         A5: (((v . (x | a)) | ( still_not-bound_in p)) . b) = ((v . (x | a)) . b) & (((w . (x | a)) | ( still_not-bound_in p)) . b) = ((w . (x | a)) . b) by A2, A4, FUNCT_1: 47;

         A6:

        now

          assume

           A7: b <> x;

          then

           A8: not b in {x} by TARSKI:def 1;

          b in ( still_not-bound_in p) by A4, Th63;

          then

           A9: b in (( still_not-bound_in p) \ {x}) by A8, XBOOLE_0:def 5;

          then b in ( dom (w | (( still_not-bound_in p) \ {x}))) by Th63;

          then

           A10: ((w | (( still_not-bound_in p) \ {x})) . b) = (w . b) by FUNCT_1: 47;

          

           A11: ((v . (x | a)) . b) = (v . b) & ((w . (x | a)) . b) = (w . b) by A7, Th48;

          b in ( dom (v | (( still_not-bound_in p) \ {x}))) by A9, Th63;

          hence thesis by A3, A5, A10, A11, FUNCT_1: 47;

        end;

        now

          

           A12: (((w . (x | a)) | ( still_not-bound_in p)) . b) = ((w . (x | a)) . b) by A2, A4, FUNCT_1: 47;

          assume

           A13: b = x;

          (((v . (x | a)) | ( still_not-bound_in p)) . b) = ((v . (x | a)) . b) by A4, FUNCT_1: 47;

          then (((v . (x | a)) | ( still_not-bound_in p)) . b) = a by A13, Th49;

          hence thesis by A13, A12, Th49;

        end;

        hence thesis by A6;

      end;

      hence thesis by A1, Th63, FUNCT_1: 2;

    end;

    theorem :: SUBLEMMA:67

    

     Th67: (for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p)) implies for v, w holds (v | ( still_not-bound_in ( All (x,p)))) = (w | ( still_not-bound_in ( All (x,p)))) implies ((J,v) |= ( All (x,p)) iff (J,w) |= ( All (x,p)))

    proof

      assume

       A1: for v, w holds ((v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p));

      set X = (( still_not-bound_in p) \ {x});

      let v, w;

      

       A2: (v | ( still_not-bound_in ( All (x,p)))) = (v | X) by QC_LANG3: 12;

      assume (v | ( still_not-bound_in ( All (x,p)))) = (w | ( still_not-bound_in ( All (x,p))));

      then

       A3: (v | X) = (w | X) by A2, QC_LANG3: 12;

      

       A4: (for a holds (J,(w . (x | a))) |= p) implies for a holds (J,(v . (x | a))) |= p

      proof

        assume

         A5: for a holds (J,(w . (x | a))) |= p;

        let a;

        ((v . (x | a)) | ( still_not-bound_in p)) = ((w . (x | a)) | ( still_not-bound_in p)) by A3, Th66;

        then (J,(v . (x | a))) |= p iff (J,(w . (x | a))) |= p by A1;

        hence thesis by A5;

      end;

      (for a holds (J,(v . (x | a))) |= p) implies for a holds (J,(w . (x | a))) |= p

      proof

        assume

         A6: for a holds (J,(v . (x | a))) |= p;

        let a;

        ((v . (x | a)) | ( still_not-bound_in p)) = ((w . (x | a)) | ( still_not-bound_in p)) by A3, Th66;

        then (J,(v . (x | a))) |= p iff (J,(w . (x | a))) |= p by A1;

        hence thesis by A6;

      end;

      hence thesis by A4, Th50;

    end;

    theorem :: SUBLEMMA:68

    

     Th68: for p holds for v, w holds (v | ( still_not-bound_in p)) = (w | ( still_not-bound_in p)) implies ((J,v) |= p iff (J,w) |= p)

    proof

      defpred P[ Element of ( CQC-WFF Al)] means for v, w holds (v | ( still_not-bound_in $1)) = (w | ( still_not-bound_in $1)) implies ((J,v) |= $1 iff (J,w) |= $1);

      

       A1: for p, q, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[p] implies P[( 'not' p)]) & ( P[p] & P[q] implies P[(p '&' q)]) & ( P[p] implies P[( All (x,p))]) by Th60, Th61, Th62, Th67, VALUAT_1: 32;

      thus for p holds P[p] from CQC_LANG:sch 1( A1);

    end;

    theorem :: SUBLEMMA:69

    

     Th69: [S, x] is quantifiable implies (((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a))) | ( still_not-bound_in (S `1 ))) = ((v . (( NEx_Val (v,S,x,xSQ)) +* (x | a))) | ( still_not-bound_in (S `1 )))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      set finSub = ( RestrictSub (x,( All (x,(S `1 ))),xSQ));

      set V1 = ((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

      set V2 = (v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

      set X = ( still_not-bound_in (S `1 ));

      

       A1: ( dom V1) = (( dom (v . (z | a))) \/ ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) by FUNCT_4:def 1;

      ( dom (v . (z | a))) = ( bound_QC-variables Al) by Th58;

      then ( dom (v . (z | a))) = ( dom v) by Th58;

      then

       A2: ( dom V1) = ( dom V2) by A1, FUNCT_4:def 1;

      assume

       A3: [S, x] is quantifiable;

       A4:

      now

        assume not x in ( rng finSub);

        then

         A5: z = x by A3, Th52;

        for b be object st b in ( dom V1) holds (V1 . b) = (V2 . b)

        proof

          let b be object such that

           A6: b in ( dom V1);

           A7:

          now

            assume

             A8: b <> z;

             A9:

            now

              

               A10: not b in ( dom (x | a)) by A5, A8, TARSKI:def 1;

              assume not b in ( dom ( NEx_Val (v,S,x,xSQ)));

              then not b in (( dom ( NEx_Val (v,S,x,xSQ))) \/ ( dom (x | a))) by A10, XBOOLE_0:def 3;

              then

               A11: not b in ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a))) by FUNCT_4:def 1;

              reconsider x = b as bound_QC-variable of Al by A6;

              (V1 . b) = ((v . (z | a)) . b) by A11, FUNCT_4: 11;

              then (V1 . b) = (v . x) by A8, Th48;

              hence thesis by A11, FUNCT_4: 11;

            end;

            now

              ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a))) = (( dom ( NEx_Val (v,S,x,xSQ))) \/ ( dom (x | a))) by FUNCT_4:def 1;

              then

               A12: ( dom ( NEx_Val (v,S,x,xSQ))) c= ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a))) by XBOOLE_1: 7;

              assume

               A13: b in ( dom ( NEx_Val (v,S,x,xSQ)));

              then (V1 . b) = ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) . b) by A12, FUNCT_4: 13;

              hence thesis by A13, A12, FUNCT_4: 13;

            end;

            hence thesis by A9;

          end;

          now

            assume b = z;

            then b in {x} by A5, TARSKI:def 1;

            then

             A14: b in ( dom (x | a));

            ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a))) = (( dom ( NEx_Val (v,S,x,xSQ))) \/ ( dom (x | a))) by FUNCT_4:def 1;

            then

             A15: ( dom (x | a)) c= ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a))) by XBOOLE_1: 7;

            then (V1 . b) = ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) . b) by A14, FUNCT_4: 13;

            hence thesis by A14, A15, FUNCT_4: 13;

          end;

          hence thesis by A7;

        end;

        hence thesis by A2, FUNCT_1: 2;

      end;

      now

        assume

         A16: x in ( rng finSub);

        

         A17: ( dom (V1 | X)) = ((( dom (v . (z | a))) \/ ( dom (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) /\ X) by A1, RELAT_1: 61;

        

         A18: for b be object st b in ( dom (V1 | X)) holds ((V1 | X) . b) = ((V2 | X) . b)

        proof

          

           A19: X c= ( Bound_Vars (S `1 )) by Th47;

          let b be object such that

           A20: b in ( dom (V1 | X));

          b in X by A17, A20, XBOOLE_0:def 4;

          then

           A21: b <> z by A3, A16, A19, Th38;

          

           A22: (V2 | X) = ((v | X) +* ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X)) by FUNCT_4: 71;

          

           A23: (V1 | X) = (((v . (z | a)) | X) +* ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X)) by FUNCT_4: 71;

          then

           A24: ( dom (V1 | X)) = (( dom ((v . (z | a)) | X)) \/ ( dom ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X))) by FUNCT_4:def 1;

           A25:

          now

            assume

             A26: not b in ( dom ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X));

            then

             A27: b in ( dom ((v . (z | a)) | X)) by A20, A24, XBOOLE_0:def 3;

            then b in (( dom (v . (z | a))) /\ X) by RELAT_1: 61;

            then

             A28: b in X by XBOOLE_0:def 4;

            b in ( bound_QC-variables Al) by A20;

            then b in ( dom v) by Th58;

            then

             A29: b in (( dom v) /\ X) by A28, XBOOLE_0:def 4;

            ((V1 | X) . b) = (((v . (z | a)) | X) . b) by A23, A26, FUNCT_4: 11;

            then ((V1 | X) . b) = ((v . (z | a)) . b) by A27, FUNCT_1: 47;

            then

             A30: ((V1 | X) . b) = (v . b) by A21, Th48;

            ((V2 | X) . b) = ((v | X) . b) by A22, A26, FUNCT_4: 11;

            hence thesis by A30, A29, FUNCT_1: 48;

          end;

          now

            assume

             A31: b in ( dom ((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X));

            then ((V1 | X) . b) = (((( NEx_Val (v,S,x,xSQ)) +* (x | a)) | X) . b) by A23, FUNCT_4: 13;

            hence thesis by A22, A31, FUNCT_4: 13;

          end;

          hence thesis by A25;

        end;

        ( dom (V2 | X)) = (( dom V1) /\ X) by A2, RELAT_1: 61;

        hence thesis by A18, FUNCT_1: 2, RELAT_1: 61;

      end;

      hence thesis by A4;

    end;

    theorem :: SUBLEMMA:70

    

     Th70: [S, x] is quantifiable implies ((for a holds (J,((v . (( S_Bound ( @ ( CQCSub_All ( [S, x],xSQ)))) | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) iff for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S)

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      assume

       A1: [S, x] is quantifiable;

      thus (for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S

      proof

        set X = ( still_not-bound_in (S `1 ));

        assume

         A2: for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        set V1 = ((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

        set V2 = (v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

        (V1 | X) = (V2 | X) by A1, Th69;

        then

         A3: (J,V1) |= (S `1 ) iff (J,V2) |= (S `1 ) by Th68;

        (J,V1) |= S by A2;

        hence thesis by A3;

      end;

      thus (for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S

      proof

        set X = ( still_not-bound_in (S `1 ));

        assume

         A4: for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        set V1 = ((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

        set V2 = (v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)));

        (V1 | X) = (V2 | X) by A1, Th69;

        then

         A5: (J,V1) |= (S `1 ) iff (J,V2) |= (S `1 ) by Th68;

        (J,V2) |= S by A4;

        hence thesis by A5;

      end;

    end;

    theorem :: SUBLEMMA:71

    

     Th71: ( dom ( NEx_Val (v,S,x,xSQ))) = ( dom ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))

    proof

      ( rng ( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))) c= ( bound_QC-variables Al);

      then ( rng ( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))) c= ( dom v) by Th58;

      then ( dom ( NEx_Val (v,S,x,xSQ))) = ( dom ( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ)))) by RELAT_1: 27;

      hence thesis by SUBSTUT1:def 2;

    end;

    theorem :: SUBLEMMA:72

    

     Th72: (for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) iff for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S

    proof

      thus (for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) implies for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S

      proof

        assume

         A1: for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S;

        let a;

        (v . (( NEx_Val (v,S,x,xSQ)) +* (x | a))) = ((v . ( NEx_Val (v,S,x,xSQ))) . (x | a)) by FUNCT_4: 14;

        hence thesis by A1;

      end;

      thus (for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S) implies for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S

      proof

        assume

         A2: for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S;

        let a;

        (v . (( NEx_Val (v,S,x,xSQ)) +* (x | a))) = ((v . ( NEx_Val (v,S,x,xSQ))) . (x | a)) by FUNCT_4: 14;

        hence thesis by A2;

      end;

    end;

    theorem :: SUBLEMMA:73

    

     Th73: (for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S) iff for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= (S `1 ) by Def2;

    theorem :: SUBLEMMA:74

    

     Th74: for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in ll)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds ((v . vS) *' ll) = ((v . ((vS +* vS1) +* vS2)) *' ll)

    proof

      let v, vS, vS1, vS2 such that

       A1: for y st y in ( dom vS1) holds not y in ( still_not-bound_in ll) and

       A2: for y st y in ( dom vS2) holds (vS2 . y) = (v . y) and

       A3: ( dom vS) misses ( dom vS2);

      set ll2 = ((v . ((vS +* vS1) +* vS2)) *' ll);

      set ll1 = ((v . vS) *' ll);

      

       A4: ( len ll1) = k by VALUAT_1:def 3;

      then

       A5: ( dom ll1) = ( Seg k) by FINSEQ_1:def 3;

      

       A6: ( len ll2) = k by VALUAT_1:def 3;

      for i be Nat st i in ( dom ll1) holds (ll1 . i) = (ll2 . i)

      proof

        let i be Nat such that

         A7: i in ( dom ll1);

        

         A8: i in ( dom ll2) by A6, A5, A7, FINSEQ_1:def 3;

        reconsider i as Nat;

        

         A9: ( dom ll2) c= ( dom ll) by RELAT_1: 25;

         A10:

        now

          reconsider x = (ll . i) as bound_QC-variable of Al by A8, A9, Th5;

          assume

           A11: (ll . i) in ( dom ((vS +* vS1) +* vS2));

           A12:

          now

             A13:

            now

              ( len ll) = k by SUBSTUT1: 34;

              then

               A14: i <= ( len ll) by A5, A7, FINSEQ_1: 1;

              1 <= i by A5, A7, FINSEQ_1: 1;

              then x in { (ll . n) : 1 <= n & n <= ( len ll) & (ll . n) in ( bound_QC-variables Al) } by A14;

              then

               A15: x in ( variables_in (ll,( bound_QC-variables Al))) by QC_LANG3:def 1;

              assume x in ( dom vS1);

              then not x in ( still_not-bound_in ll) by A1;

              hence contradiction by A15, QC_LANG3: 2;

            end;

            assume

             A16: not x in ( dom vS2);

            then

             A17: (((vS +* vS1) +* vS2) . x) = ((vS +* vS1) . x) by FUNCT_4: 11;

            

             A18: x in ( dom (vS +* vS1)) by A11, A16, FUNCT_4: 12;

            now

              assume

               A19: not x in ( dom vS1);

              then (((vS +* vS1) +* vS2) . x) = (vS . x) by A17, FUNCT_4: 11;

              then

               A20: ((v +* ((vS +* vS1) +* vS2)) . x) = (vS . x) by A11, FUNCT_4: 13;

              x in ( dom vS) by A18, A19, FUNCT_4: 12;

              then ((v . ((vS +* vS1) +* vS2)) . x) = ((v +* vS) . x) by A20, FUNCT_4: 13;

              then (ll2 . i) = ((v . vS) . x) by A8, FUNCT_1: 12;

              hence thesis by A7, FUNCT_1: 12;

            end;

            hence thesis by A13;

          end;

          now

            assume

             A21: x in ( dom vS2);

            then (((vS +* vS1) +* vS2) . x) = (vS2 . x) by FUNCT_4: 13;

            then (((vS +* vS1) +* vS2) . x) = (v . x) by A2, A21;

            then ((v +* ((vS +* vS1) +* vS2)) . x) = (v . x) by A11, FUNCT_4: 13;

            then

             A22: (ll2 . i) = (v . x) by A8, FUNCT_1: 12;

             not x in ( dom vS) by A3, A21, XBOOLE_0: 3;

            then ((v +* vS) . x) = (v . x) by FUNCT_4: 11;

            hence thesis by A7, A22, FUNCT_1: 12;

          end;

          hence thesis by A12;

        end;

        now

          assume

           A23: not (ll . i) in ( dom ((vS +* vS1) +* vS2));

          then not (ll . i) in ( dom (vS +* vS1)) by FUNCT_4: 12;

          then not (ll . i) in ( dom vS) by FUNCT_4: 12;

          then ((v +* vS) . (ll . i)) = (v . (ll . i)) by FUNCT_4: 11;

          then

           A24: (ll1 . i) = (v . (ll . i)) by A7, FUNCT_1: 12;

          ((v +* ((vS +* vS1) +* vS2)) . (ll . i)) = (v . (ll . i)) by A23, FUNCT_4: 11;

          hence thesis by A8, A24, FUNCT_1: 12;

        end;

        hence thesis by A10;

      end;

      hence thesis by A4, A6, FINSEQ_2: 9;

    end;

    theorem :: SUBLEMMA:75

    

     Th75: for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in (P ! ll))) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= (P ! ll) iff (J,(v . ((vS +* vS1) +* vS2))) |= (P ! ll)

    proof

      let v, vS, vS1, vS2 such that

       A1: for y st y in ( dom vS1) holds not y in ( still_not-bound_in (P ! ll)) and

       A2: (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2);

      

       A3: for y st y in ( dom vS1) holds not y in ( still_not-bound_in ll)

      proof

        let y;

        assume y in ( dom vS1);

        then not y in ( still_not-bound_in (P ! ll)) by A1;

        hence thesis by QC_LANG3: 5;

      end;

      

       A4: ((v . ((vS +* vS1) +* vS2)) *' ll) in (J . P) iff (( Valid ((P ! ll),J)) . (v . ((vS +* vS1) +* vS2))) = TRUE by VALUAT_1: 7;

      (( Valid ((P ! ll),J)) . (v . vS)) = TRUE iff ((v . vS) *' ll) in (J . P) by VALUAT_1: 7;

      hence thesis by A2, A3, A4, Th74, VALUAT_1:def 7;

    end;

    theorem :: SUBLEMMA:76

    

     Th76: (for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p) implies for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( 'not' p))) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= ( 'not' p) iff (J,(v . ((vS +* vS1) +* vS2))) |= ( 'not' p)

    proof

      assume

       A1: for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p;

      let v, vS, vS1, vS2 such that

       A2: for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( 'not' p)) and

       A3: (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2);

      for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)

      proof

        let y;

        assume y in ( dom vS1);

        then not y in ( still_not-bound_in ( 'not' p)) by A2;

        hence thesis by QC_LANG3: 7;

      end;

      then not (J,(v . vS)) |= p iff not (J,(v . ((vS +* vS1) +* vS2))) |= p by A1, A3;

      hence thesis by VALUAT_1: 17;

    end;

    theorem :: SUBLEMMA:77

    

     Th77: (for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p) & (for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in q)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= q iff (J,(v . ((vS +* vS1) +* vS2))) |= q) implies for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in (p '&' q))) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= (p '&' q) iff (J,(v . ((vS +* vS1) +* vS2))) |= (p '&' q)

    proof

      assume

       A1: (for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p) & for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in q)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= q iff (J,(v . ((vS +* vS1) +* vS2))) |= q;

      let v, vS, vS1, vS2 such that

       A2: for y st y in ( dom vS1) holds not y in ( still_not-bound_in (p '&' q)) and

       A3: (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2);

      

       A4: for y st y in ( dom vS1) holds ( not y in ( still_not-bound_in p)) & not y in ( still_not-bound_in q)

      proof

        let y;

        assume y in ( dom vS1);

        then not y in ( still_not-bound_in (p '&' q)) by A2;

        then not y in (( still_not-bound_in p) \/ ( still_not-bound_in q)) by QC_LANG3: 10;

        hence thesis by XBOOLE_0:def 3;

      end;

      

       A5: (J,(v . ((vS +* vS1) +* vS2))) |= p & (J,(v . ((vS +* vS1) +* vS2))) |= q implies (J,(v . vS)) |= p & (J,(v . vS)) |= q

      proof

        assume

         A6: (J,(v . ((vS +* vS1) +* vS2))) |= p & (J,(v . ((vS +* vS1) +* vS2))) |= q;

        (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & for y st y in ( dom vS1) holds not y in ( still_not-bound_in q) by A4;

        hence thesis by A1, A3, A6;

      end;

      (J,(v . vS)) |= p & (J,(v . vS)) |= q implies (J,(v . ((vS +* vS1) +* vS2))) |= p & (J,(v . ((vS +* vS1) +* vS2))) |= q

      proof

        assume

         A7: (J,(v . vS)) |= p & (J,(v . vS)) |= q;

        (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & for y st y in ( dom vS1) holds not y in ( still_not-bound_in q) by A4;

        hence thesis by A1, A3, A7;

      end;

      hence thesis by A5, VALUAT_1: 18;

    end;

    theorem :: SUBLEMMA:78

    

     Th78: (for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,p)))) implies for y st y in (( dom vS1) \ {x}) holds not y in ( still_not-bound_in p)

    proof

      assume

       A1: for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,p)));

      let y such that

       A2: y in (( dom vS1) \ {x});

      (( dom vS1) \ {x}) c= ( dom vS1) by XBOOLE_1: 36;

      then not y in ( still_not-bound_in ( All (x,p))) by A1, A2;

      then

       A3: not y in (( still_not-bound_in p) \ {x}) by QC_LANG3: 12;

      

       A4: ( {x} \/ (( still_not-bound_in p) \ {x})) = ( {x} \/ ( still_not-bound_in p)) by XBOOLE_1: 39;

       not y in {x} by A2, XBOOLE_0:def 5;

      then not y in ( {x} \/ (( still_not-bound_in p) \ {x})) by A3, XBOOLE_0:def 3;

      hence thesis by A4, XBOOLE_0:def 3;

    end;

    theorem :: SUBLEMMA:79

    

     Th79: for vS1 be Function holds (for y st y in ( dom vS1) holds (vS1 . y) = (v . y)) & ( dom vS) misses ( dom vS1) implies for y st y in (( dom vS1) \ {x}) holds ((vS1 | (( dom vS1) \ {x})) . y) = ((v . vS) . y)

    proof

      let vS1 be Function;

      assume that

       A1: for y st y in ( dom vS1) holds (vS1 . y) = (v . y) and

       A2: ( dom vS) misses ( dom vS1);

      let y such that

       A3: y in (( dom vS1) \ {x});

      y in (( dom vS1) /\ (( dom vS1) \ {x})) by A3, XBOOLE_0:def 4;

      then ((vS1 | (( dom vS1) \ {x})) . y) = (vS1 . y) by FUNCT_1: 48;

      then

       A4: ((vS1 | (( dom vS1) \ {x})) . y) = (v . y) by A1, A3;

       not y in ( dom vS) by A2, A3, XBOOLE_0: 3;

      hence thesis by A4, FUNCT_4: 11;

    end;

    theorem :: SUBLEMMA:80

    

     Th80: (for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p) implies for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,p)))) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= ( All (x,p)) iff (J,(v . ((vS +* vS1) +* vS2))) |= ( All (x,p))

    proof

      assume

       A1: for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p;

      let v, vS, vS1, vS2 such that

       A2: for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,p))) and

       A3: (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2);

      set vS19 = (vS1 | (( dom vS1) \ {x}));

      set vS29 = (vS2 | (( dom vS2) \ {x}));

      

       A4: for y st y in ( dom vS29) holds (vS29 . y) = ((v . vS) . y) by A3, Th79;

      

       A5: ( dom vS29) misses {x} by XBOOLE_1: 63, XBOOLE_1: 79;

      

       A6: for y st y in ( dom vS19) holds not y in ( still_not-bound_in p) by A2, Th78;

      

       A7: (for a holds (J,((v . vS) . (x | a))) |= p) implies for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p

      proof

        assume

         A8: for a holds (J,((v . vS) . (x | a))) |= p;

        let a;

        ( dom vS29) misses ( dom (x | a)) by A5;

        then (J,((v . vS) . (x | a))) |= p iff (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p by A1, A6, A4;

        hence thesis by A8;

      end;

      

       A9: ( dom vS19) misses {x} by XBOOLE_1: 63, XBOOLE_1: 79;

      

       A10: for a holds ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v . ((vS +* vS1) +* vS2)) . (x | a))

      proof

        let a;

        ( dom vS19) misses ( dom (x | a)) by A9;

        then ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS19 +* (x | a)) +* vS29)) by FUNCT_4: 35;

        then

         A11: ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* (vS19 +* ((x | a) +* vS29))) by FUNCT_4: 14;

        ( dom vS29) misses ( dom (x | a)) by A5;

        then ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* (vS19 +* (vS29 +* (x | a)))) by A11, FUNCT_4: 35;

        then

         A12: ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS19 +* vS29) +* (x | a))) by FUNCT_4: 14;

         A13:

        now

          assume x in ( dom vS1);

          then

           A14: (vS19 +* (x .--> (vS1 . x))) = vS1 by Th2;

           A15:

          now

            assume not x in ( dom vS2);

            then vS29 = (vS2 | ( dom vS2)) by ZFMISC_1: 57;

            then vS29 = vS2;

            then

             A16: (vS29 +* {} ) = vS2;

            ( dom {} ) c= ( dom (x | a)) & ( dom (x .--> (vS1 . x))) = ( dom (x | a));

            hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A12, A14, A16, Th1;

          end;

          now

            

             A17: ( dom (x .--> (vS2 . x))) = ( dom (x | a));

            

             A18: ( dom (x .--> (vS1 . x))) = ( dom (x | a));

            assume x in ( dom vS2);

            then (vS29 +* (x .--> (vS2 . x))) = vS2 by Th2;

            hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A12, A14, A18, A17, Th1;

          end;

          hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A15;

        end;

        now

          

           A19: ( dom {} ) c= ( dom (x | a));

          assume not x in ( dom vS1);

          then vS19 = (vS1 | ( dom vS1)) by ZFMISC_1: 57;

          then

           A20: vS19 = vS1;

          then

           A21: (vS19 +* {} ) = vS1;

           A22:

          now

            

             A23: ( dom (x .--> (vS2 . x))) = ( dom (x | a));

            assume x in ( dom vS2);

            then (vS29 +* (x .--> (vS2 . x))) = vS2 by Th2;

            hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A12, A21, A19, A23, Th1;

          end;

          now

            assume not x in ( dom vS2);

            then vS29 = (vS2 | ( dom vS2)) by ZFMISC_1: 57;

            hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A12, A20;

          end;

          hence ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v +* vS) +* ((vS1 +* vS2) +* (x | a))) by A22;

        end;

        then ((v . vS) . (((x | a) +* vS19) +* vS29)) = (((v +* vS) +* (vS1 +* vS2)) +* (x | a)) by A13, FUNCT_4: 14;

        then ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((((v +* vS) +* vS1) +* vS2) +* (x | a)) by FUNCT_4: 14;

        then ((v . vS) . (((x | a) +* vS19) +* vS29)) = (((v +* (vS +* vS1)) +* vS2) +* (x | a)) by FUNCT_4: 14;

        hence thesis by FUNCT_4: 14;

      end;

      

       A24: (for a holds (J,((v . ((vS +* vS1) +* vS2)) . (x | a))) |= p) implies for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p

      proof

        assume

         A25: for a holds (J,((v . ((vS +* vS1) +* vS2)) . (x | a))) |= p;

        let a;

        ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v . ((vS +* vS1) +* vS2)) . (x | a)) by A10;

        hence thesis by A25;

      end;

      

       A26: (for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p) implies for a holds (J,((v . vS) . (x | a))) |= p

      proof

        assume

         A27: for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p;

        let a;

        ( dom vS29) misses ( dom (x | a)) by A5;

        then (J,((v . vS) . (x | a))) |= p iff (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p by A1, A6, A4;

        hence thesis by A27;

      end;

      (for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p) implies for a holds (J,((v . ((vS +* vS1) +* vS2)) . (x | a))) |= p

      proof

        assume

         A28: for a holds (J,((v . vS) . (((x | a) +* vS19) +* vS29))) |= p;

        let a;

        ((v . vS) . (((x | a) +* vS19) +* vS29)) = ((v . ((vS +* vS1) +* vS2)) . (x | a)) by A10;

        hence thesis by A28;

      end;

      hence thesis by A7, A26, A24, Th50;

    end;

    theorem :: SUBLEMMA:81

    

     Th81: for p holds for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in p)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= p iff (J,(v . ((vS +* vS1) +* vS2))) |= p

    proof

      defpred P[ Element of ( CQC-WFF Al)] means for v, vS, vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in $1)) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom vS) misses ( dom vS2) holds (J,(v . vS)) |= $1 iff (J,(v . ((vS +* vS1) +* vS2))) |= $1;

      

       A1: for p, q, x, k holds for l be CQC-variable_list of k, Al holds for P be QC-pred_symbol of k, Al holds P[( VERUM Al)] & P[(P ! l)] & ( P[p] implies P[( 'not' p)]) & ( P[p] & P[q] implies P[(p '&' q)]) & ( P[p] implies P[( All (x,p))]) by Th75, Th76, Th77, Th80, VALUAT_1: 32;

      thus for p holds P[p] from CQC_LANG:sch 1( A1);

    end;

    definition

      let Al, p;

      :: SUBLEMMA:def9

      func RSub1 (p) -> set means

      : Def9: b in it iff ex x st x = b & not x in ( still_not-bound_in p);

      existence

      proof

        defpred P[ object] means ex x st x = $1 & not x in ( still_not-bound_in p);

        consider X be set such that

         A1: for b be object holds b in X iff b in ( bound_QC-variables Al) & P[b] from XBOOLE_0:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be set;

        assume that

         A2: for b holds b in X1 iff ex x st x = b & not x in ( still_not-bound_in p) and

         A3: for b holds b in X2 iff ex x st x = b & not x in ( still_not-bound_in p);

        now

          let b be object;

          b in X1 iff ex x st x = b & not x in ( still_not-bound_in p) by A2;

          hence b in X1 iff b in X2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let Al, p, Sub;

      :: SUBLEMMA:def10

      func RSub2 (p,Sub) -> set means

      : Def10: b in it iff ex x st x = b & x in ( still_not-bound_in p) & x = (( @ Sub) . x);

      existence

      proof

        defpred P[ object] means ex x st x = $1 & x in ( still_not-bound_in p) & x = (( @ Sub) . x);

        consider X be set such that

         A1: for b be object holds b in X iff b in ( bound_QC-variables Al) & P[b] from XBOOLE_0:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be set;

        assume that

         A2: for b holds b in X1 iff ex x st x = b & x in ( still_not-bound_in p) & x = (( @ Sub) . x) and

         A3: for b holds b in X2 iff ex x st x = b & x in ( still_not-bound_in p) & x = (( @ Sub) . x);

        now

          let b be object;

          b in X1 iff ex x st x = b & x in ( still_not-bound_in p) & x = (( @ Sub) . x) by A2;

          hence b in X1 iff b in X2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: SUBLEMMA:82

    

     Th82: ( dom (( @ Sub) | ( RSub1 p))) misses ( dom (( @ Sub) | ( RSub2 (p,Sub))))

    proof

      now

        assume ( dom (( @ Sub) | ( RSub1 p))) meets ( dom (( @ Sub) | ( RSub2 (p,Sub))));

        then

        consider a be object such that

         A1: a in (( dom (( @ Sub) | ( RSub1 p))) /\ ( dom (( @ Sub) | ( RSub2 (p,Sub))))) by XBOOLE_0: 4;

        ( dom (( @ Sub) | ( RSub1 p))) = (( dom ( @ Sub)) /\ ( RSub1 p)) & ( dom (( @ Sub) | ( RSub2 (p,Sub)))) = (( dom ( @ Sub)) /\ ( RSub2 (p,Sub))) by RELAT_1: 61;

        then a in ((( dom ( @ Sub)) /\ (( dom ( @ Sub)) /\ ( RSub1 p))) /\ ( RSub2 (p,Sub))) by A1, XBOOLE_1: 16;

        then a in (((( dom ( @ Sub)) /\ ( dom ( @ Sub))) /\ ( RSub1 p)) /\ ( RSub2 (p,Sub))) by XBOOLE_1: 16;

        then a in (( dom ( @ Sub)) /\ (( RSub1 p) /\ ( RSub2 (p,Sub)))) by XBOOLE_1: 16;

        then

         A2: a in (( RSub1 p) /\ ( RSub2 (p,Sub))) by XBOOLE_0:def 4;

        then a in ( RSub2 (p,Sub)) by XBOOLE_0:def 4;

        then

         A3: ex b be bound_QC-variable of Al st b = a & b in ( still_not-bound_in p) & b = (( @ Sub) . b) by Def10;

        a in ( RSub1 p) by A2, XBOOLE_0:def 4;

        then ex b be bound_QC-variable of Al st b = a & not b in ( still_not-bound_in p) by Def9;

        hence contradiction by A3;

      end;

      hence thesis;

    end;

    theorem :: SUBLEMMA:83

    

     Th83: ( @ ( RestrictSub (x,( All (x,p)),Sub))) = (( @ Sub) \ ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))))

    proof

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

      thus ( @ ( RestrictSub (x,( All (x,p)),Sub))) c= (( @ Sub) \ ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))))

      proof

        let b be object;

        

         A1: ( dom (( @ Sub) | ( RSub1 ( All (x,p))))) misses ( dom (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by Th82;

        assume b in ( @ ( RestrictSub (x,( All (x,p)),Sub)));

        then b in ( RestrictSub (x,( All (x,p)),Sub)) by SUBSTUT1:def 2;

        then b in (Sub | X) by SUBSTUT1:def 6;

        then b in (( @ Sub) | X) by SUBSTUT1:def 2;

        then

         A2: b in (( @ Sub) /\ [:X, ( rng ( @ Sub)):]) by RELAT_1: 67;

        then b in [:X, ( rng ( @ Sub)):] by XBOOLE_0:def 4;

        then

        consider c,d be object such that

         A3: c in X and d in ( rng ( @ Sub)) and

         A4: b = [c, d] by ZFMISC_1:def 2;

        

         A5: ex y1 st y1 = c & y1 in ( still_not-bound_in ( All (x,p))) & y1 is Element of ( dom Sub) & y1 <> x & y1 <> (Sub . y1) by A3;

        now

          assume c in ( RSub2 (( All (x,p)),Sub));

          then ex y st y = c & y in ( still_not-bound_in ( All (x,p))) & y = (( @ Sub) . y) by Def10;

          hence contradiction by A5, SUBSTUT1:def 2;

        end;

        then not b in [:( RSub2 (( All (x,p)),Sub)), ( rng ( @ Sub)):] by A4, ZFMISC_1: 87;

        then not b in (( @ Sub) /\ [:( RSub2 (( All (x,p)),Sub)), ( rng ( @ Sub)):]) by XBOOLE_0:def 4;

        then

         A6: not b in (( @ Sub) | ( RSub2 (( All (x,p)),Sub))) by RELAT_1: 67;

        now

          assume c in ( RSub1 ( All (x,p)));

          then ex y st y = c & not y in ( still_not-bound_in ( All (x,p))) by Def9;

          hence contradiction by A5;

        end;

        then not b in [:( RSub1 ( All (x,p))), ( rng ( @ Sub)):] by A4, ZFMISC_1: 87;

        then not b in (( @ Sub) /\ [:( RSub1 ( All (x,p))), ( rng ( @ Sub)):]) by XBOOLE_0:def 4;

        then not b in (( @ Sub) | ( RSub1 ( All (x,p)))) by RELAT_1: 67;

        then not b in ((( @ Sub) | ( RSub1 ( All (x,p)))) \/ (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by A6, XBOOLE_0:def 3;

        then

         A7: not b in ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by A1, FUNCT_4: 31;

        b in ( @ Sub) by A2, XBOOLE_0:def 4;

        hence thesis by A7, XBOOLE_0:def 5;

      end;

      thus (( @ Sub) \ ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub))))) c= ( @ ( RestrictSub (x,( All (x,p)),Sub)))

      proof

        

         A8: ( dom (( @ Sub) | ( RSub1 ( All (x,p))))) misses ( dom (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by Th82;

        let b be object;

        assume

         A9: b in (( @ Sub) \ ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))));

        then

         A10: b in ( @ Sub) by XBOOLE_0:def 5;

        consider c,d be object such that

         A11: b = [c, d] by A9, RELAT_1:def 1;

        

         A12: c in ( dom ( @ Sub)) by A10, A11, FUNCT_1: 1;

        then

        reconsider z = c as bound_QC-variable of Al;

        

         A13: d = (( @ Sub) . c) by A10, A11, FUNCT_1: 1;

        then

         A14: d in ( rng ( @ Sub)) by A12, FUNCT_1: 3;

         not b in ((( @ Sub) | ( RSub1 ( All (x,p)))) +* (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by A9, XBOOLE_0:def 5;

        then

         A15: not b in ((( @ Sub) | ( RSub1 ( All (x,p)))) \/ (( @ Sub) | ( RSub2 (( All (x,p)),Sub)))) by A8, FUNCT_4: 31;

        then not b in (( @ Sub) | ( RSub1 ( All (x,p)))) by XBOOLE_0:def 3;

        then not b in (( @ Sub) /\ [:( RSub1 ( All (x,p))), ( rng ( @ Sub)):]) by RELAT_1: 67;

        then not [z, d] in [:( RSub1 ( All (x,p))), ( rng ( @ Sub)):] by A10, A11, XBOOLE_0:def 4;

        then

         A16: not z in ( RSub1 ( All (x,p))) by A14, ZFMISC_1: 87;

        then

         A17: z in ( still_not-bound_in ( All (x,p))) by Def9;

        then z in (( still_not-bound_in p) \ {x}) by QC_LANG3: 12;

        then not z in {x} by XBOOLE_0:def 5;

        then

         A18: z <> x by TARSKI:def 1;

        

         A19: d in ( rng ( @ Sub)) by A12, A13, FUNCT_1: 3;

         not b in (( @ Sub) | ( RSub2 (( All (x,p)),Sub))) by A15, XBOOLE_0:def 3;

        then not b in (( @ Sub) /\ [:( RSub2 (( All (x,p)),Sub)), ( rng ( @ Sub)):]) by RELAT_1: 67;

        then not [z, d] in [:( RSub2 (( All (x,p)),Sub)), ( rng ( @ Sub)):] by A10, A11, XBOOLE_0:def 4;

        then not z in ( RSub2 (( All (x,p)),Sub)) by A19, ZFMISC_1: 87;

        then not z in ( still_not-bound_in ( All (x,p))) or z <> (( @ Sub) . z) by Def10;

        then

         A20: z <> (Sub . z) by A16, Def9, SUBSTUT1:def 2;

        

         A21: d in ( rng ( @ Sub)) by A12, A13, FUNCT_1: 3;

        z is Element of ( dom Sub) by A12, SUBSTUT1:def 2;

        then z in X by A17, A18, A20;

        then [z, d] in [:X, ( rng ( @ Sub)):] by A21, ZFMISC_1: 87;

        then b in (( @ Sub) /\ [:X, ( rng ( @ Sub)):]) by A10, A11, XBOOLE_0:def 4;

        then b in (( @ Sub) | X) by RELAT_1: 67;

        then b in (Sub | X) by SUBSTUT1:def 2;

        then b in ( RestrictSub (x,( All (x,p)),Sub)) by SUBSTUT1:def 6;

        hence thesis by SUBSTUT1:def 2;

      end;

    end;

    theorem :: SUBLEMMA:84

    

     Th84: ( dom ( @ ( RestrictSub (x,p,Sub)))) misses (( dom (( @ Sub) | ( RSub1 p))) \/ ( dom (( @ Sub) | ( RSub2 (p,Sub)))))

    proof

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

      

       A1: ( dom (( @ Sub) | ( RSub2 (p,Sub)))) = (( dom ( @ Sub)) /\ ( RSub2 (p,Sub))) by RELAT_1: 61;

      ( RestrictSub (x,p,Sub)) = (Sub | X) by SUBSTUT1:def 6;

      then ( RestrictSub (x,p,Sub)) = (( @ Sub) | X) by SUBSTUT1:def 2;

      then ( dom ( @ ( RestrictSub (x,p,Sub)))) = ( dom (( @ Sub) | X)) by SUBSTUT1:def 2;

      then

       A2: ( dom ( @ ( RestrictSub (x,p,Sub)))) = (( dom ( @ Sub)) /\ X) by RELAT_1: 61;

      

       A3: ( dom (( @ Sub) | ( RSub1 p))) = (( dom ( @ Sub)) /\ ( RSub1 p)) by RELAT_1: 61;

      now

        assume ( dom ( @ ( RestrictSub (x,p,Sub)))) meets (( dom (( @ Sub) | ( RSub1 p))) \/ ( dom (( @ Sub) | ( RSub2 (p,Sub)))));

        then

        consider b be object such that

         A4: b in ( dom ( @ ( RestrictSub (x,p,Sub)))) and

         A5: b in (( dom (( @ Sub) | ( RSub1 p))) \/ ( dom (( @ Sub) | ( RSub2 (p,Sub))))) by XBOOLE_0: 3;

        b in X by A2, A4, XBOOLE_0:def 4;

        then

         A6: ex y st b = y & y in ( still_not-bound_in p) & y is Element of ( dom Sub) & y <> x & y <> (Sub . y);

         A7:

        now

          assume b in ( dom (( @ Sub) | ( RSub2 (p,Sub))));

          then b in ( RSub2 (p,Sub)) by A1, XBOOLE_0:def 4;

          then ex y1 st y1 = b & y1 in ( still_not-bound_in p) & y1 = (( @ Sub) . y1) by Def10;

          hence contradiction by A6, SUBSTUT1:def 2;

        end;

        now

          assume b in ( dom (( @ Sub) | ( RSub1 p)));

          then b in ( RSub1 p) by A3, XBOOLE_0:def 4;

          then ex y1 st y1 = b & not y1 in ( still_not-bound_in p) by Def9;

          hence contradiction by A6;

        end;

        hence contradiction by A5, A7, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: SUBLEMMA:85

    

     Th85: [S, x] is quantifiable implies ( @ (( CQCSub_All ( [S, x],xSQ)) `2 )) = ((( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) +* (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      

       A1: (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))) c= ( @ xSQ) by RELAT_1: 59;

      ( dom (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) misses ( dom (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) by Th82;

      then

       A2: ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) = ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) \/ (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) by FUNCT_4: 31;

      assume

       A3: [S, x] is quantifiable;

      then S1 = ( Sub_All ( [S, x],xSQ)) by Def5;

      then

       A4: ( @ (S1 `2 )) = ( @ xSQ) by A3, Th26;

      

       A5: ( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) = (( @ xSQ) \ ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))) by Th83;

      then

      reconsider F = (( @ xSQ) \ ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))) as PartFunc of ( bound_QC-variables Al), ( bound_QC-variables Al);

      ( dom F) misses (( dom (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) \/ ( dom (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))) by A5, Th84;

      then

       A6: ( dom F) misses ( dom ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))) by FUNCT_4:def 1;

      (((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) \/ F) = (((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) \/ ( @ xSQ)) & (( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) c= ( @ xSQ) by RELAT_1: 59, XBOOLE_1: 39;

      then (((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) \/ F) = ( @ xSQ) by A2, A1, XBOOLE_1: 8, XBOOLE_1: 12;

      then (F +* ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))))) = ( @ xSQ) by A6, FUNCT_4: 31;

      hence thesis by A4, A5, FUNCT_4: 14;

    end;

    theorem :: SUBLEMMA:86

    

     Th86: [S, x] is quantifiable implies ex vS1, vS2 st (for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,(S `1 ))))) & (for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom ( NEx_Val (v,S,x,xSQ))) misses ( dom vS2) & (v . ( Val_S (v,( CQCSub_All ( [S, x],xSQ))))) = (v . ((( NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume [S, x] is quantifiable;

      then

       A1: ( Val_S (v,S1)) = (((( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) +* (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) +* (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) * v) by Th85;

      take vS1 = ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) * v);

      take vS2 = ((( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))) * v);

      ( rng (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) c= ( bound_QC-variables Al);

      then

       A2: ( rng (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) c= ( dom v) by Th58;

      thus for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,(S `1 ))))

      proof

        let y;

        assume y in ( dom vS1);

        then y in ( dom (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) by A2, RELAT_1: 27;

        then y in (( dom ( @ xSQ)) /\ ( RSub1 ( All (x,(S `1 ))))) by RELAT_1: 61;

        then y in ( RSub1 ( All (x,(S `1 )))) by XBOOLE_0:def 4;

        then ex y1 st y1 = y & not y1 in ( still_not-bound_in ( All (x,(S `1 )))) by Def9;

        hence thesis;

      end;

      ( rng (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) c= ( bound_QC-variables Al);

      then

       A3: ( rng (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) c= ( dom v) by Th58;

      thus for y st y in ( dom vS2) holds (vS2 . y) = (v . y)

      proof

        let y;

        assume y in ( dom vS2);

        then

         A4: y in ( dom (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) by A3, RELAT_1: 27;

        then y in (( dom ( @ xSQ)) /\ ( RSub2 (( All (x,(S `1 ))),xSQ))) by RELAT_1: 61;

        then y in ( RSub2 (( All (x,(S `1 ))),xSQ)) by XBOOLE_0:def 4;

        then ex y1 st y1 = y & y1 in ( still_not-bound_in ( All (x,(S `1 )))) & y1 = (( @ xSQ) . y1) by Def10;

        then (v . y) = (v . ((( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ))) . y)) by A4, FUNCT_1: 47;

        hence thesis by A4, FUNCT_1: 13;

      end;

      thus ( dom ( NEx_Val (v,S,x,xSQ))) misses ( dom vS2)

      proof

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

        ( RestrictSub (x,( All (x,(S `1 ))),xSQ)) = (xSQ | X) by SUBSTUT1:def 6;

        then ( RestrictSub (x,( All (x,(S `1 ))),xSQ)) = (( @ xSQ) | X) by SUBSTUT1:def 2;

        then ( dom ( NEx_Val (v,S,x,xSQ))) = ( dom (( @ xSQ) | X)) by Th71;

        then

         A5: ( dom ( NEx_Val (v,S,x,xSQ))) = (( dom ( @ xSQ)) /\ X) by RELAT_1: 61;

        ( dom vS2) = ( dom (( @ xSQ) | ( RSub2 (( All (x,(S `1 ))),xSQ)))) by A3, RELAT_1: 27;

        then

         A6: ( dom vS2) = (( dom ( @ xSQ)) /\ ( RSub2 (( All (x,(S `1 ))),xSQ))) by RELAT_1: 61;

        now

          assume ( dom ( NEx_Val (v,S,x,xSQ))) meets ( dom vS2);

          then

          consider b be object such that

           A7: b in ( dom ( NEx_Val (v,S,x,xSQ))) and

           A8: b in ( dom vS2) by XBOOLE_0: 3;

          b in X by A5, A7, XBOOLE_0:def 4;

          then

           A9: ex y st y = b & y in ( still_not-bound_in ( All (x,(S `1 )))) & y is Element of ( dom xSQ) & y <> x & y <> (xSQ . y);

          b in ( RSub2 (( All (x,(S `1 ))),xSQ)) by A6, A8, XBOOLE_0:def 4;

          then ex y1 st y1 = b & y1 in ( still_not-bound_in ( All (x,(S `1 )))) & y1 = (( @ xSQ) . y1) by Def10;

          hence contradiction by A9, SUBSTUT1:def 2;

        end;

        hence thesis;

      end;

      ((( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) +* (( @ xSQ) | ( RSub1 ( All (x,(S `1 )))))) * v) = ((( @ ( RestrictSub (x,( All (x,(S `1 ))),xSQ))) * v) +* ((( @ xSQ) | ( RSub1 ( All (x,(S `1 ))))) * v)) by A2, FUNCT_7: 9;

      hence thesis by A1, A3, FUNCT_7: 9;

    end;

    theorem :: SUBLEMMA:87

    

     Th87: [S, x] is quantifiable implies for v holds ((J,(v . ( NEx_Val (v,S,x,xSQ)))) |= ( All (x,(S `1 ))) iff (J,(v . ( Val_S (v,( CQCSub_All ( [S, x],xSQ)))))) |= ( CQCSub_All ( [S, x],xSQ)))

    proof

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      assume

       A1: [S, x] is quantifiable;

      then S1 = ( Sub_All ( [S, x],xSQ)) by Def5;

      then (S1 `1 ) = ( All (( [S, x] `2 ),(( [S, x] `1 ) `1 ))) by A1, Th26;

      then (S1 `1 ) = ( All (x,(( [S, x] `1 ) `1 )));

      then

       A2: (S1 `1 ) = ( All (x,(S `1 )));

      let v;

      consider vS1, vS2 such that

       A3: ((for y st y in ( dom vS1) holds not y in ( still_not-bound_in ( All (x,(S `1 ))))) & for y st y in ( dom vS2) holds (vS2 . y) = (v . y)) & ( dom ( NEx_Val (v,S,x,xSQ))) misses ( dom vS2) and

       A4: (v . ( Val_S (v,S1))) = (v . ((( NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2)) by A1, Th86;

      (J,(v . ( NEx_Val (v,S,x,xSQ)))) |= ( All (x,(S `1 ))) iff (J,(v . ((( NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2))) |= ( All (x,(S `1 ))) by A3, Th81;

      hence thesis by A4, A2;

    end;

    theorem :: SUBLEMMA:88

    

     Th88: [S, x] is quantifiable & (for v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S)) implies for v holds ((J,v) |= ( CQC_Sub ( CQCSub_All ( [S, x],xSQ))) iff (J,(v . ( Val_S (v,( CQCSub_All ( [S, x],xSQ)))))) |= ( CQCSub_All ( [S, x],xSQ)))

    proof

      assume that

       A1: [S, x] is quantifiable and

       A2: for v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S);

      let v;

      set S1 = ( CQCSub_All ( [S, x],xSQ));

      set z = ( S_Bound ( @ S1));

      

       A3: (for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S) iff for a holds (J,((v . (z | a)) . (( NEx_Val ((v . (z | a)),S,x,xSQ)) +* (x | a)))) |= S by A1, Th54;

      set q = ( CQC_Sub S);

      

       A4: (J,v) |= ( All (z,q)) iff for a holds (J,(v . (z | a))) |= q by Th50;

      

       A5: (for a holds (J,(v . (z | a))) |= q) implies for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S by A2;

      

       A6: (for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S) implies for a holds (J,(v . (z | a))) |= q

      proof

        assume

         A7: for a holds (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S;

        let a;

        (J,((v . (z | a)) . ( Val_S ((v . (z | a)),S)))) |= S by A7;

        hence thesis by A2;

      end;

      set p = ( CQC_Sub ( CQCSub_the_scope_of S1));

      

       A8: (J,v) |= ( CQCQuant (S1,p)) iff (J,v) |= ( CQCQuant (S1,( CQC_Sub S))) by A1, Th30;

      

       A9: (for a holds (J,((v . (z | a)) . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S) iff for a holds (J,(v . (( NEx_Val (v,S,x,xSQ)) +* (x | a)))) |= S by A1, Th70;

      

       A10: (J,(v . ( NEx_Val (v,S,x,xSQ)))) |= ( All (x,(S `1 ))) implies for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S by Th50;

      

       A11: (for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S) implies (J,(v . ( NEx_Val (v,S,x,xSQ)))) |= ( All (x,(S `1 )))

      proof

        assume for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= S;

        then for a holds (J,((v . ( NEx_Val (v,S,x,xSQ))) . (x | a))) |= (S `1 ) by Th73;

        hence thesis by Th50;

      end;

      S1 is Sub_universal by A1, Th27;

      hence thesis by A1, A8, A4, A5, A6, A3, A9, A11, A10, Th28, Th31, Th56, Th72, Th87;

    end;

    scheme :: SUBLEMMA:sch1

    SubCQCInd1 { 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[( CQCSub_& (S,S9))]) & ( [S, x] is quantifiable & Pro[S] implies Pro[( CQCSub_All ( [S, x],SQ))]);

      

       A2: for S,S9 be Element of ( CQC-Sub-WFF Al()), x be bound_QC-variable of Al(), xSQ be second_Q_comp of [S, x] holds [S, x] is quantifiable & Pro[S] implies Pro[( Sub_All ( [S, x],xSQ))]

      proof

        let S,S9 be Element of ( CQC-Sub-WFF Al());

        let x be bound_QC-variable of Al();

        let xSQ be second_Q_comp of [S, x];

        assume that

         A3: [S, x] is quantifiable and

         A4: Pro[S];

        Pro[( CQCSub_All ( [S, x],xSQ))] by A1, A3, A4;

        hence thesis by A3, Def5;

      end;

      for S,S9 be Element of ( CQC-Sub-WFF Al()) holds (S `2 ) = (S9 `2 ) & Pro[S] & Pro[S9] implies Pro[( Sub_& (S,S9))]

      proof

        let S,S9 be Element of ( CQC-Sub-WFF Al());

        assume that

         A5: (S `2 ) = (S9 `2 ) and

         A6: Pro[S] & Pro[S9];

        ( CQCSub_& (S,S9)) = ( Sub_& (S,S9)) by A5, Def3;

        hence thesis by A1, A5, A6;

      end;

      then

       A7: 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))]) by A1, A2;

      thus thesis from SUBSTUT1:sch 5( A7);

    end;

    theorem :: SUBLEMMA:89

    for S, v holds ((J,v) |= ( CQC_Sub S) iff (J,(v . ( Val_S (v,S)))) |= S)

    proof

      defpred Pro[ Element of ( CQC-Sub-WFF Al)] means for v holds ((J,v) |= ( CQC_Sub $1) iff (J,(v . ( Val_S (v,$1)))) |= $1);

      

       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[( CQCSub_& (S,S9))]) & ( [S, x] is quantifiable & Pro[S] implies Pro[( CQCSub_All ( [S, x],SQ))]) by Th4, Th15, Th19, Th25, Th88;

      thus for S holds Pro[S] from SubCQCInd1( A1);

    end;