:: SUBSTUT1 semantic presentation

begin


definition
let A be QC-alphabet ;
func vSUB A ->  set  equals :: SUBSTUT1:def 1
 PFuncs ((bound_QC-variables A),(bound_QC-variables A));
coherence
 PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is set ;
end;

:: deftheorem  defines vSUB SUBSTUT1:def_1_:_
 for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A));

registration
let A be QC-alphabet ;
cluster vSUB A ->  non empty ;
coherence
 not vSUB A is empty ;
end;

definition
let A be QC-alphabet ;
mode CQC_Substitution of A is Element of vSUB A;
end;

registration
let A be QC-alphabet ;
cluster vSUB A ->  functional ;
coherence
 vSUB A is functional ;
end;

definition
let A be QC-alphabet ;
let Sub be CQC_Substitution of A;
func @ Sub ->  PartFunc of (bound_QC-variables A),(bound_QC-variables A) equals :: SUBSTUT1:def 2
Sub;
coherence
 Sub is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by PARTFUN1:47;
end;

:: deftheorem  defines @ SUBSTUT1:def_2_:_
 for A being QC-alphabet
for Sub being CQC_Substitution of A holds @ Sub = Sub;

theorem Th1: :: SUBSTUT1:1
for A being QC-alphabet
for a being set
for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A
proof
let A be QC-alphabet ; ::_thesis: for a being set
for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A
let a be set ; ::_thesis: for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A
let Sub be CQC_Substitution of A; ::_thesis: ( a in dom Sub implies Sub . a in bound_QC-variables A )
assume  a in dom Sub ; ::_thesis: Sub . a in bound_QC-variables A
then  a in dom (@ Sub) ;
hence  Sub . a in bound_QC-variables A by PARTFUN1:4; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let l be FinSequence of QC-variables A;
let Sub be CQC_Substitution of A;
func CQC_Subst (l,Sub) ->  FinSequence of QC-variables A means :Def3: :: SUBSTUT1:def 3
( len it = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies it . k = Sub . (l . k) ) & ( not l . k in dom Sub implies it . k = l . k ) ) ) );
existence
 ex b1 being FinSequence of QC-variables A st
( len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) )
proof
defpred S1[ set , set ] means ( ( l . $1 in dom Sub implies $2 = Sub . (l . $1) ) & ( not l . $1 in dom Sub implies $2 = l . $1 ) );
A1: for k being Nat st k in Seg (len l) holds
ex y being set st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg (len l) implies ex y being set st S1[k,y] )
assume  k in Seg (len l) ; ::_thesis: ex y being set st S1[k,y]
 ( l . k in dom Sub implies ex y being set st S1[k,y] ) ;
hence  ex y being set st S1[k,y] ; ::_thesis: verum
end;
consider s being FinSequence such that
A2: dom s = Seg (len l) and
A3: for k being Nat st k in Seg (len l) holds
S1[k,s . k] from FINSEQ_1:sch_1(A1);
 rng s c= QC-variables A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in QC-variables A )
assume  y in rng s ; ::_thesis: y in QC-variables A
then consider x being set  such that
A4: x in dom s and
A5: s . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A4;
now__::_thesis:_(_(_l_._x_in_dom_Sub_&_s_._x_in_bound_QC-variables_A_)_or_(_not_l_._x_in_dom_Sub_&_s_._x_in_QC-variables_A_)_)
percases ( l . x in dom Sub or not l . x in dom Sub ) ;
caseA6: l . x in dom Sub ; ::_thesis: s . x in bound_QC-variables A
then  s . x = Sub . (l . x) by A2, A3, A4;
hence  s . x in bound_QC-variables A by A6, Th1; ::_thesis: verum
end;
caseA7: not l . x in dom Sub ; ::_thesis: s . x in QC-variables A
 x in dom l by A2, A4, FINSEQ_1:def_3;
then A8: l . x in rng l by FUNCT_1:3;
 s . x = l . x by A2, A3, A4, A7;
hence  s . x in QC-variables A by A8; ::_thesis: verum
end;
end;
end;
hence  y in QC-variables A by A5; ::_thesis: verum
end;
then reconsider s = s as FinSequence of QC-variables A by FINSEQ_1:def_4;
take  s ; ::_thesis: ( len s = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ) )
thus  len s = len l by A2, FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) )
thus  for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ::_thesis: verum
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len l implies ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) )
assume  ( 1 <= k & k <= len l ) ; ::_thesis: ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) )
then  k in dom l by FINSEQ_3:25;
then  k in Seg (len l) by FINSEQ_1:def_3;
hence  ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) by A3; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being FinSequence of QC-variables A st len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) & len b2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b2 . k = l . k ) ) ) holds
b1 = b2
proof
let l1, l2 be FinSequence of QC-variables A; ::_thesis: ( len l1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) ) & len l2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l2 . k = l . k ) ) ) implies l1 = l2 )
assume that
A9: len l1 = len l and
A10: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) and
A11: len l2 = len l and
A12: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l2 . k = l . k ) ) ; ::_thesis: l1 = l2
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_l_holds_
l1_._k_=_l2_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len l implies l1 . k = l2 . k )
assume A13: ( 1 <= k & k <= len l ) ; ::_thesis: l1 . k = l2 . k
A14: k in NAT by ORDINAL1:def_12;
then A15: ( not l . k in dom Sub implies l1 . k = l . k ) by A10, A13;
 ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) by A10, A14, A13;
hence  l1 . k = l2 . k by A12, A14, A13, A15; ::_thesis: verum
end;
hence  l1 = l2 by A9, A11, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def_3_:_
 for A being QC-alphabet
for l being FinSequence of QC-variables A
for Sub being CQC_Substitution of A
for b4 being FinSequence of QC-variables A holds
( b4 = CQC_Subst (l,Sub) iff ( len b4 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b4 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b4 . k = l . k ) ) ) ) );

definition
let A be QC-alphabet ;
let l be FinSequence of bound_QC-variables A;
func @ l ->  FinSequence of QC-variables A equals :: SUBSTUT1:def 4
l;
coherence
 l is FinSequence of QC-variables A
proof
 rng l c= QC-variables A by XBOOLE_1:1;
hence  l is FinSequence of QC-variables A by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines @ SUBSTUT1:def_4_:_
 for A being QC-alphabet
for l being FinSequence of bound_QC-variables A holds @ l = l;

definition
let A be QC-alphabet ;
let l be FinSequence of bound_QC-variables A;
let Sub be CQC_Substitution of A;
func CQC_Subst (l,Sub) ->  FinSequence of bound_QC-variables A equals :: SUBSTUT1:def 5
 CQC_Subst ((@ l),Sub);
coherence
 CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A
proof
 len (CQC_Subst ((@ l),Sub)) = len (@ l) by Def3;
then A1: dom (CQC_Subst ((@ l),Sub)) = Seg (len (@ l)) by FINSEQ_1:def_3;
A2: for k being Element of NAT st k in Seg (len (@ l)) holds
( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) )
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len (@ l)) implies ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) )
assume  k in Seg (len (@ l)) ; ::_thesis: ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) )
then  ( 1 <= k & k <= len (@ l) ) by FINSEQ_1:1;
hence  ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) by Def3; ::_thesis: verum
end;
 rng (CQC_Subst ((@ l),Sub)) c= bound_QC-variables A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (CQC_Subst ((@ l),Sub)) or y in bound_QC-variables A )
assume  y in rng (CQC_Subst ((@ l),Sub)) ; ::_thesis: y in bound_QC-variables A
then consider x being set  such that
A3: x in dom (CQC_Subst ((@ l),Sub)) and
A4: (CQC_Subst ((@ l),Sub)) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
now__::_thesis:_(_(_(@_l)_._x_in_dom_Sub_&_(CQC_Subst_((@_l),Sub))_._x_in_bound_QC-variables_A_)_or_(_not_(@_l)_._x_in_dom_Sub_&_(CQC_Subst_((@_l),Sub))_._x_in_bound_QC-variables_A_)_)
percases ( (@ l) . x in dom Sub or not (@ l) . x in dom Sub ) ;
caseA5: (@ l) . x in dom Sub ; ::_thesis: (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A
then  (CQC_Subst ((@ l),Sub)) . x = Sub . ((@ l) . x) by A1, A2, A3;
hence  (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A by A5, Th1; ::_thesis: verum
end;
caseA6: not (@ l) . x in dom Sub ; ::_thesis: (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A
A7: rng l c= bound_QC-variables A ;
 x in dom (@ l) by A1, A3, FINSEQ_1:def_3;
then A8: (@ l) . x in rng (@ l) by FUNCT_1:3;
 (CQC_Subst ((@ l),Sub)) . x = (@ l) . x by A1, A2, A3, A6;
hence  (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A by A8, A7; ::_thesis: verum
end;
end;
end;
hence  y in bound_QC-variables A by A4; ::_thesis: verum
end;
hence  CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines CQC_Subst SUBSTUT1:def_5_:_
 for A being QC-alphabet
for l being FinSequence of bound_QC-variables A
for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub);

definition
let A be QC-alphabet ;
let Sub be CQC_Substitution of A;
let X be set ;
:: original: |
redefine funcSub | X ->  CQC_Substitution of A;
coherence
 Sub | X is CQC_Substitution of A
proof
 Sub | X = (@ Sub) | X ;
hence  Sub | X is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum
end;
end;

registration
let A be QC-alphabet ;
cluster Relation-like Function-like finite for Element of vSUB A;
existence
 ex b1 being CQC_Substitution of A st b1 is finite
proof
take L = {} ; ::_thesis: ( L is CQC_Substitution of A & L is finite )
 L is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by RELSET_1:12;
hence  L is CQC_Substitution of A by PARTFUN1:45; ::_thesis: L is finite
thus  L is finite ; ::_thesis: verum
end;
end;

definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be QC-formula of A;
let Sub be CQC_Substitution of A;
func RestrictSub (x,p,Sub) ->  finite CQC_Substitution of A equals :: SUBSTUT1:def 6
Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;
coherence
 Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  is finite CQC_Substitution of A
proof
set Y =  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;
set X =  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;
reconsider Z = still_not-bound_in p as finite set by CQC_SIM1:19;
 for a being set holds
( a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  iff a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  )
proof
let a be set ; ::_thesis: ( a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  iff a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  )
thus  ( a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  implies a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  ) ::_thesis: ( a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  implies a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  )
proof
assume  a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ; ::_thesis: a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }
then consider y being bound_QC-variable of A such that
A1: ( a = y & y in still_not-bound_in p ) and
A2: ( y is Element of dom Sub & y <> x & y <> Sub . y ) ;
 y in  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A2;
hence  a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  ( a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  implies a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ) ::_thesis: verum
proof
assume A3: a in Z /\  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  ; ::_thesis: a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }
then  a in  {  y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y )  }  by XBOOLE_0:def_4;
then A4: ex y being bound_QC-variable of A st
( a = y & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
 a in Z by A3, XBOOLE_0:def_4;
hence  a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A4; ::_thesis: verum
end;
end;
then reconsider X =  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  as finite set by TARSKI:1;
 Sub | X is finite ;
hence  Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  is finite CQC_Substitution of A ; ::_thesis: verum
end;
end;

:: deftheorem  defines RestrictSub SUBSTUT1:def_6_:_
 for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for Sub being CQC_Substitution of A holds RestrictSub (x,p,Sub) = Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;

definition
let A be QC-alphabet ;
let l1 be FinSequence of QC-variables A;
func Bound_Vars l1 ->  Subset of (bound_QC-variables A) equals :: SUBSTUT1:def 7
 {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  ;
coherence
  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  is Subset of (bound_QC-variables A)
proof
set A2 =  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  ;
  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  c= bound_QC-variables A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  or x in bound_QC-variables A )
assume  x in  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  ; ::_thesis: x in bound_QC-variables A
then  ex k being Element of NAT st
( l1 . k = x & 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) ;
hence  x in bound_QC-variables A ; ::_thesis: verum
end;
hence   {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  is Subset of (bound_QC-variables A) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Bound_Vars SUBSTUT1:def_7_:_
 for A being QC-alphabet
for l1 being FinSequence of QC-variables A holds Bound_Vars l1 =  {  (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A )  }  ;

definition
let A be QC-alphabet ;
let p be QC-formula of A;
func Bound_Vars p ->  Subset of (bound_QC-variables A) means :Def8: :: SUBSTUT1:def 8
 ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( it = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) );
correctness
existence
ex b1 being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) );
uniqueness
for b1, b2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b2 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) holds
b1 = b2;
proof
deffunc H1( Element of QC-WFF A) ->  Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of $1);
set V = bound_QC-variables A;
deffunc H2( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H3( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H4( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \/ {(bound_in $1)};
thus  ( ex d being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) & ( for x1, x2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( x1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( x2 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) holds
x1 = x2 ) ) from QC_LANG3:sch_2(); ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def_8_:_
 for A being QC-alphabet
for p being QC-formula of A
for b3 being Subset of (bound_QC-variables A) holds
( b3 = Bound_Vars p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b3 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) );

Lm1:  for A being QC-alphabet
for p being QC-formula of A holds
( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof
let A be QC-alphabet ; ::_thesis: for p being QC-formula of A holds
( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
let p be QC-formula of A; ::_thesis: ( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
deffunc H1( Element of QC-WFF A) ->  Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of $1);
deffunc H2( Element of QC-WFF A) ->  Subset of (bound_QC-variables A) = Bound_Vars $1;
set V = bound_QC-variables A;
deffunc H3( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H4( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H5( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \/ {(bound_in $1)};
A1: for p being QC-formula of A
for X being Subset of (bound_QC-variables A) holds
( X = H2(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( X = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H4(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H5(p,d1) ) ) ) ) ) by Def8;
H2( VERUM A) = {} (bound_QC-variables A) from QC_LANG3:sch_3(A1)
.= {} ;
hence  Bound_Vars (VERUM A) = {} (bound_QC-variables A) ; ::_thesis: ( ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
thus  ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) ::_thesis: ( ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof
assume A2: p is atomic ; ::_thesis: Bound_Vars p = Bound_Vars (the_arguments_of p)
thus  H2(p) = H1(p) from QC_LANG3:sch_4(A1, A2); ::_thesis: verum
end;
thus  ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) ::_thesis: ( ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof
assume A3: p is negative ; ::_thesis: Bound_Vars p = Bound_Vars (the_argument_of p)
thus  H2(p) = H3(H2( the_argument_of p)) from QC_LANG3:sch_5(A1, A3); ::_thesis: verum
end;
thus  ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) ::_thesis: ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} )
proof
assume A4: p is conjunctive ; ::_thesis: Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p))
 for d1, d2 being Subset of (bound_QC-variables A) st d1 = H2( the_left_argument_of p) & d2 = H2( the_right_argument_of p) holds
H2(p) = H4(d1,d2) from QC_LANG3:sch_6(A1, A4);
hence  Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ; ::_thesis: verum
end;
thus  ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ::_thesis: verum
proof
assume A5: p is universal ; ::_thesis: Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)}
thus  H2(p) = H5(p,H2( the_scope_of p)) from QC_LANG3:sch_7(A1, A5); ::_thesis: verum
end;
end;

theorem Th2: :: SUBSTUT1:2
for A being QC-alphabet holds Bound_Vars (VERUM A) = {}
proof
let A be QC-alphabet ; ::_thesis: Bound_Vars (VERUM A) = {}
 Bound_Vars (VERUM A) = {} (bound_QC-variables A) by Lm1;
hence  Bound_Vars (VERUM A) = {} ; ::_thesis: verum
end;

theorem :: SUBSTUT1:3
for A being QC-alphabet
for p being QC-formula of A st p is atomic holds
Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;

theorem :: SUBSTUT1:4
for A being QC-alphabet
for p being QC-formula of A st p is negative holds
Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1;

theorem :: SUBSTUT1:5
for A being QC-alphabet
for p being QC-formula of A st p is conjunctive holds
Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by Lm1;

theorem :: SUBSTUT1:6
for A being QC-alphabet
for p being QC-formula of A st p is universal holds
Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;

registration
let A be QC-alphabet ;
let p be QC-formula of A;
cluster Bound_Vars p ->  finite ;
coherence
 Bound_Vars p is finite
proof
defpred S1[ Element of QC-WFF A] means  Bound_Vars A is finite ;
A1: for p being Element of QC-WFF A holds
( ( p is atomic implies S1[p] ) & S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) )
proof
let p be Element of QC-WFF A; ::_thesis: ( ( p is atomic implies S1[p] ) & S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) )
thus  ( p is atomic implies Bound_Vars p is finite ) ::_thesis: ( S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) )
proof
deffunc H1( set ) ->  set = (the_arguments_of p) . A;
defpred S2[ Element of NAT ] means ( 1 <= A & A <= len (the_arguments_of p) );
defpred S3[ Element of NAT ] means ( 1 <= A & A <= len (the_arguments_of p) & (the_arguments_of p) . A in bound_QC-variables A );
A2: for k being Element of NAT st S3[k] holds
S2[k] ;
A3:  {  H1(k) where k is Element of NAT : S3[k]  }  c=  {  H1(n) where n is Element of NAT : S2[n]  }  from FRAENKEL:sch_1(A2);
assume  p is atomic ; ::_thesis: Bound_Vars p is finite
then  Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1
.=  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A )  }  ;
then  Bound_Vars p c= rng (the_arguments_of p) by A3, CQC_SIM1:9;
hence  Bound_Vars p is finite ; ::_thesis: verum
end;
thus  Bound_Vars (VERUM A) is finite by Th2; ::_thesis: ( ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) )
thus  ( p is negative & Bound_Vars (the_argument_of p) is finite implies Bound_Vars p is finite ) by Lm1; ::_thesis: ( ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) )
thus  ( p is conjunctive & Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite implies Bound_Vars p is finite ) ::_thesis: ( p is universal & S1[ the_scope_of p] implies S1[p] )
proof
assume that
A4: p is conjunctive and
A5: ( Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite ) ; ::_thesis: Bound_Vars p is finite
 Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by A4, Lm1;
hence  Bound_Vars p is finite by A5; ::_thesis: verum
end;
assume that
A6: p is universal and
A7: Bound_Vars (the_scope_of p) is finite ; ::_thesis: S1[p]
 Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by A6, Lm1;
hence  S1[p] by A7; ::_thesis: verum
end;
 for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch_2(A1);
hence  Bound_Vars p is finite ; ::_thesis: verum
end;
end;

definition
let A be QC-alphabet ;
let p be QC-formula of A;
func Dom_Bound_Vars p ->  finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 9
 {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ;
coherence
  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  is finite Subset of (QC-symbols A)
proof
defpred S1[ set , set ] means  ex s being QC-symbol of A st
( s = $1 & $2 = x. s );
set X =  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ;
A1:  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  c= QC-symbols A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  or a in QC-symbols A )
assume  a in  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ; ::_thesis: a in QC-symbols A
then  ex s being QC-symbol of A st
( a = s & x. s in Bound_Vars p ) ;
hence  a in QC-symbols A ; ::_thesis: verum
end;
A2: for a being set st a in QC-symbols A holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in QC-symbols A implies ex b being set st S1[a,b] )
assume  a in QC-symbols A ; ::_thesis: ex b being set st S1[a,b]
then reconsider s = a as QC-symbol of A ;
take  x. s ; ::_thesis: S1[a, x. s]
take  s ; ::_thesis: ( s = a & x. s = x. s )
thus  ( s = a & x. s = x. s ) ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = QC-symbols A & ( for a being set st a in QC-symbols A holds
S1[a,f . a] ) ) from CLASSES1:sch_1(A2);
A4: rng (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) c= Bound_Vars p
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) or b in Bound_Vars p )
assume  b in rng (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) ; ::_thesis: b in Bound_Vars p
then consider a being set  such that
A5: a in dom (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) and
A6: b = (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) . a by FUNCT_1:def_3;
 a in  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  by A5, RELAT_1:57;
then A7: ex s being QC-symbol of A st
( a = s & x. s in Bound_Vars p ) ;
 ( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57;
then  ex s being QC-symbol of A st
( s = a & b = x. s ) by A3;
hence  b in Bound_Vars p by A7; ::_thesis: verum
end;
 f is one-to-one
proof
let a1, a2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 )
assume that
A8: ( a1 in dom f & a2 in dom f ) and
A9: f . a1 = f . a2 ; ::_thesis: a1 = a2
 ( ex s being QC-symbol of A st
( s = a1 & f . a1 = x. s ) & ex t being QC-symbol of A st
( t = a2 & f . a2 = x. t ) ) by A3, A8;
hence  a1 = a2 by A9, XTUPLE_0:1; ::_thesis: verum
end;
then  f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  is one-to-one by FUNCT_1:52;
then A10: dom (f |  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ) is finite by A4, CARD_1:59;
reconsider X =  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  as Subset of (QC-symbols A) by A1;
 for a being set holds
( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57;
then  dom (f | X) = X /\ (QC-symbols A) by A3, XBOOLE_0:def_4;
hence   {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  is finite Subset of (QC-symbols A) by A10, XBOOLE_1:28; ::_thesis: verum
end;
end;

:: deftheorem  defines Dom_Bound_Vars SUBSTUT1:def_9_:_
 for A being QC-alphabet
for p being QC-formula of A holds Dom_Bound_Vars p =  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ;

definition
let A be QC-alphabet ;
let finSub be finite CQC_Substitution of A;
func Sub_Var finSub ->  finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 10
 {  s where s is QC-symbol of A : x. s in rng finSub  }  ;
coherence
  {  s where s is QC-symbol of A : x. s in rng finSub  }  is finite Subset of (QC-symbols A)
proof
defpred S1[ set , set ] means  ex s being QC-symbol of A st
( s = $1 & $2 = x. s );
set X =  {  s where s is QC-symbol of A : x. s in rng finSub  }  ;
A1:  {  s where s is QC-symbol of A : x. s in rng finSub  }  c= QC-symbols A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  s where s is QC-symbol of A : x. s in rng finSub  }  or a in QC-symbols A )
assume  a in  {  s where s is QC-symbol of A : x. s in rng finSub  }  ; ::_thesis: a in QC-symbols A
then  ex s being QC-symbol of A st
( a = s & x. s in rng finSub ) ;
hence  a in QC-symbols A ; ::_thesis: verum
end;
A2: for a being set st a in QC-symbols A holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in QC-symbols A implies ex b being set st S1[a,b] )
assume  a in QC-symbols A ; ::_thesis: ex b being set st S1[a,b]
then reconsider s = a as QC-symbol of A ;
take  x. s ; ::_thesis: S1[a, x. s]
take  s ; ::_thesis: ( s = a & x. s = x. s )
thus  ( s = a & x. s = x. s ) ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = QC-symbols A & ( for a being set st a in QC-symbols A holds
S1[a,f . a] ) ) from CLASSES1:sch_1(A2);
A4: rng (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) c= rng finSub
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) or b in rng finSub )
assume  b in rng (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) ; ::_thesis: b in rng finSub
then consider a being set  such that
A5: a in dom (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) and
A6: b = (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) . a by FUNCT_1:def_3;
 a in  {  s where s is QC-symbol of A : x. s in rng finSub  }  by A5, RELAT_1:57;
then A7: ex s being QC-symbol of A st
( a = s & x. s in rng finSub ) ;
 ( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57;
then  ex s being QC-symbol of A st
( s = a & b = x. s ) by A3;
hence  b in rng finSub by A7; ::_thesis: verum
end;
 f is one-to-one
proof
let a1, a2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 )
assume that
A8: ( a1 in dom f & a2 in dom f ) and
A9: f . a1 = f . a2 ; ::_thesis: a1 = a2
 ( ex s being QC-symbol of A st
( s = a1 & f . a1 = x. s ) & ex t being QC-symbol of A st
( t = a2 & f . a2 = x. t ) ) by A3, A8;
hence  a1 = a2 by A9, XTUPLE_0:1; ::_thesis: verum
end;
then  f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  is one-to-one by FUNCT_1:52;
then A10: dom (f |  {  s where s is QC-symbol of A : x. s in rng finSub  }  ) is finite by A4, CARD_1:59;
reconsider X =  {  s where s is QC-symbol of A : x. s in rng finSub  }  as Subset of (QC-symbols A) by A1;
 for a being set holds
( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57;
then  dom (f | X) = X /\ (QC-symbols A) by A3, XBOOLE_0:def_4;
hence   {  s where s is QC-symbol of A : x. s in rng finSub  }  is finite Subset of (QC-symbols A) by A10, XBOOLE_1:28; ::_thesis: verum
end;
end;

:: deftheorem  defines Sub_Var SUBSTUT1:def_10_:_
 for A being QC-alphabet
for finSub being finite CQC_Substitution of A holds Sub_Var finSub =  {  s where s is QC-symbol of A : x. s in rng finSub  }  ;

Lm2:  for X, Y being set st card X in card Y holds
Y \ X <> {}
proof
let X, Y be set ; ::_thesis: ( card X in card Y implies Y \ X <> {} )
assume that
A1: card X in card Y and
A2: Y \ X = {} ; ::_thesis: contradiction
 Y c= X by A2, XBOOLE_1:37;
then  card Y c= card X by CARD_1:11;
hence  contradiction by A1, CARD_1:4; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let p be QC-formula of A;
let finSub be finite CQC_Substitution of A;
func NSub (p,finSub) ->  non empty Subset of (QC-symbols A) equals :: SUBSTUT1:def 11
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));
coherence
 NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A)
proof
set X = (Dom_Bound_Vars p) \/ (Sub_Var finSub);
 card ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) in card NAT by CARD_3:42;
hence  NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A) by Lm2, QC_LANG1:3, XBOOLE_1:109; ::_thesis: verum
end;
end;

:: deftheorem  defines NSub SUBSTUT1:def_11_:_
 for A being QC-alphabet
for p being QC-formula of A
for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

definition
let A be QC-alphabet ;
let finSub be finite CQC_Substitution of A;
let p be QC-formula of A;
func upVar (finSub,p) ->  QC-symbol of A equals :: SUBSTUT1:def 12
 the Element of NSub (p,finSub);
coherence
 the Element of NSub (p,finSub) is QC-symbol of A ;
end;

:: deftheorem  defines upVar SUBSTUT1:def_12_:_
 for A being QC-alphabet
for finSub being finite CQC_Substitution of A
for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub);

definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be QC-formula of A;
let finSub be finite CQC_Substitution of A;
assume A1: ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) ;
func ExpandSub (x,p,finSub) ->  CQC_Substitution of A equals :: SUBSTUT1:def 13
finSub \/ {[x,(x. (upVar (finSub,p)))]} if x in rng finSub
otherwise finSub \/ {[x,x]};
coherence
 ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) )
proof
A2: now__::_thesis:_(_not_x_in_rng_finSub_implies_finSub_\/_{[x,x]}_is_CQC_Substitution_of_A_)
reconsider Z = {[x,x]} as Relation-like set ;
assume  not x in rng finSub ; ::_thesis: finSub \/ {[x,x]} is CQC_Substitution of A
A3: now__::_thesis:_for_a_being_set_holds_not_a_in_(dom_finSub)_/\_(dom_Z)
consider Sub being CQC_Substitution of A such that
A4: finSub = RestrictSub (x,(All (x,p)),Sub) by A1;
set X =  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;
A5: dom finSub c=  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A4, RELAT_1:58;
given a being set  such that A6: a in (dom finSub) /\ (dom Z) ; ::_thesis: contradiction
 a in dom finSub by A6, XBOOLE_0:def_4;
then  a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A5;
then A7: ( dom Z = {x} & ex y being bound_QC-variable of A st
( a = y & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:9;
 a in dom Z by A6, XBOOLE_0:def_4;
hence  contradiction by A7, TARSKI:def_1; ::_thesis: verum
end;
reconsider Z = Z as Function ;
 for a being set st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A3;
then consider h being Function such that
A8: (@ finSub) \/ Z = h by PARTFUN1:1;
reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ;
 (@ finSub) \/ Z = h by A8;
hence  finSub \/ {[x,x]} is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum
end;
now__::_thesis:_(_x_in_rng_finSub_implies_finSub_\/_{[x,(x._(upVar_(finSub,p)))]}_is_CQC_Substitution_of_A_)
reconsider Z = {[x,(x. (upVar (finSub,p)))]} as Relation-like set ;
assume  x in rng finSub ; ::_thesis: finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A
A9: now__::_thesis:_for_a_being_set_holds_not_a_in_(dom_finSub)_/\_(dom_Z)
consider Sub being CQC_Substitution of A such that
A10: finSub = RestrictSub (x,(All (x,p)),Sub) by A1;
set X =  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  ;
A11: dom finSub c=  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A10, RELAT_1:58;
given a being set  such that A12: a in (dom finSub) /\ (dom Z) ; ::_thesis: contradiction
 a in dom finSub by A12, XBOOLE_0:def_4;
then  a in  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y )  }  by A11;
then A13: ( dom Z = {x} & ex y being bound_QC-variable of A st
( a = y & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:9;
 a in dom Z by A12, XBOOLE_0:def_4;
hence  contradiction by A13, TARSKI:def_1; ::_thesis: verum
end;
reconsider Z = Z as Function ;
 for a being set st a in (dom (@ finSub)) /\ (dom Z) holds
(@ finSub) . a = Z . a by A9;
then consider h being Function such that
A14: (@ finSub) \/ Z = h by PARTFUN1:1;
reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ;
 (@ finSub) \/ Z = h by A14;
hence  finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum
end;
hence  ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) ) by A2; ::_thesis: verum
end;
consistency
 for b1 being CQC_Substitution of A holds verum ;
end;

:: deftheorem  defines ExpandSub SUBSTUT1:def_13_:_
 for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) holds
( ( x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,(x. (upVar (finSub,p)))]} ) & ( not x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,x]} ) );

definition
let A be QC-alphabet ;
let p be QC-formula of A;
let Sub be CQC_Substitution of A;
let b be set ;
predp,Sub PQSub b means :Def14: :: SUBSTUT1:def 14
( ( p is universal implies b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) ) & ( not p is universal implies b = {} ) );
end;

:: deftheorem Def14 defines PQSub SUBSTUT1:def_14_:_
 for A being QC-alphabet
for p being QC-formula of A
for Sub being CQC_Substitution of A
for b being set holds
( p,Sub PQSub b iff ( ( p is universal implies b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) ) & ( not p is universal implies b = {} ) ) );

definition
let A be QC-alphabet ;
func QSub A ->  Function means :: SUBSTUT1:def 15
 for a being set holds
( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) );
existence
 ex b1 being Function st
for a being set holds
( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
proof
defpred S1[ set , set ] means  ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( $1 = [p,Sub] & p,Sub PQSub $2 );
A1: for a, b1, b2 being set st S1[a,b1] & S1[a,b2] holds
b1 = b2
proof
let a, b1, b2 be set ; ::_thesis: ( S1[a,b1] & S1[a,b2] implies b1 = b2 )
assume that
A2: ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b1 ) and
A3: ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b2 ) ; ::_thesis: b1 = b2
consider p1 being QC-formula of A, Sub1 being CQC_Substitution of A such that
A4: a = [p1,Sub1] and
A5: p1,Sub1 PQSub b1 by A2;
consider p2 being QC-formula of A, Sub2 being CQC_Substitution of A such that
A6: a = [p2,Sub2] and
A7: p2,Sub2 PQSub b2 by A3;
A8: p1 = p2 by A4, A6, XTUPLE_0:1;
A9: Sub1 = Sub2 by A4, A6, XTUPLE_0:1;
percases ( p1 is universal or not p1 is universal ) ;
supposeA10: p1 is universal ; ::_thesis: b1 = b2
then  b1 = ExpandSub ((bound_in p1),(the_scope_of p1),(RestrictSub ((bound_in p1),p1,Sub1))) by A5, Def14;
hence  b1 = b2 by A7, A8, A9, A10, Def14; ::_thesis: verum
end;
supposeA11: not p1 is universal ; ::_thesis: b1 = b2
then  b1 = {} by A5, Def14;
hence  b1 = b2 by A7, A8, A11, Def14; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A12: for a, b being set holds
( [a,b] in f iff ( a in [:(QC-WFF A),(vSUB A):] & S1[a,b] ) ) from FUNCT_1:sch_1(A1);
take  f ; ::_thesis: for a being set holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
 for c being set holds
( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) )
proof
let c be set ; ::_thesis: ( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) )
thus  ( c in f implies ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) ) ::_thesis: ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f )
proof
assume A13: c in f ; ::_thesis: ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b )
then consider a, b being set  such that
A14: c = [a,b] by RELAT_1:def_1;
 ex p being QC-formula of A ex Sub being CQC_Substitution of A st
( a = [p,Sub] & p,Sub PQSub b ) by A12, A13, A14;
hence  ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) by A14; ::_thesis: verum
end;
thus  ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f ) by A12; ::_thesis: verum
end;
hence  for a being set holds
( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st ( for a being set holds
( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds
( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds
b1 = b2
proof
let F1, F2 be Function; ::_thesis: ( ( for a being set holds
( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds
( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) implies F1 = F2 )
assume that
A15: for a being set holds
( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) and
A16: for a being set holds
( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_a_being_set_holds_
(_a_in_F1_iff_a_in_F2_)
let a be set ; ::_thesis: ( a in F1 iff a in F2 )
 ( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) by A15;
hence  ( a in F1 iff a in F2 ) by A16; ::_thesis: verum
end;
hence  F1 = F2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem  defines QSub SUBSTUT1:def_15_:_
 for A being QC-alphabet
for b2 being Function holds
( b2 = QSub A iff for a being set holds
( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) );

begin

theorem Th7: :: SUBSTUT1:7
for A being QC-alphabet holds
( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
proof
let A be QC-alphabet ; ::_thesis: ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
 QC-WFF A is A -closed by QC_LANG1:7;
then  QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) by QC_LANG1:def_10;
hence  [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:95; ::_thesis: ( ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
thus  for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ::_thesis: ( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
proof
let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
let e be Element of vSUB A; ::_thesis: [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
 p ! ll = <*p*> ^ ll by QC_LANG1:8;
hence  [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;
 VERUM A in QC-WFF A ;
hence  for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
thus  for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ::_thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
proof
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]
let e be Element of vSUB A; ::_thesis: ( [p,e] in [:(QC-WFF A),(vSUB A):] implies [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] )
assume  [p,e] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]
then  ex a, b being set st
( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by ZFMISC_1:def_2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
 'not' p9 = <*[1,0]*> ^ (@ p9) ;
hence  [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;
thus  for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ::_thesis: for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
proof
let p, q be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]
let e be Element of vSUB A; ::_thesis: ( [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] implies [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] )
assume that
A1: [p,e] in [:(QC-WFF A),(vSUB A):] and
A2: [q,e] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]
 ex c, d being set st
( c in QC-WFF A & d in vSUB A & [q,e] = [c,d] ) by A2, ZFMISC_1:def_2;
then reconsider q9 = q as Element of QC-WFF A by XTUPLE_0:1;
 ex a, b being set st
( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by A1, ZFMISC_1:def_2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
 p9 '&' q9 = (<*[2,0]*> ^ (@ p9)) ^ (@ q9) ;
hence  [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;
thus  for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ::_thesis: verum
proof
let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
let e be Element of vSUB A; ::_thesis: ( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] )
assume  [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
then  ex a, b being set st
( a in QC-WFF A & b in vSUB A & [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] = [a,b] ) by ZFMISC_1:def_2;
then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1;
 All (x,p9) = (<*[3,0]*> ^ <*x*>) ^ (@ p9) ;
hence  [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;
end;

definition
let A be QC-alphabet ;
let IT be set ;
attrIT is A -Sub-closed  means :Def16: :: SUBSTUT1:def 16
( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) );
end;

:: deftheorem Def16 defines -Sub-closed SUBSTUT1:def_16_:_
 for A being QC-alphabet
for IT being set holds
( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) ) );

registration
let A be QC-alphabet ;
cluster non empty A -Sub-closed for set ;
existence
 ex b1 being set st
( b1 is A -Sub-closed & not b1 is empty )
proof
take  [:(QC-WFF A),(vSUB A):] ; ::_thesis: ( [:(QC-WFF A),(vSUB A):] is A -Sub-closed & not [:(QC-WFF A),(vSUB A):] is empty )
 ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) ) by Th7;
hence  ( [:(QC-WFF A),(vSUB A):] is A -Sub-closed & not [:(QC-WFF A),(vSUB A):] is empty ) by Def16; ::_thesis: verum
end;
end;

Lm3:  for A being QC-alphabet
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
 0 in QC-symbols A by QC_LANG1:3;
then  [3,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then  ( rng <*[3,0]*> = {[3,0]} & {[3,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[3,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
 QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4;
then  bound_QC-variables A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then  rng <*x*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then reconsider z = <*x*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
 (y ^ z) ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
hence  (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] ; ::_thesis: verum
end;

Lm4:  for A being QC-alphabet
for k being Element of NAT
for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let k be Element of NAT ; ::_thesis: for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let l be QC-symbol of A; ::_thesis: for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let e be Element of vSUB A; ::_thesis: [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
 <*[k,l]*> in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
hence  [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;

Lm5:  for A being QC-alphabet
for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
 QC-pred_symbols A c= [:NAT,(QC-symbols A):] by QC_LANG1:6;
then  k -ary_QC-pred_symbols A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then A1: rng <*p*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
 QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4;
then  rng ll c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then  (rng <*p*>) \/ (rng ll) c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8;
then  rng (<*p*> ^ ll) c= [:NAT,(QC-symbols A):] by FINSEQ_1:31;
then  <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
then  <*p*> ^ ll in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
hence  for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
func QC-Sub-WFF A ->  non empty set  means :Def17: :: SUBSTUT1:def 17
( it is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
it c= D ) );
existence
 ex b1 being non empty set st
( b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) )
proof
set e = the Element of vSUB A;
defpred S1[ set ] means  for D being non empty set st D is A -Sub-closed holds
$1 in D;
consider D0 being set  such that
A1: for x being set holds
( x in D0 iff ( x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & S1[x] ) ) from XBOOLE_0:sch_1();
 0 in QC-symbols A by QC_LANG1:3;
then  ( [<*[0,0]*>, the Element of vSUB A] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[<*[0,0]*>, the Element of vSUB A] in D ) ) by Def16, Lm4;
then reconsider D0 = D0 as non empty set by A1;
take  D0 ; ::_thesis: ( D0 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
 D0 c= [:([:NAT,(QC-symbols A):] *),(vSUB A):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] )
thus  ( not x in D0 or x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] ) by A1; ::_thesis: verum
end;
hence  D0 is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] ; :: according to SUBSTUT1:def_16 ::_thesis: ( ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
thus  for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ::_thesis: ( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let e be Element of vSUB A; ::_thesis: [(<*p*> ^ ll),e] in D0
 ( [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[(<*p*> ^ ll),e] in D ) ) by Def16, Lm5;
hence  [(<*p*> ^ ll),e] in D0 by A1; ::_thesis: verum
end;
thus  for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ::_thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let e be Element of vSUB A; ::_thesis: [<*[0,0]*>,e] in D0
 0 in QC-symbols A by QC_LANG1:3;
then  ( [<*[0,0]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[<*[0,0]*>,e] in D ) ) by Def16, Lm4;
hence  [<*[0,0]*>,e] in D0 by A1; ::_thesis: verum
end;
thus  for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ::_thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0
let e be Element of vSUB A; ::_thesis: ( [p,e] in D0 implies [(<*[1,0]*> ^ p),e] in D0 )
assume A2: [p,e] in D0 ; ::_thesis: [(<*[1,0]*> ^ p),e] in D0
A3: for D being non empty set st D is A -Sub-closed holds
[(<*[1,0]*> ^ p),e] in D
proof
let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [(<*[1,0]*> ^ p),e] in D )
assume A4: D is A -Sub-closed ; ::_thesis: [(<*[1,0]*> ^ p),e] in D
then  [p,e] in D by A1, A2;
hence  [(<*[1,0]*> ^ p),e] in D by A4, Def16; ::_thesis: verum
end;
 0 in QC-symbols A by QC_LANG1:3;
then  [1,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then  ( rng <*[1,0]*> = {[1,0]} & {[1,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[1,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
 y ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
then  <*[1,0]*> ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
then  [(<*[1,0]*> ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2;
hence  [(<*[1,0]*> ^ p),e] in D0 by A1, A3; ::_thesis: verum
end;
thus  for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ::_thesis: ( ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let p, q be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0
let e be Element of vSUB A; ::_thesis: ( [p,e] in D0 & [q,e] in D0 implies [((<*[2,0]*> ^ p) ^ q),e] in D0 )
assume A5: ( [p,e] in D0 & [q,e] in D0 ) ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in D0
A6: for D being non empty set st D is A -Sub-closed holds
[((<*[2,0]*> ^ p) ^ q),e] in D
proof
let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [((<*[2,0]*> ^ p) ^ q),e] in D )
assume A7: D is A -Sub-closed ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in D
then  ( [p,e] in D & [q,e] in D ) by A1, A5;
hence  [((<*[2,0]*> ^ p) ^ q),e] in D by A7, Def16; ::_thesis: verum
end;
 0 in QC-symbols A by QC_LANG1:3;
then  [2,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then  ( rng <*[2,0]*> = {[2,0]} & {[2,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[2,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
 (y ^ p) ^ q is FinSequence of [:NAT,(QC-symbols A):] ;
then  (<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
then  [((<*[2,0]*> ^ p) ^ q),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2;
hence  [((<*[2,0]*> ^ p) ^ q),e] in D0 by A1, A6; ::_thesis: verum
end;
thus  for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ::_thesis: for D being non empty set st D is A -Sub-closed holds
D0 c= D
proof
let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
let e be Element of vSUB A; ::_thesis: ( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 )
assume A8: [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
A9: for D being non empty set st D is A -Sub-closed holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D
proof
let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D )
assume A10: D is A -Sub-closed ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in D
then  [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D by A1, A8;
hence  [((<*[3,0]*> ^ <*x*>) ^ p),e] in D by A10, Def16; ::_thesis: verum
end;
 (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] by Lm3;
then  (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
then  [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2;
hence  [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 by A1, A9; ::_thesis: verum
end;
let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies D0 c= D )
assume A11: D is A -Sub-closed ; ::_thesis: D0 c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D )
assume  x in D0 ; ::_thesis: x in D
hence  x in D by A1, A11; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty set st b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) & b2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be non empty set ; ::_thesis: ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D2 c= D ) implies D1 = D2 )
assume  ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D2 c= D ) ) ; ::_thesis: D1 = D2
then  ( D1 c= D2 & D2 c= D1 ) ;
hence  D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def_17_:_
 for A being QC-alphabet
for b2 being non empty set holds
( b2 = QC-Sub-WFF A iff ( b2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b2 c= D ) ) );


theorem Th8: :: SUBSTUT1:8
for A being QC-alphabet
for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]
let S be Element of QC-Sub-WFF A; ::_thesis: ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]
 ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) ) by Th7;
then  [:(QC-WFF A),(vSUB A):] is A -Sub-closed by Def16;
then  QC-Sub-WFF A c= [:(QC-WFF A),(vSUB A):] by Def17;
then  S in [:(QC-WFF A),(vSUB A):] by TARSKI:def_3;
then consider a, b being set  such that
A1: a in QC-WFF A and
A2: b in vSUB A and
A3: S = [a,b] by ZFMISC_1:def_2;
reconsider e = b as Element of vSUB A by A2;
reconsider p = a as Element of QC-WFF A by A1;
take  p ; ::_thesis: ex e being Element of vSUB A st S = [p,e]
take  e ; ::_thesis: S = [p,e]
thus  S = [p,e] by A3; ::_thesis: verum
end;

registration
let A be QC-alphabet ;
cluster QC-Sub-WFF A ->  non empty A -Sub-closed ;
coherence
 QC-Sub-WFF A is A -Sub-closed by Def17;
end;

definition
let A be QC-alphabet ;
let P be QC-pred_symbol of A;
let l be FinSequence of QC-variables A;
let e be Element of vSUB A;
assume A1: the_arity_of P = len l ;
func Sub_P (P,l,e) ->  Element of QC-Sub-WFF A equals :Def18: :: SUBSTUT1:def 18
[(P ! l),e];
coherence
 [(P ! l),e] is Element of QC-Sub-WFF A
proof
set k = len l;
set QCP =  {  QP where QP is QC-pred_symbol of A : the_arity_of QP = len l  }  ;
 P in  {  QP where QP is QC-pred_symbol of A : the_arity_of QP = len l  }  by A1;
then reconsider P = P as QC-pred_symbol of (len l),A ;
reconsider l = l as QC-variable_list of len l,A by CARD_1:def_7;
 P ! l = <*P*> ^ l by QC_LANG1:8;
hence  [(P ! l),e] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def_18_:_
 for A being QC-alphabet
for P being QC-pred_symbol of A
for l being FinSequence of QC-variables A
for e being Element of vSUB A st the_arity_of P = len l holds
Sub_P (P,l,e) = [(P ! l),e];

theorem Th9: :: SUBSTUT1:9
for A being QC-alphabet
for e being Element of vSUB A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
proof
let A be QC-alphabet ; ::_thesis: for e being Element of vSUB A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let e be Element of vSUB A; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let ll be QC-variable_list of k,A; ::_thesis: Sub_P (P,ll,e) = [(P ! ll),e]
set QCP =  {  QP where QP is QC-pred_symbol of A : the_arity_of QP = k  }  ;
 P in  {  QP where QP is QC-pred_symbol of A : the_arity_of QP = k  }  ;
then A1: ex Q being QC-pred_symbol of A st
( P = Q & the_arity_of Q = k ) ;
 len ll = k by CARD_1:def_7;
hence  Sub_P (P,ll,e) = [(P ! ll),e] by A1, Def18; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is A -Sub_VERUM  means :Def19: :: SUBSTUT1:def 19
 ex e being Element of vSUB A st S = [(VERUM A),e];
end;

:: deftheorem Def19 defines -Sub_VERUM SUBSTUT1:def_19_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
:: original: `1
redefine funcS `1  ->  Element of QC-WFF A;
coherence
 S `1 is Element of QC-WFF A
proof
 ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8;
hence  S `1 is Element of QC-WFF A by MCART_1:7; ::_thesis: verum
end;
:: original: `2
redefine funcS `2  ->  Element of vSUB A;
coherence
 S `2 is Element of vSUB A
proof
 ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8;
hence  S `2 is Element of vSUB A by MCART_1:7; ::_thesis: verum
end;
end;

theorem Th10: :: SUBSTUT1:10
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds S = [(S `1),(S `2)]
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds S = [(S `1),(S `2)]
let S be Element of QC-Sub-WFF A; ::_thesis: S = [(S `1),(S `2)]
 ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8;
hence  S = [(S `1),(S `2)] by MCART_1:8; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
func Sub_not S ->  Element of QC-Sub-WFF A equals :: SUBSTUT1:def 20
[('not' (S `1)),(S `2)];
coherence
 [('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A
proof
 [(S `1),(S `2)] is Element of QC-Sub-WFF A by Th10;
hence  [('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum
end;
end;

:: deftheorem  defines Sub_not SUBSTUT1:def_20_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)];

definition
let A be QC-alphabet ;
let S, S9 be Element of QC-Sub-WFF A;
assume A1: S `2 = S9 `2 ;
func Sub_& (S,S9) ->  Element of QC-Sub-WFF A equals :Def21: :: SUBSTUT1:def 21
[((S `1) '&' (S9 `1)),(S `2)];
coherence
 [((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A
proof
 ( [(S `1),(S `2)] is Element of QC-Sub-WFF A & [(S9 `1),(S9 `2)] is Element of QC-Sub-WFF A ) by Th10;
hence  [((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A by A1, Def16; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines Sub_& SUBSTUT1:def_21_:_
 for A being QC-alphabet
for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds
Sub_& (S,S9) = [((S `1) '&' (S9 `1)),(S `2)];

definition
let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
:: original: `1
redefine funcB `1  ->  Element of QC-Sub-WFF A;
coherence
 B `1 is Element of QC-Sub-WFF A by MCART_1:10;
:: original: `2
redefine funcB `2  ->  Element of bound_QC-variables A;
coherence
 B `2 is Element of bound_QC-variables A by MCART_1:10;
end;

definition
let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
attrB is quantifiable  means :Def22: :: SUBSTUT1:def 22
 ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e];
end;

:: deftheorem Def22 defines quantifiable SUBSTUT1:def_22_:_
 for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds
( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] );

definition
let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
assume A1: B is quantifiable ;
mode second_Q_comp of B ->  Element of vSUB A means :Def23: :: SUBSTUT1:def 23
(B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),it];
existence
 ex b1 being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b1] by A1, Def22;
end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def_23_:_
 for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] st B is quantifiable holds
for b3 being Element of vSUB A holds
( b3 is second_Q_comp of B iff (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b3] );

definition
let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;
func Sub_All (B,SQ) ->  Element of QC-Sub-WFF A equals :Def24: :: SUBSTUT1:def 24
[(All ((B `2),((B `1) `1))),SQ];
coherence
 [(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A
proof
 (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),SQ] by A1, Def23;
then  B `1 = [((B `1) `1),((QSub A) . [(All ((B `2),((B `1) `1))),SQ])] by Th10;
hence  [(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum
end;
end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def_24_:_
 for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ];

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
let x be bound_QC-variable of A;
:: original: [
redefine func[S,x] ->  Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
coherence
 [S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
proof
 [S,x] in [:(QC-Sub-WFF A),(bound_QC-variables A):] ;
hence  [S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ; ::_thesis: verum
end;
end;

scheme :: SUBSTUT1:sch 1
SubQCInd{ F1() ->  QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } :
 for S being Element of QC-Sub-WFF F1() holds P1[S]
provided
A1: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] and
A2: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
P1[S] and
A3: for S being Element of QC-Sub-WFF F1() st P1[S] holds
P1[ Sub_not S] and
A4: for S, S9 being Element of QC-Sub-WFF F1() st S `2 = S9 `2 & P1[S] & P1[S9] holds
P1[ Sub_& (S,S9)] and
A5: for x being bound_QC-variable of F1()
for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
proof
set X =  {  S where S is Element of QC-Sub-WFF F1() : P1[S]  }  ;
 not  {  S where S is Element of QC-Sub-WFF F1() : P1[S]  }  is empty
proof
set e = the Element of vSUB F1();
reconsider V = [(VERUM F1()), the Element of vSUB F1()] as Element of QC-Sub-WFF F1() by Def16;
 V is F1() -Sub_VERUM by Def19;
then  P1[V] by A2;
then  V in  {  S where S is Element of QC-Sub-WFF F1() : P1[S]  }  ;
hence  not  {  S where S is Element of QC-Sub-WFF F1() : P1[S]  }  is empty ; ::_thesis: verum
end;
then reconsider X =  {  S where S is Element of QC-Sub-WFF F1() : P1[S]  }  as non empty set ;
 for e being Element of vSUB F1() holds [(VERUM F1()),e] in X
proof
let e be Element of vSUB F1(); ::_thesis: [(VERUM F1()),e] in X
reconsider V = [(VERUM F1()),e] as Element of QC-Sub-WFF F1() by Def16;
 V is F1() -Sub_VERUM by Def19;
then  P1[V] by A2;
hence  [(VERUM F1()),e] in X ; ::_thesis: verum
end;
then A6: for e being Element of vSUB F1() holds [<*[0,0]*>,e] in X ;
A7: for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
proof
let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
let e be Element of vSUB F1(); ::_thesis: ( [p,e] in X implies [(<*[1,0]*> ^ p),e] in X )
assume  [p,e] in X ; ::_thesis: [(<*[1,0]*> ^ p),e] in X
then consider S being Element of QC-Sub-WFF F1() such that
A8: S = [p,e] and
A9: P1[S] ;
 P1[ Sub_not S] by A3, A9;
then A10: Sub_not S in X ;
consider p9 being Element of QC-WFF F1(), e9 being Element of vSUB F1() such that
A11: S = [p9,e9] by Th8;
A12: S `1 = p9 by A11, MCART_1:7;
 p = p9 by A8, A11, XTUPLE_0:1;
hence  [(<*[1,0]*> ^ p),e] in X by A8, A10, A12, MCART_1:7; ::_thesis: verum
end;
A13: for x being bound_QC-variable of F1()
for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
proof
let x be bound_QC-variable of F1(); ::_thesis: for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let e be Element of vSUB F1(); ::_thesis: ( [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in X )
assume  [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in X
then consider S being Element of QC-Sub-WFF F1() such that
A14: S = [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] and
A15: P1[S] ;
consider B being set  such that
A16: B = [S,x] ;
reconsider B = B as Element of [:(QC-Sub-WFF F1()),(bound_QC-variables F1()):] by A16;
A17: ( B `1 = S & B `2 = x ) by A16, MCART_1:7;
 S `1 = p by A14, MCART_1:7;
then A18: S `2 = (QSub F1()) . [(All (x,(S `1))),e] by A14, MCART_1:7;
then A19: B is quantifiable by A17, Def22;
then reconsider e = e as second_Q_comp of B by A18, A17, Def23;
 P1[ Sub_All (B,e)] by A5, A15, A16, A19;
then  Sub_All (B,e) in X ;
then  [(All ((B `2),((B `1) `1))),e] in X by A19, Def24;
hence  [((<*[3,0]*> ^ <*x*>) ^ p),e] in X by A14, A17, MCART_1:7; ::_thesis: verum
end;
let F be Element of QC-Sub-WFF F1(); ::_thesis: P1[F]
A20: X c= [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] )
assume  x in X ; ::_thesis: x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
then  ex S being Element of QC-Sub-WFF F1() st
( x = S & P1[S] ) ;
then consider p being Element of QC-WFF F1(), e being Element of vSUB F1() such that
A21: x = [p,e] by Th8;
 p = @ p ;
then  p in [:NAT,(QC-symbols F1()):] * by FINSEQ_1:def_11;
hence  x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] by A21, ZFMISC_1:def_2; ::_thesis: verum
end;
A22: for p, q being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
proof
let p, q be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
let e be Element of vSUB F1(); ::_thesis: ( [p,e] in X & [q,e] in X implies [((<*[2,0]*> ^ p) ^ q),e] in X )
assume  [p,e] in X ; ::_thesis: ( not [q,e] in X or [((<*[2,0]*> ^ p) ^ q),e] in X )
then consider S1 being Element of QC-Sub-WFF F1() such that
A23: S1 = [p,e] and
A24: P1[S1] ;
assume  [q,e] in X ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in X
then consider S2 being Element of QC-Sub-WFF F1() such that
A25: S2 = [q,e] and
A26: P1[S2] ;
consider p9 being Element of QC-WFF F1(), e1 being Element of vSUB F1() such that
A27: [p,e] = [p9,e1] by A23, Th8;
A28: e = e1 by A27, XTUPLE_0:1;
A29: S1 `2 = e1 by A23, A27, MCART_1:7;
then A30: S1 `2 = S2 `2 by A25, A28, MCART_1:7;
then  P1[ Sub_& (S1,S2)] by A4, A24, A26;
then  Sub_& (S1,S2) in X ;
then A31: [((S1 `1) '&' (S2 `1)),(S1 `2)] in X by A30, Def21;
A32: p = p9 by A27, XTUPLE_0:1;
 S1 `1 = p9 by A23, A27, MCART_1:7;
hence  [((<*[2,0]*> ^ p) ^ q),e] in X by A25, A32, A28, A29, A31, MCART_1:7; ::_thesis: verum
end;
 for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let ll be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let e be Element of vSUB F1(); ::_thesis: [(<*P*> ^ ll),e] in X
 ( P1[ Sub_P (P,ll,e)] & [(P ! ll),e] = Sub_P (P,ll,e) ) by A1, Th9;
then  [(P ! ll),e] in X ;
hence  [(<*P*> ^ ll),e] in X by QC_LANG1:8; ::_thesis: verum
end;
then  X is F1() -Sub-closed by A20, A6, A7, A22, A13, Def16;
then  QC-Sub-WFF F1() c= X by Def17;
then  F in X by TARSKI:def_3;
then  ex S being Element of QC-Sub-WFF F1() st
( S = F & P1[S] ) ;
hence  P1[F] ; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is Sub_atomic  means :Def25: :: SUBSTUT1:def 25
 ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e);
end;

:: deftheorem Def25 defines Sub_atomic SUBSTUT1:def_25_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_atomic iff ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e) );

theorem Th11: :: SUBSTUT1:11
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
S `1 is atomic
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
S `1 is atomic
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_atomic implies S `1 is atomic )
assume  S is Sub_atomic ; ::_thesis: S `1 is atomic
then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that
A1: S = Sub_P (P,ll,e) by Def25;
 S = [(P ! ll),e] by A1, Th9;
then  S `1 = P ! ll by MCART_1:7;
hence  S `1 is atomic by QC_LANG1:def_18; ::_thesis: verum
end;

registration
let A be QC-alphabet ;
let k be Element of NAT ;
let P be QC-pred_symbol of k,A;
let ll be QC-variable_list of k,A;
let e be Element of vSUB A;
cluster Sub_P (P,ll,e) ->  Sub_atomic ;
coherence
 Sub_P (P,ll,e) is Sub_atomic by Def25;
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is Sub_negative  means :Def26: :: SUBSTUT1:def 26
 ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9;
attrS is Sub_conjunctive  means :Def27: :: SUBSTUT1:def 27
 ex S1, S2 being Element of QC-Sub-WFF A st
( S = Sub_& (S1,S2) & S1 `2 = S2 `2 );
end;

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def_26_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 );

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def_27_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF A st
( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is Sub_universal  means :Def28: :: SUBSTUT1:def 28
 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B is quantifiable );
end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def_28_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_universal iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B is quantifiable ) );

theorem Th12: :: SUBSTUT1:12
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal )
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal )
defpred S1[ Element of QC-Sub-WFF A] means ( $1 is A -Sub_VERUM or $1 is Sub_atomic or $1 is Sub_negative or $1 is Sub_conjunctive or $1 is Sub_universal );
A1: for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds S1[ Sub_P (p,ll,e)] ;
A2: for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds
S1[S] ;
A3: for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)] by Def28;
A4: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds
S1[ Sub_& (S1,S2)] by Def27;
A5: for S being Element of QC-Sub-WFF A st S1[S] holds
S1[ Sub_not S] by Def26;
thus  for S being Element of QC-Sub-WFF A holds S1[S] from SUBSTUT1:sch_1(A1, A2, A5, A4, A3); ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: S is Sub_atomic ;
func Sub_the_arguments_of S ->  FinSequence of QC-variables A means :Def29: :: SUBSTUT1:def 29
 ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( it = ll & S = Sub_P (P,ll,e) );
existence
 ex b1 being FinSequence of QC-variables A ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( b1 = ll & S = Sub_P (P,ll,e) )
proof
consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that
A1: S = Sub_P (P,ll,e) by B1, Def25;
reconsider ll = ll as FinSequence of QC-variables A ;
take  ll ; ::_thesis: ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll = ll & S = Sub_P (P,ll,e) )
thus  ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll = ll & S = Sub_P (P,ll,e) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of QC-variables A st ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( b1 = ll & S = Sub_P (P,ll,e) ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( b2 = ll & S = Sub_P (P,ll,e) ) holds
b1 = b2
proof
let ll1, ll2 be FinSequence of QC-variables A; ::_thesis: ( ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll1 = ll & S = Sub_P (P,ll,e) ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll2 = ll & S = Sub_P (P,ll,e) ) implies ll1 = ll2 )
given k1 being Element of NAT , P1 being QC-pred_symbol of k1,A, ll19 being QC-variable_list of k1,A, e1 being Element of vSUB A such that A2: ll1 = ll19 and
A3: S = Sub_P (P1,ll19,e1) ; ::_thesis: ( for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds
( not ll2 = ll or not S = Sub_P (P,ll,e) ) or ll1 = ll2 )
A4: S = [(P1 ! ll19),e1] by A3, Th9;
given k2 being Element of NAT , P2 being QC-pred_symbol of k2,A, ll29 being QC-variable_list of k2,A, e2 being Element of vSUB A such that A5: ll2 = ll29 and
A6: S = Sub_P (P2,ll29,e2) ; ::_thesis: ll1 = ll2
 <*P1*> ^ ll19 = P1 ! ll19 by QC_LANG1:8;
then A7: ( <*P2*> ^ ll29 = P2 ! ll29 & S `1 = <*P1*> ^ ll19 ) by A4, MCART_1:7, QC_LANG1:8;
A8: S `1 is atomic by B1, Th11;
A9: S = [(P2 ! ll29),e2] by A6, Th9;
then A10: S `1 = P2 ! ll29 by MCART_1:7;
 S `1 = P1 ! ll19 by A4, MCART_1:7;
then P1 = the_pred_symbol_of (S `1) by A8, QC_LANG1:def_22
.= P2 by A10, A8, QC_LANG1:def_22 ;
hence  ll1 = ll2 by A2, A5, A9, A7, FINSEQ_1:33, MCART_1:7; ::_thesis: verum
end;
end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def_29_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
for b3 being FinSequence of QC-variables A holds
( b3 = Sub_the_arguments_of S iff ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( b3 = ll & S = Sub_P (P,ll,e) ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_negative ;
func Sub_the_argument_of S ->  Element of QC-Sub-WFF A means :Def30: :: SUBSTUT1:def 30
S = Sub_not it;
existence
 ex b1 being Element of QC-Sub-WFF A st S = Sub_not b1 by A1, Def26;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st S = Sub_not b1 & S = Sub_not b2 holds
b1 = b2
proof
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S = Sub_not S1 & S = Sub_not S2 implies S1 = S2 )
A1: ( S1 = [(S1 `1),(S1 `2)] & S2 = [(S2 `1),(S2 `2)] ) by Th10;
assume A2: ( S = Sub_not S1 & S = Sub_not S2 ) ; ::_thesis: S1 = S2
then  'not' (S1 `1) = 'not' (S2 `1) by XTUPLE_0:1;
then  S1 `1 = S2 `1 by FINSEQ_1:33;
hence  S1 = S2 by A2, A1, XTUPLE_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def_30_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_argument_of S iff S = Sub_not b3 );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_conjunctive ;
func Sub_the_left_argument_of S ->  Element of QC-Sub-WFF A means :Def31: :: SUBSTUT1:def 31
 ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (it,S9) & it `2 = S9 `2 );
existence
 ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b1,S9) & b1 `2 = S9 `2 ) by A1, Def27;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b1,S9) & b1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b2,S9) & b2 `2 = S9 `2 ) holds
b1 = b2
proof
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S1,S9) & S1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S2,S9) & S2 `2 = S9 `2 ) implies S1 = S2 )
given T1 being Element of QC-Sub-WFF A such that A1: ( S = Sub_& (S1,T1) & S1 `2 = T1 `2 ) ; ::_thesis: ( for S9 being Element of QC-Sub-WFF A holds
( not S = Sub_& (S2,S9) or not S2 `2 = S9 `2 ) or S1 = S2 )
given T2 being Element of QC-Sub-WFF A such that A2: ( S = Sub_& (S2,T2) & S2 `2 = T2 `2 ) ; ::_thesis: S1 = S2
A3: ( len (@ (S1 `1)) <= len (@ (S2 `1)) or len (@ (S2 `1)) <= len (@ (S1 `1)) ) ;
A4: S = [((S2 `1) '&' (T2 `1)),(S2 `2)] by A2, Def21;
A5: S = [((S1 `1) '&' (T1 `1)),(S1 `2)] by A1, Def21;
then  (S1 `1) '&' (T1 `1) = (S2 `1) '&' (T2 `1) by A4, XTUPLE_0:1;
then <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (T1 `1))) = (S2 `1) '&' (T2 `1) by FINSEQ_1:32
.= <*[2,0]*> ^ ((@ (S2 `1)) ^ (@ (T2 `1))) by FINSEQ_1:32 ;
then  (@ (S1 `1)) ^ (@ (T1 `1)) = (@ (S2 `1)) ^ (@ (T2 `1)) by FINSEQ_1:33;
then consider a, b, c, d being FinSequence such that
A6: ( ( a = @ (S1 `1) & b = @ (S2 `1) ) or ( a = @ (S2 `1) & b = @ (S1 `1) ) ) and
A7: ( len a <= len b & a ^ c = b ^ d ) by A3;
A8: ( S1 = [(S1 `1),(S1 `2)] & S2 = [(S2 `1),(S2 `2)] ) by Th10;
 ex t being FinSequence st a ^ t = b by A7, FINSEQ_1:47;
then  S1 `1 = S2 `1 by A6, QC_LANG1:13;
hence  S1 = S2 by A5, A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def_31_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_left_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b3,S9) & b3 `2 = S9 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: S is Sub_conjunctive ;
func Sub_the_right_argument_of S ->  Element of QC-Sub-WFF A means :Def32: :: SUBSTUT1:def 32
 ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,it) & S9 `2 = it `2 );
existence
 ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b1) & S9 `2 = b1 `2 )
proof
consider S1, S2 being Element of QC-Sub-WFF A such that
A1: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by B1, Def27;
take  S2 ; ::_thesis: ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,S2) & S9 `2 = S2 `2 )
thus  ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,S2) & S9 `2 = S2 `2 ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b1) & S9 `2 = b1 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b2) & S9 `2 = b2 `2 ) holds
b1 = b2
proof
let T1, T2 be Element of QC-Sub-WFF A; ::_thesis: ( ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,T1) & S9 `2 = T1 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,T2) & S9 `2 = T2 `2 ) implies T1 = T2 )
given S1 being Element of QC-Sub-WFF A such that A2: ( S = Sub_& (S1,T1) & S1 `2 = T1 `2 ) ; ::_thesis: ( for S9 being Element of QC-Sub-WFF A holds
( not S = Sub_& (S9,T2) or not S9 `2 = T2 `2 ) or T1 = T2 )
A3: ( T1 = [(T1 `1),(T1 `2)] & T2 = [(T2 `1),(T2 `2)] ) by Th10;
given S2 being Element of QC-Sub-WFF A such that A4: ( S = Sub_& (S2,T2) & S2 `2 = T2 `2 ) ; ::_thesis: T1 = T2
A5: S = [((S1 `1) '&' (T1 `1)),(T1 `2)] by A2, Def21;
A6: S = [((S2 `1) '&' (T2 `1)),(T2 `2)] by A4, Def21;
then  (S1 `1) '&' (T1 `1) = (S2 `1) '&' (T2 `1) by A5, XTUPLE_0:1;
then <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (T1 `1))) = (S2 `1) '&' (T2 `1) by FINSEQ_1:32
.= <*[2,0]*> ^ ((@ (S2 `1)) ^ (@ (T2 `1))) by FINSEQ_1:32 ;
then A7: (@ (S1 `1)) ^ (@ (T1 `1)) = (@ (S2 `1)) ^ (@ (T2 `1)) by FINSEQ_1:33;
S1 = Sub_the_left_argument_of S by B1, A2, Def31
.= S2 by B1, A4, Def31 ;
then  @ (T1 `1) = @ (T2 `1) by A7, FINSEQ_1:33;
hence  T1 = T2 by A5, A6, A3, XTUPLE_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def_32_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_right_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b3) & S9 `2 = b3 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: S is Sub_universal ;
func Sub_the_bound_of S ->  bound_QC-variable of A means :: SUBSTUT1:def 33
 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = it & B is quantifiable );
existence
 ex b1 being bound_QC-variable of A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = b1 & B is quantifiable )
proof
consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A1: ( S = Sub_All (B,SQ) & B is quantifiable ) by B1, Def28;
take  B `2 ; ::_thesis: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable )
thus  ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being bound_QC-variable of A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = b1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = b2 & B is quantifiable ) holds
b1 = b2
proof
let x1, x2 be bound_QC-variable of A; ::_thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) implies x1 = x2 )
assume that
A2: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x1 & B is quantifiable ) and
A3: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) ; ::_thesis: x1 = x2
consider B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that
A4: S = Sub_All (B1,SQ1) and
A5: B1 `2 = x1 and
A6: B1 is quantifiable by A2;
consider B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that
A7: S = Sub_All (B2,SQ2) and
A8: B2 `2 = x2 and
A9: B2 is quantifiable by A3;
A10: [(All ((B2 `2),((B2 `1) `1))),SQ2] = S by A7, A9, Def24;
 [(All ((B1 `2),((B1 `1) `1))),SQ1] = S by A4, A6, Def24;
then  All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A10, XTUPLE_0:1;
hence  x1 = x2 by A5, A8, QC_LANG2:5; ::_thesis: verum
end;
end;

:: deftheorem  defines Sub_the_bound_of SUBSTUT1:def_33_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
for b3 being bound_QC-variable of A holds
( b3 = Sub_the_bound_of S iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = b3 & B is quantifiable ) );

definition
let A be QC-alphabet ;
let A2 be Element of QC-Sub-WFF A;
assume B1: A2 is Sub_universal ;
func Sub_the_scope_of A2 ->  Element of QC-Sub-WFF A means :Def34: :: SUBSTUT1:def 34
 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = it & B is quantifiable );
existence
 ex b1 being Element of QC-Sub-WFF A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = b1 & B is quantifiable )
proof
consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A1: ( A2 = Sub_All (B,SQ) & B is quantifiable ) by B1, Def28;
take  B `1 ; ::_thesis: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = B `1 & B is quantifiable )
thus  ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = B `1 & B is quantifiable ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = b1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = b2 & B is quantifiable ) holds
b1 = b2
proof
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = S1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = S2 & B is quantifiable ) implies S1 = S2 )
given B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that A2: A2 = Sub_All (B1,SQ1) and
A3: B1 `1 = S1 and
A4: B1 is quantifiable ; ::_thesis: ( for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B holds
( not A2 = Sub_All (B,SQ) or not B `1 = S2 or not B is quantifiable ) or S1 = S2 )
A5: A2 = [(All ((B1 `2),((B1 `1) `1))),SQ1] by A2, A4, Def24;
A6: (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A4, Def23;
given B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that A7: A2 = Sub_All (B2,SQ2) and
A8: B2 `1 = S2 and
A9: B2 is quantifiable ; ::_thesis: S1 = S2
A10: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10;
A11: A2 = [(All ((B2 `2),((B2 `1) `1))),SQ2] by A7, A9, Def24;
then  All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A5, XTUPLE_0:1;
then  (B1 `1) `1 = (B2 `1) `1 by QC_LANG2:5;
hence  S1 = S2 by A3, A8, A9, A5, A11, A6, A10, Def23; ::_thesis: verum
end;
end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def_34_:_
 for A being QC-alphabet
for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_scope_of A2 iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = b3 & B is quantifiable ) );

registration
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
cluster Sub_not S ->  Sub_negative ;
coherence
 Sub_not S is Sub_negative
proof
take  S ; :: according to SUBSTUT1:def_26 ::_thesis: Sub_not S = Sub_not S
thus  Sub_not S = Sub_not S ; ::_thesis: verum
end;
end;

theorem Th13: :: SUBSTUT1:13
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_& (S1,S2) is Sub_conjunctive
proof
let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_& (S1,S2) is Sub_conjunctive
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_& (S1,S2) is Sub_conjunctive )
assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_& (S1,S2) is Sub_conjunctive
take  S1 ; :: according to SUBSTUT1:def_27 ::_thesis: ex S2 being Element of QC-Sub-WFF A st
( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 )
take  S2 ; ::_thesis: ( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 )
thus  ( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by A1; ::_thesis: verum
end;

theorem Th14: :: SUBSTUT1:14
for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) is Sub_universal
proof
let A be QC-alphabet ; ::_thesis: for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) is Sub_universal
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) is Sub_universal
let SQ be second_Q_comp of B; ::_thesis: ( B is quantifiable implies Sub_All (B,SQ) is Sub_universal )
assume A1: B is quantifiable ; ::_thesis: Sub_All (B,SQ) is Sub_universal
take  B ; :: according to SUBSTUT1:def_28 ::_thesis: ex SQ being second_Q_comp of B st
( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable )
take  SQ ; ::_thesis: ( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable )
thus  ( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable ) by A1; ::_thesis: verum
end;

theorem :: SUBSTUT1:15
for A being QC-alphabet
for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds
S = S9
proof
let A be QC-alphabet ; ::_thesis: for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds
S = S9
let S, S9 be Element of QC-Sub-WFF A; ::_thesis: ( Sub_not S = Sub_not S9 implies S = S9 )
assume  Sub_not S = Sub_not S9 ; ::_thesis: S = S9
then A1: ( 'not' (S `1) = 'not' (S9 `1) & S `2 = S9 `2 ) by XTUPLE_0:1;
 ( S = [(S `1),(S `2)] & S9 = [(S9 `1),(S9 `2)] ) by Th10;
hence  S = S9 by A1, FINSEQ_1:33; ::_thesis: verum
end;

theorem :: SUBSTUT1:16
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds Sub_the_argument_of (Sub_not S) = S by Def30;

theorem :: SUBSTUT1:17
for A being QC-alphabet
for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds
( S1 = S19 & S2 = S29 )
proof
let A be QC-alphabet ; ::_thesis: for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds
( S1 = S19 & S2 = S29 )
let S1, S2, S19, S29 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) implies ( S1 = S19 & S2 = S29 ) )
assume that
A1: S1 `2 = S2 `2 and
A2: S19 `2 = S29 `2 and
A3: Sub_& (S1,S2) = Sub_& (S19,S29) ; ::_thesis: ( S1 = S19 & S2 = S29 )
 Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, Def21;
then  [((S1 `1) '&' (S2 `1)),(S1 `2)] = [((S19 `1) '&' (S29 `1)),(S19 `2)] by A2, A3, Def21;
then A4: ( (S1 `1) '&' (S2 `1) = (S19 `1) '&' (S29 `1) & S1 `2 = S19 `2 ) by XTUPLE_0:1;
A5: ( S2 = [(S2 `1),(S2 `2)] & S29 = [(S29 `1),(S29 `2)] ) by Th10;
 ( S1 = [(S1 `1),(S1 `2)] & S19 = [(S19 `1),(S19 `2)] ) by Th10;
hence  ( S1 = S19 & S2 = S29 ) by A1, A2, A4, A5, QC_LANG2:2; ::_thesis: verum
end;

theorem Th18: :: SUBSTUT1:18
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1
proof
let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 )
assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_the_left_argument_of (Sub_& (S1,S2)) = S1
then  Sub_& (S1,S2) is Sub_conjunctive by Th13;
hence  Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 by A1, Def31; ::_thesis: verum
end;

theorem Th19: :: SUBSTUT1:19
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
proof
let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 )
assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
then  Sub_& (S1,S2) is Sub_conjunctive by Th13;
hence  Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A1, Def32; ::_thesis: verum
end;

theorem :: SUBSTUT1:20
for A being QC-alphabet
for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2
proof
let A be QC-alphabet ; ::_thesis: for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2
let B1, B2 be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2
let SQ1 be second_Q_comp of B1; ::_thesis: for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2
let SQ2 be second_Q_comp of B2; ::_thesis: ( B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) implies B1 = B2 )
assume that
A1: B1 is quantifiable and
A2: B2 is quantifiable and
A3: Sub_All (B1,SQ1) = Sub_All (B2,SQ2) ; ::_thesis: B1 = B2
A4: ( Sub_All (B1,SQ1) = [(All ((B1 `2),((B1 `1) `1))),SQ1] & Sub_All (B2,SQ2) = [(All ((B2 `2),((B2 `1) `1))),SQ2] ) by A1, A2, Def24;
then  All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A3, XTUPLE_0:1;
then A5: ( B1 `2 = B2 `2 & (B1 `1) `1 = (B2 `1) `1 ) by QC_LANG2:5;
 ex a, b being set st
( a in QC-Sub-WFF A & b in bound_QC-variables A & B2 = [a,b] ) by ZFMISC_1:def_2;
then A6: B2 = [(B2 `1),(B2 `2)] by MCART_1:8;
 ex a, b being set st
( a in QC-Sub-WFF A & b in bound_QC-variables A & B1 = [a,b] ) by ZFMISC_1:def_2;
then A7: B1 = [(B1 `1),(B1 `2)] by MCART_1:8;
A8: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10;
 (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A1, Def23;
hence  B1 = B2 by A2, A3, A4, A5, A8, A7, A6, Def23; ::_thesis: verum
end;

theorem Th21: :: SUBSTUT1:21
for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_the_scope_of (Sub_All (B,SQ)) = B `1
proof
let A be QC-alphabet ; ::_thesis: for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_the_scope_of (Sub_All (B,SQ)) = B `1
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ being second_Q_comp of B st B is quantifiable holds
Sub_the_scope_of (Sub_All (B,SQ)) = B `1
let SQ be second_Q_comp of B; ::_thesis: ( B is quantifiable implies Sub_the_scope_of (Sub_All (B,SQ)) = B `1 )
assume A1: B is quantifiable ; ::_thesis: Sub_the_scope_of (Sub_All (B,SQ)) = B `1
then  Sub_All (B,SQ) is Sub_universal by Th14;
hence  Sub_the_scope_of (Sub_All (B,SQ)) = B `1 by A1, Def34; ::_thesis: verum
end;

scheme :: SUBSTUT1:sch 2
SubQCInd2{ F1() ->  QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } :
 for S being Element of QC-Sub-WFF F1() holds P1[S]
provided
A1: for S being Element of QC-Sub-WFF F1() holds
( ( S is Sub_atomic implies P1[S] ) & ( S is F1() -Sub_VERUM implies P1[S] ) & ( S is Sub_negative & P1[ Sub_the_argument_of S] implies P1[S] ) & ( S is Sub_conjunctive & P1[ Sub_the_left_argument_of S] & P1[ Sub_the_right_argument_of S] implies P1[S] ) & ( S is Sub_universal & P1[ Sub_the_scope_of S] implies P1[S] ) )
proof
A2: now__::_thesis:_for_x_being_bound_QC-variable_of_F1()
for_S_being_Element_of_QC-Sub-WFF_F1()
for_SQ_being_second_Q_comp_of_[S,x]_st_[S,x]_is_quantifiable_&_P1[S]_holds_
P1[_Sub_All_([S,x],SQ)]
let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] )
assume that
A3: [S,x] is quantifiable and
A4: P1[S] ; ::_thesis: P1[ Sub_All ([S,x],SQ)]
 [S,x] `1 = Sub_the_scope_of (Sub_All ([S,x],SQ)) by A3, Th21;
then A5: S = Sub_the_scope_of (Sub_All ([S,x],SQ)) ;
 Sub_All ([S,x],SQ) is Sub_universal by A3, Th14;
hence  P1[ Sub_All ([S,x],SQ)] by A1, A4, A5; ::_thesis: verum
end;
A6: now__::_thesis:_for_S1,_S2_being_Element_of_QC-Sub-WFF_F1()_st_S1_`2_=_S2_`2_&_P1[S1]_&_P1[S2]_holds_
P1[_Sub_&_(S1,S2)]
let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & P1[S1] & P1[S2] implies P1[ Sub_& (S1,S2)] )
assume that
A7: S1 `2 = S2 `2 and
A8: ( P1[S1] & P1[S2] ) ; ::_thesis: P1[ Sub_& (S1,S2)]
A9: S2 = Sub_the_right_argument_of (Sub_& (S1,S2)) by A7, Th19;
 ( Sub_& (S1,S2) is Sub_conjunctive & S1 = Sub_the_left_argument_of (Sub_& (S1,S2)) ) by A7, Th13, Th18;
hence  P1[ Sub_& (S1,S2)] by A1, A8, A9; ::_thesis: verum
end;
A10: now__::_thesis:_for_S_being_Element_of_QC-Sub-WFF_F1()_st_P1[S]_holds_
P1[_Sub_not_S]
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( P1[S] implies P1[ Sub_not S] )
assume A11: P1[S] ; ::_thesis: P1[ Sub_not S]
 S = Sub_the_argument_of (Sub_not S) by Def30;
hence  P1[ Sub_not S] by A1, A11; ::_thesis: verum
end;
A12: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
P1[S] by A1;
A13: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] by A1;
thus  for S being Element of QC-Sub-WFF F1() holds P1[S] from SUBSTUT1:sch_1(A13, A12, A10, A6, A2); ::_thesis: verum
end;

theorem Th22: :: SUBSTUT1:22
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_negative implies len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) )
assume  S is Sub_negative ; ::_thesis: len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))
then consider S9 being Element of QC-Sub-WFF A such that
A1: S = Sub_not S9 by Def26;
A2: 'not' (S9 `1) is negative by QC_LANG1:def_19;
 S `1 = 'not' (S9 `1) by A1, MCART_1:7;
then A3: len (@ (the_argument_of ('not' (S9 `1)))) < len (@ (S `1)) by A2, QC_LANG1:14;
 (Sub_the_argument_of S) `1 = S9 `1 by A1, Def30;
hence  len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:1; ::_thesis: verum
end;

theorem Th23: :: SUBSTUT1:23
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_conjunctive implies ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) )
assume  S is Sub_conjunctive ; ::_thesis: ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
then consider S1, S2 being Element of QC-Sub-WFF A such that
A1: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by Def27;
 S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, Def21;
then A2: S `1 = (S1 `1) '&' (S2 `1) by MCART_1:7;
 (S1 `1) '&' (S2 `1) is conjunctive by QC_LANG1:def_20;
then A3: ( len (@ (the_left_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) & len (@ (the_right_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) ) by A2, QC_LANG1:15;
 ( (Sub_the_right_argument_of S) `1 = S2 `1 & (Sub_the_left_argument_of S) `1 = S1 `1 ) by A1, Th18, Th19;
hence  ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) by A3, QC_LANG2:4; ::_thesis: verum
end;

theorem Th24: :: SUBSTUT1:24
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_universal holds
len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_universal implies len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) )
assume  S is Sub_universal ; ::_thesis: len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))
then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A1: ( S = Sub_All (B,SQ) & B is quantifiable ) by Def28;
 S = [(All ((B `2),((B `1) `1))),SQ] by A1, Def24;
then A2: S `1 = All ((B `2),((B `1) `1)) by MCART_1:7;
 All ((B `2),((B `1) `1)) is universal by QC_LANG1:def_21;
then A3: len (@ (the_scope_of (All ((B `2),((B `1) `1))))) < len (@ (S `1)) by A2, QC_LANG1:16;
 (Sub_the_scope_of S) `1 = (B `1) `1 by A1, Th21;
hence  len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:7; ::_thesis: verum
end;

theorem Th25: :: SUBSTUT1:25
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
let S be Element of QC-Sub-WFF A; ::_thesis: ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
thus  ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) ::_thesis: ( ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume  S is A -Sub_VERUM ; ::_thesis: ((@ (S `1)) . 1) `1 = 0
then  ex e being Element of vSUB A st S = [(VERUM A),e] by Def19;
then  S `1 = VERUM A by MCART_1:7;
hence ((@ (S `1)) . 1) `1 = [0,0] `1 by FINSEQ_1:def_8
.= 0 ;
::_thesis: verum
end;
thus  ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) ::_thesis: ( ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume  S is Sub_atomic ; ::_thesis: ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A
then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that
A1: S = Sub_P (P,ll,e) by Def25;
 S = [(P ! ll),e] by A1, Th9;
then  S `1 = P ! ll by MCART_1:7;
then  @ (S `1) = <*P*> ^ ll by QC_LANG1:8;
then  (@ (S `1)) . 1 = P by FINSEQ_1:41;
hence  ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ; ::_thesis: verum
end;
thus  ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) ::_thesis: ( ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume  S is Sub_negative ; ::_thesis: ((@ (S `1)) . 1) `1 = 1
then consider S9 being Element of QC-Sub-WFF A such that
A2: S = Sub_not S9 by Def26;
 S `1 = 'not' (S9 `1) by A2, MCART_1:7;
then  (@ (S `1)) . 1 = [1,0] by FINSEQ_1:41;
hence  ((@ (S `1)) . 1) `1 = 1 by MCART_1:7; ::_thesis: verum
end;
thus  ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) ::_thesis: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 )
proof
assume  S is Sub_conjunctive ; ::_thesis: ((@ (S `1)) . 1) `1 = 2
then consider S1, S2 being Element of QC-Sub-WFF A such that
A3: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by Def27;
 S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A3, Def21;
then  S `1 = (S1 `1) '&' (S2 `1) by MCART_1:7;
then  @ (S `1) = <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (S2 `1))) by FINSEQ_1:32;
then  (@ (S `1)) . 1 = [2,0] by FINSEQ_1:41;
hence  ((@ (S `1)) . 1) `1 = 2 by MCART_1:7; ::_thesis: verum
end;
thus  ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) ::_thesis: verum
proof
assume  S is Sub_universal ; ::_thesis: ((@ (S `1)) . 1) `1 = 3
then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A4: ( S = Sub_All (B,SQ) & B is quantifiable ) by Def28;
 S = [(All ((B `2),((B `1) `1))),SQ] by A4, Def24;
then  S `1 = All ((B `2),((B `1) `1)) by MCART_1:7;
then  @ (S `1) = <*[3,0]*> ^ (<*(B `2)*> ^ (@ ((B `1) `1))) by FINSEQ_1:32;
then  (@ (S `1)) . 1 = [3,0] by FINSEQ_1:41;
hence  ((@ (S `1)) . 1) `1 = 3 by MCART_1:7; ::_thesis: verum
end;
end;

theorem Th26: :: SUBSTUT1:26
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 )
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 )
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_atomic implies ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) )
assume  S is Sub_atomic ; ::_thesis: ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 )
then  ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A by Th25;
hence  ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) by QC_LANG1:17; ::_thesis: verum
end;

theorem Th27: :: SUBSTUT1:27
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds
( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )
let S be Element of QC-Sub-WFF A; ::_thesis: ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )
A1: ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) by Th25;
A2: ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) by Th25;
A3: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) by Th25;
 ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) by Th25;
hence  ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) by A1, A2, A3, Th26; ::_thesis: verum
end;

scheme :: SUBSTUT1:sch 3
SubFuncEx{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4( Element of QC-Sub-WFF F1()) ->  Element of F2(), F5( Element of F2()) ->  Element of F2(), F6( Element of F2(), Element of F2()) ->  Element of F2(), F7( set , Element of QC-Sub-WFF F1(), Element of F2()) ->  Element of F2() } :
 ex F being Function of (QC-Sub-WFF F1()),F2() st
for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
proof
defpred S1[ Function of (QC-Sub-WFF F1()),F2(), Element of NAT ] means  for S being Element of QC-Sub-WFF F1() st len (@ (S `1)) <= $2 holds
( ( S is F1() -Sub_VERUM implies $1 . S = F3() ) & ( S is Sub_atomic implies $1 . S = F4(S) ) & ( S is Sub_negative implies $1 . S = F5(($1 . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies $1 . S = F6(($1 . (Sub_the_left_argument_of S)),($1 . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies $1 . S = F7(F1(),S,($1 . (Sub_the_scope_of S))) ) );
defpred S2[ Element of F2(), Function of (QC-Sub-WFF F1()),F2(), Element of QC-Sub-WFF F1()] means ( ( $3 is F1() -Sub_VERUM implies $1 = F3() ) & ( $3 is Sub_atomic implies $1 = F4($3) ) & ( $3 is Sub_negative implies $1 = F5(($2 . (Sub_the_argument_of $3))) ) & ( $3 is Sub_conjunctive implies $1 = F6(($2 . (Sub_the_left_argument_of $3)),($2 . (Sub_the_right_argument_of $3))) ) & ( $3 is Sub_universal implies $1 = F7(F1(),$3,($2 . (Sub_the_scope_of $3))) ) );
defpred S3[ Element of NAT ] means  ex F being Function of (QC-Sub-WFF F1()),F2() st S1[F,$1];
defpred S4[ set , set ] means  ex S being Element of QC-Sub-WFF F1() st
( S = $1 & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds
$2 = g . S ) );
A1: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
given F being Function of (QC-Sub-WFF F1()),F2() such that A2: S1[F,n] ; ::_thesis: S3[n + 1]
defpred S5[ Element of QC-Sub-WFF F1(), Element of F2()] means ( ( len (@ ($1 `1)) <> n + 1 implies $2 = F . $1 ) & ( len (@ ($1 `1)) = n + 1 implies S2[$2,F,$1] ) );
A3: for S being Element of QC-Sub-WFF F1() ex y being Element of F2() st S5[S,y]
proof
let S be Element of QC-Sub-WFF F1(); ::_thesis: ex y being Element of F2() st S5[S,y]
now__::_thesis:_(_(_len_(@_(S_`1))_<>_n_+_1_&_ex_y_being_Element_of_F2()_st_y_=_F_._S_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_F1()_-Sub_VERUM_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_atomic_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_negative_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_conjunctive_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_universal_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_)
percases ( len (@ (S `1)) <> n + 1 or ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) or ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) or ( len (@ (S `1)) = n + 1 & S is Sub_negative ) or ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) or ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ) by Th12;
case len (@ (S `1)) <> n + 1 ; ::_thesis: ex y being Element of F2() st y = F . S
take y = F . S; ::_thesis: y = F . S
thus  y = F . S ; ::_thesis: verum
end;
caseA4: ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S]
take y = F3(); ::_thesis: S2[y,F,S]
thus  S2[y,F,S] by A4, Th27; ::_thesis: verum
end;
caseA5: ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S]
take y = F4(S); ::_thesis: S2[y,F,S]
thus  S2[y,F,S] by A5, Th27; ::_thesis: verum
end;
caseA6: ( len (@ (S `1)) = n + 1 & S is Sub_negative ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S]
take y = F5((F . (Sub_the_argument_of S))); ::_thesis: S2[y,F,S]
thus  S2[y,F,S] by A6, Th27; ::_thesis: verum
end;
caseA7: ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S]
take y = F6((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))); ::_thesis: S2[y,F,S]
thus  S2[y,F,S] by A7, Th27; ::_thesis: verum
end;
caseA8: ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S]
take y = F7(F1(),S,(F . (Sub_the_scope_of S))); ::_thesis: S2[y,F,S]
thus  S2[y,F,S] by A8, Th27; ::_thesis: verum
end;
end;
end;
hence  ex y being Element of F2() st S5[S,y] ; ::_thesis: verum
end;
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A9: for S being Element of QC-Sub-WFF F1() holds S5[S,G . S] from FUNCT_2:sch_3(A3);
take H = G; ::_thesis: S1[H,n + 1]
thus  S1[H,n + 1] ::_thesis: verum
proof
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S `1)) <= n + 1 implies ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) )
assume A10: len (@ (S `1)) <= n + 1 ; ::_thesis: ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
thus  ( S is F1() -Sub_VERUM implies H . S = F3() ) ::_thesis: ( ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
now__::_thesis:_(_S_is_F1()_-Sub_VERUM_implies_H_._S_=_F3()_)
percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; ::_thesis: ( S is F1() -Sub_VERUM implies H . S = F3() )
then  ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence  ( S is F1() -Sub_VERUM implies H . S = F3() ) by A2; ::_thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; ::_thesis: ( S is F1() -Sub_VERUM implies H . S = F3() )
hence  ( S is F1() -Sub_VERUM implies H . S = F3() ) by A9; ::_thesis: verum
end;
end;
end;
hence  ( S is F1() -Sub_VERUM implies H . S = F3() ) ; ::_thesis: verum
end;
thus  ( S is Sub_atomic implies H . S = F4(S) ) ::_thesis: ( ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
now__::_thesis:_(_S_is_Sub_atomic_implies_H_._S_=_F4(S)_)
percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; ::_thesis: ( S is Sub_atomic implies H . S = F4(S) )
then  ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence  ( S is Sub_atomic implies H . S = F4(S) ) by A2; ::_thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; ::_thesis: ( S is Sub_atomic implies H . S = F4(S) )
hence  ( S is Sub_atomic implies H . S = F4(S) ) by A9; ::_thesis: verum
end;
end;
end;
hence  ( S is Sub_atomic implies H . S = F4(S) ) ; ::_thesis: verum
end;
thus  ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) ::_thesis: ( ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
assume A11: S is Sub_negative ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S)))
then  len (@ ((Sub_the_argument_of S) `1)) <> n + 1 by A10, Th22;
then A12: H . (Sub_the_argument_of S) = F . (Sub_the_argument_of S) by A9;
now__::_thesis:_H_._S_=_F5((H_._(Sub_the_argument_of_S)))
percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S)))
then  ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence  H . S = F5((H . (Sub_the_argument_of S))) by A2, A11, A12; ::_thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S)))
hence  H . S = F5((H . (Sub_the_argument_of S))) by A9, A11, A12; ::_thesis: verum
end;
end;
end;
hence  H . S = F5((H . (Sub_the_argument_of S))) ; ::_thesis: verum
end;
thus  ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) ::_thesis: ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) )
proof
assume A13: S is Sub_conjunctive ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
then  len (@ ((Sub_the_right_argument_of S) `1)) <> n + 1 by A10, Th23;
then A14: H . (Sub_the_right_argument_of S) = F . (Sub_the_right_argument_of S) by A9;
 len (@ ((Sub_the_left_argument_of S) `1)) <> n + 1 by A10, A13, Th23;
then A15: H . (Sub_the_left_argument_of S) = F . (Sub_the_left_argument_of S) by A9;
now__::_thesis:_H_._S_=_F6((H_._(Sub_the_left_argument_of_S)),(H_._(Sub_the_right_argument_of_S)))
percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
then  ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence  H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) by A2, A13, A15, A14; ::_thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
hence  H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) by A9, A13, A15, A14; ::_thesis: verum
end;
end;
end;
hence  H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ; ::_thesis: verum
end;
thus  ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ::_thesis: verum
proof
assume A16: S is Sub_universal ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
then  len (@ ((Sub_the_scope_of S) `1)) <> n + 1 by A10, Th24;
then A17: H . (Sub_the_scope_of S) = F . (Sub_the_scope_of S) by A9;
now__::_thesis:_H_._S_=_F7(F1(),S,(H_._(Sub_the_scope_of_S)))
percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
then  ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence  H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A2, A16, A17; ::_thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
hence  H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A9, A16, A17; ::_thesis: verum
end;
end;
end;
hence  H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ; ::_thesis: verum
end;
end;
end;
A18: S3[ 0 ]
proof
set F = the Function of (QC-Sub-WFF F1()),F2();
take  the Function of (QC-Sub-WFF F1()),F2() ; ::_thesis: S1[ the Function of (QC-Sub-WFF F1()),F2(), 0 ]
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S `1)) <= 0 implies ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) )
assume  len (@ (S `1)) <= 0 ; ::_thesis: ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) )
hence  ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) by QC_LANG1:10; ::_thesis: verum
end;
A19: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A18, A1);
A20: for x being set st x in QC-Sub-WFF F1() holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in QC-Sub-WFF F1() implies ex y being set st S4[x,y] )
assume  x in QC-Sub-WFF F1() ; ::_thesis: ex y being set st S4[x,y]
then reconsider x9 = x as Element of QC-Sub-WFF F1() ;
consider F being Function of (QC-Sub-WFF F1()),F2() such that
A21: S1[F, len (@ (x9 `1))] by A19;
take  F . x ; ::_thesis: S4[x,F . x]
take  x9 ; ::_thesis: ( x9 = x & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds
F . x = g . x9 ) )
thus  x9 = x ; ::_thesis: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds
F . x = g . x9
let G be Function of (QC-Sub-WFF F1()),F2(); ::_thesis: ( S1[G, len (@ (x9 `1))] implies F . x = G . x9 )
assume A22: S1[G, len (@ (x9 `1))] ; ::_thesis: F . x = G . x9
defpred S5[ Element of QC-Sub-WFF F1()] means ( len (@ ($1 `1)) <= len (@ (x9 `1)) implies F . $1 = G . $1 );
A23: now__::_thesis:_for_S_being_Element_of_QC-Sub-WFF_F1()_holds_
(_(_S_is_Sub_atomic_implies_S5[S]_)_&_(_S_is_F1()_-Sub_VERUM_implies_S5[S]_)_&_(_S_is_Sub_negative_&_S5[_Sub_the_argument_of_S]_implies_S5[S]_)_&_(_S_is_Sub_conjunctive_&_S5[_Sub_the_left_argument_of_S]_&_S5[_Sub_the_right_argument_of_S]_implies_S5[S]_)_&_(_S_is_Sub_universal_&_S5[_Sub_the_scope_of_S]_implies_S5[S]_)_)
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( ( S is Sub_atomic implies S5[S] ) & ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
thus  ( S is Sub_atomic implies S5[S] ) ::_thesis: ( ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume A24: ( S is Sub_atomic & len (@ (S `1)) <= len (@ (x9 `1)) ) ; ::_thesis: F . S = G . S
hence F . S = F4(S) by A21
.= G . S by A22, A24 ;
::_thesis: verum
end;
thus  ( S is F1() -Sub_VERUM implies S5[S] ) ::_thesis: ( ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume A25: ( S is F1() -Sub_VERUM & len (@ (S `1)) <= len (@ (x9 `1)) ) ; ::_thesis: F . S = G . S
hence F . S = F3() by A21
.= G . S by A22, A25 ;
::_thesis: verum
end;
thus  ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) ::_thesis: ( ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume that
A26: S is Sub_negative and
A27: S5[ Sub_the_argument_of S] and
A28: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S
 len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A26, Th22;
hence F . S = F5((G . (Sub_the_argument_of S))) by A21, A26, A27, A28, XXREAL_0:2
.= G . S by A22, A26, A28 ;
::_thesis: verum
end;
thus  ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) ::_thesis: ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] )
proof
assume that
A29: S is Sub_conjunctive and
A30: ( S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] ) and
A31: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S
 ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) by A29, Th23;
hence F . S = F6((G . (Sub_the_left_argument_of S)),(G . (Sub_the_right_argument_of S))) by A21, A29, A30, A31, XXREAL_0:2
.= G . S by A22, A29, A31 ;
::_thesis: verum
end;
thus  ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ::_thesis: verum
proof
assume that
A32: S is Sub_universal and
A33: S5[ Sub_the_scope_of S] and
A34: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S
 len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A32, Th24;
hence F . S = F7(F1(),S,(G . (Sub_the_scope_of S))) by A21, A32, A33, A34, XXREAL_0:2
.= G . S by A22, A32, A34 ;
::_thesis: verum
end;
end;
 for S being Element of QC-Sub-WFF F1() holds S5[S] from SUBSTUT1:sch_2(A23);
hence  F . x = G . x9 ; ::_thesis: verum
end;
consider F being Function such that
A35: dom F = QC-Sub-WFF F1() and
A36: for x being set st x in QC-Sub-WFF F1() holds
S4[x,F . x] from CLASSES1:sch_1(A20);
 rng F c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in F2() )
assume  y in rng F ; ::_thesis: y in F2()
then consider x being set  such that
A37: ( x in QC-Sub-WFF F1() & y = F . x ) by A35, FUNCT_1:def_3;
consider S being Element of QC-Sub-WFF F1() such that
 S = x and
A38: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds
y = g . S by A36, A37;
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A39: S1[G, len (@ (S `1))] by A19;
 y = G . S by A38, A39;
hence  y in F2() ; ::_thesis: verum
end;
then reconsider F = F as Function of (QC-Sub-WFF F1()),F2() by A35, FUNCT_2:def_1, RELSET_1:4;
take  F ; ::_thesis: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
let S be Element of QC-Sub-WFF F1(); ::_thesis: for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
consider S1 being Element of QC-Sub-WFF F1() such that
A40: S1 = S and
A41: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . S = g . S1 by A36;
let d1, d2 be Element of F2(); ::_thesis: ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A42: S1[G, len (@ (S1 `1))] by A19;
set S9 = Sub_the_scope_of S;
A43: ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_scope_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_scope_of S) = g . S1 ) ) by A36;
A44: F . S = G . S by A40, A41, A42;
hence  ( S is F1() -Sub_VERUM implies F . S = F3() ) by A40, A42; ::_thesis: ( ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
thus  ( S is Sub_atomic implies F . S = F4(S) ) by A40, A42, A44; ::_thesis: ( ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
A45: for k being Element of NAT st k < len (@ (S `1)) holds
S1[G,k]
proof
let k be Element of NAT ; ::_thesis: ( k < len (@ (S `1)) implies S1[G,k] )
assume A46: k < len (@ (S `1)) ; ::_thesis: S1[G,k]
let S9 be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S9 `1)) <= k implies ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) )
assume  len (@ (S9 `1)) <= k ; ::_thesis: ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) )
then  len (@ (S9 `1)) <= len (@ (S `1)) by A46, XXREAL_0:2;
hence  ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) by A40, A42; ::_thesis: verum
end;
thus  ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) ::_thesis: ( ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
proof
set S9 = Sub_the_argument_of S;
set k = len (@ ((Sub_the_argument_of S) `1));
A47: ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_argument_of S) = g . S1 ) ) by A36;
assume A48: S is Sub_negative ; ::_thesis: ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) )
then  len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by Th22;
then  S1[G, len (@ ((Sub_the_argument_of S) `1))] by A45;
then  F . (Sub_the_argument_of S) = G . (Sub_the_argument_of S) by A47;
hence  ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) ) by A40, A42, A44, A48; ::_thesis: verum
end;
thus  ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) ::_thesis: ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) )
proof
set S99 = Sub_the_right_argument_of S;
set S9 = Sub_the_left_argument_of S;
set k9 = len (@ ((Sub_the_left_argument_of S) `1));
set k99 = len (@ ((Sub_the_right_argument_of S) `1));
A49: ex S2 being Element of QC-Sub-WFF F1() st
( S2 = Sub_the_right_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S2 `1))] holds
F . (Sub_the_right_argument_of S) = g . S2 ) ) by A36;
assume A50: S is Sub_conjunctive ; ::_thesis: ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) )
then  len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) by Th23;
then A51: S1[G, len (@ ((Sub_the_left_argument_of S) `1))] by A45;
 len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) by A50, Th23;
then  S1[G, len (@ ((Sub_the_right_argument_of S) `1))] by A45;
then A52: F . (Sub_the_right_argument_of S) = G . (Sub_the_right_argument_of S) by A49;
 ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_left_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_left_argument_of S) = g . S1 ) ) by A36;
then  F . (Sub_the_left_argument_of S) = G . (Sub_the_left_argument_of S) by A51;
hence  ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) ) by A40, A42, A44, A50, A52; ::_thesis: verum
end;
set k = len (@ ((Sub_the_scope_of S) `1));
assume A53: S is Sub_universal ; ::_thesis: ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) )
then  len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by Th24;
then  S1[G, len (@ ((Sub_the_scope_of S) `1))] by A45;
then  F . (Sub_the_scope_of S) = G . (Sub_the_scope_of S) by A43;
hence  ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) ) by A40, A42, A44, A53; ::_thesis: verum
end;

scheme :: SUBSTUT1:sch 4
SubQCFuncUniq{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Function of (QC-Sub-WFF F1()),F2(), F4() ->  Function of (QC-Sub-WFF F1()),F2(), F5() ->  Element of F2(), F6( set ) ->  Element of F2(), F7( set ) ->  Element of F2(), F8( set , set ) ->  Element of F2(), F9( set , set , set ) ->  Element of F2() } :
 F3() = F4()
provided
A1: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F3() . S = F5() ) & ( S is Sub_atomic implies F3() . S = F6(S) ) & ( S is Sub_negative & d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F3() . (Sub_the_left_argument_of S) & d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F3() . (Sub_the_scope_of S) implies F3() . S = F9(F1(),S,d1) ) ) and
A2: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F4() . S = F5() ) & ( S is Sub_atomic implies F4() . S = F6(S) ) & ( S is Sub_negative & d1 = F4() . (Sub_the_argument_of S) implies F4() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F4() . (Sub_the_left_argument_of S) & d2 = F4() . (Sub_the_right_argument_of S) implies F4() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F4() . (Sub_the_scope_of S) implies F4() . S = F9(F1(),S,d1) ) )
proof
defpred S1[ Element of QC-Sub-WFF F1()] means F3() . $1 = F4() . $1;
A3: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]
let P be QC-pred_symbol of k,F1(); ::_thesis: for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]
let l be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]
let e be Element of vSUB F1(); ::_thesis: S1[ Sub_P (P,l,e)]
thus F3() . (Sub_P (P,l,e)) = F6((Sub_P (P,l,e))) by A1
.= F4() . (Sub_P (P,l,e)) by A2 ; ::_thesis: verum
end;
A4: for x being bound_QC-variable of F1()
for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
proof
let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] )
assume that
A5: [S,x] is quantifiable and
A6: F3() . S = F4() . S ; ::_thesis: S1[ Sub_All ([S,x],SQ)]
A7: Sub_All ([S,x],SQ) is Sub_universal by A5, Th14;
 Sub_the_scope_of (Sub_All ([S,x],SQ)) = [S,x] `1 by A5, Th21;
then  Sub_the_scope_of (Sub_All ([S,x],SQ)) = S ;
hence F3() . (Sub_All ([S,x],SQ)) = F9(F1(),(Sub_All ([S,x],SQ)),(F4() . (Sub_the_scope_of (Sub_All ([S,x],SQ))))) by A1, A6, A7
.= F4() . (Sub_All ([S,x],SQ)) by A2, A7 ;
::_thesis: verum
end;
A8: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
S1[S]
proof
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S is F1() -Sub_VERUM implies S1[S] )
assume A9: S is F1() -Sub_VERUM ; ::_thesis: S1[S]
then  F3() . S = F5() by A1;
hence  S1[S] by A2, A9; ::_thesis: verum
end;
A10: for S1, S2 being Element of QC-Sub-WFF F1() st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds
S1[ Sub_& (S1,S2)]
proof
let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & S1[S1] & S1[S2] implies S1[ Sub_& (S1,S2)] )
assume that
A11: S1 `2 = S2 `2 and
A12: ( F3() . S1 = F4() . S1 & F3() . S2 = F4() . S2 ) ; ::_thesis: S1[ Sub_& (S1,S2)]
A13: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A11, Th19;
A14: ( Sub_& (S1,S2) is Sub_conjunctive & Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 ) by A11, Th13, Th18;
hence F3() . (Sub_& (S1,S2)) = F8((F4() . S1),(F4() . S2)) by A1, A12, A13
.= F4() . (Sub_& (S1,S2)) by A2, A14, A13 ;
::_thesis: verum
end;
A15: for S being Element of QC-Sub-WFF F1() st S1[S] holds
S1[ Sub_not S]
proof
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S1[S] implies S1[ Sub_not S] )
assume A16: F3() . S = F4() . S ; ::_thesis: S1[ Sub_not S]
A17: Sub_the_argument_of (Sub_not S) = S by Def30;
hence F3() . (Sub_not S) = F7((F4() . S)) by A1, A16
.= F4() . (Sub_not S) by A2, A17 ;
::_thesis: verum
end;
 for S being Element of QC-Sub-WFF F1() holds S1[S] from SUBSTUT1:sch_1(A3, A8, A15, A10, A4);
hence  F3() = F4() by FUNCT_2:63; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
func @ S ->  Element of [:(QC-WFF A),(vSUB A):] equals :: SUBSTUT1:def 35
S;
coherence
 S is Element of [:(QC-WFF A),(vSUB A):]
proof
 ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8;
hence  S is Element of [:(QC-WFF A),(vSUB A):] ; ::_thesis: verum
end;
end;

:: deftheorem  defines @ SUBSTUT1:def_35_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds @ S = S;

definition
let A be QC-alphabet ;
let Z be Element of [:(QC-WFF A),(vSUB A):];
:: original: `1
redefine funcZ `1  ->  Element of QC-WFF A;
coherence
 Z `1 is Element of QC-WFF A
proof
 ex a, b being set st
( a in QC-WFF A & b in vSUB A & [a,b] = Z ) by ZFMISC_1:def_2;
hence  Z `1 is Element of QC-WFF A by MCART_1:7; ::_thesis: verum
end;
:: original: `2
redefine funcZ `2  ->  CQC_Substitution of A;
coherence
 Z `2 is CQC_Substitution of A
proof
 ex a, b being set st
( a in QC-WFF A & b in vSUB A & [a,b] = Z ) by ZFMISC_1:def_2;
hence  Z `2 is CQC_Substitution of A by MCART_1:7; ::_thesis: verum
end;
end;

definition
let A be QC-alphabet ;
let Z be Element of [:(QC-WFF A),(vSUB A):];
func S_Bound Z ->  bound_QC-variable of A equals :: SUBSTUT1:def 36
 x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) if  bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2)))
otherwise  bound_in (Z `1);
coherence
 ( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) is bound_QC-variable of A ) & ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies bound_in (Z `1) is bound_QC-variable of A ) ) ;
consistency
 for b1 being bound_QC-variable of A holds verum ;
end;

:: deftheorem  defines S_Bound SUBSTUT1:def_36_:_
 for A being QC-alphabet
for Z being Element of [:(QC-WFF A),(vSUB A):] holds
( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) ) & ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = bound_in (Z `1) ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
let p be QC-formula of A;
func Quant (S,p) ->  Element of QC-WFF A equals :: SUBSTUT1:def 37
 All ((S_Bound (@ S)),p);
coherence
 All ((S_Bound (@ S)),p) is Element of QC-WFF A ;
end;

:: deftheorem  defines Quant SUBSTUT1:def_37_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A
for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p);

Lm6:  for A being QC-alphabet
for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) holds
F1 = F2
proof
let A be QC-alphabet ; ::_thesis: for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) holds
F1 = F2
let F1, F2 be Function of (QC-Sub-WFF A),(QC-WFF A); ::_thesis: ( ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) implies F1 = F2 )
deffunc H1( Element of QC-WFF A, Element of QC-WFF A) ->  Element of QC-WFF A = $1 '&' $2;
deffunc H2( Element of QC-WFF A) ->  Element of QC-WFF A = 'not' $1;
deffunc H3( Element of QC-Sub-WFF A) ->  Element of QC-WFF A = (the_pred_symbol_of ($1 `1)) ! (CQC_Subst ((Sub_the_arguments_of $1),($1 `2)));
assume  for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = H3(S) ) & ( S is Sub_negative implies F1 . S = H2(F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = H1(F1 . (Sub_the_left_argument_of S),F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ; ::_thesis: ( ex S being Element of QC-Sub-WFF A st
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) implies ( S is Sub_universal & not F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) or F1 = F2 )
then A1: for S being Element of QC-Sub-WFF A
for d1, d2 being Element of QC-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = H3(S) ) & ( S is Sub_negative & d1 = F1 . (Sub_the_argument_of S) implies F1 . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F1 . (Sub_the_left_argument_of S) & d2 = F1 . (Sub_the_right_argument_of S) implies F1 . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F1 . (Sub_the_scope_of S) implies F1 . S = Quant (S,d1) ) ) ;
assume  for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = H3(S) ) & ( S is Sub_negative implies F2 . S = H2(F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = H1(F2 . (Sub_the_left_argument_of S),F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ; ::_thesis: F1 = F2
then A2: for S being Element of QC-Sub-WFF A
for d1, d2 being Element of QC-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = H3(S) ) & ( S is Sub_negative & d1 = F2 . (Sub_the_argument_of S) implies F2 . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F2 . (Sub_the_left_argument_of S) & d2 = F2 . (Sub_the_right_argument_of S) implies F2 . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F2 . (Sub_the_scope_of S) implies F2 . S = Quant (S,d1) ) ) ;
thus  F1 = F2 from SUBSTUT1:sch_4(A1, A2); ::_thesis: verum
end;

begin

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
func CQC_Sub S ->  Element of QC-WFF A means :Def38: :: SUBSTUT1:def 38
 ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( it = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) );
existence
 ex b1 being Element of QC-WFF A ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b1 = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )
proof
deffunc H1( Element of QC-WFF A, Element of QC-WFF A) ->  Element of QC-WFF A = $1 '&' $2;
deffunc H2( Element of QC-WFF A) ->  Element of QC-WFF A = 'not' $1;
deffunc H3( Element of QC-Sub-WFF A) ->  Element of QC-WFF A = (the_pred_symbol_of ($1 `1)) ! (CQC_Subst ((Sub_the_arguments_of $1),($1 `2)));
consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A1: for S being Element of QC-Sub-WFF A
for d1, d2 being Element of QC-WFF A holds
( ( S is A -Sub_VERUM implies F . S = VERUM A ) & ( S is Sub_atomic implies F . S = H3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = Quant (S,d1) ) ) from SUBSTUT1:sch_3();
take  F . S ; ::_thesis: ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( F . S = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )
take  F ; ::_thesis: ( F . S = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )
thus  F . S = F . S ; ::_thesis: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) )
thus  for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b1 = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) & ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b2 = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) holds
b1 = b2 by Lm6;
end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def_38_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A
for b3 being Element of QC-WFF A holds
( b3 = CQC_Sub S iff ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b3 = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) );

theorem Th28: :: SUBSTUT1:28
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_negative holds
CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_negative implies CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) )
consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A1: CQC_Sub S = F . S and
A2: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) by Def38;
consider G being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A3: CQC_Sub (Sub_the_argument_of S) = G . (Sub_the_argument_of S) and
A4: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies G . S9 = VERUM A ) & ( S9 is Sub_atomic implies G . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies G . S9 = 'not' (G . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies G . S9 = (G . (Sub_the_left_argument_of S9)) '&' (G . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies G . S9 = Quant (S9,(G . (Sub_the_scope_of S9))) ) ) by Def38;
 F = G by A2, A4, Lm6;
hence  ( S is Sub_negative implies CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) ) by A1, A2, A3; ::_thesis: verum
end;

theorem Th29: :: SUBSTUT1:29
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
let S be Element of QC-Sub-WFF A; ::_thesis: CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
set 9S = Sub_not S;
 Sub_the_argument_of (Sub_not S) = S by Def30;
hence  CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th28; ::_thesis: verum
end;

theorem Th30: :: SUBSTUT1:30
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S))
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S))
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) )
consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A1: CQC_Sub S = F . S and
A2: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) by Def38;
consider F2 being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A3: CQC_Sub (Sub_the_right_argument_of S) = F2 . (Sub_the_right_argument_of S) and
A4: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F2 . S9 = VERUM A ) & ( S9 is Sub_atomic implies F2 . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F2 . S9 = 'not' (F2 . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F2 . S9 = (F2 . (Sub_the_left_argument_of S9)) '&' (F2 . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F2 . S9 = Quant (S9,(F2 . (Sub_the_scope_of S9))) ) ) by Def38;
A5: F2 = F by A2, A4, Lm6;
consider F1 being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A6: CQC_Sub (Sub_the_left_argument_of S) = F1 . (Sub_the_left_argument_of S) and
A7: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F1 . S9 = VERUM A ) & ( S9 is Sub_atomic implies F1 . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F1 . S9 = 'not' (F1 . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F1 . S9 = (F1 . (Sub_the_left_argument_of S9)) '&' (F1 . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F1 . S9 = Quant (S9,(F1 . (Sub_the_scope_of S9))) ) ) by Def38;
 F1 = F by A2, A7, Lm6;
hence  ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) ) by A1, A2, A6, A3, A5; ::_thesis: verum
end;

theorem Th31: :: SUBSTUT1:31
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
proof
let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) )
set S = Sub_& (S1,S2);
assume A1: S1 `2 = S2 `2 ; ::_thesis: CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
then  ( Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 & Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 ) by Th18, Th19;
hence  CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) by A1, Th13, Th30; ::_thesis: verum
end;

theorem Th32: :: SUBSTUT1:32
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_universal holds
CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) )
consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A1: CQC_Sub S = F . S and
A2: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) by Def38;
consider G being Function of (QC-Sub-WFF A),(QC-WFF A) such that
A3: CQC_Sub (Sub_the_scope_of S) = G . (Sub_the_scope_of S) and
A4: for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies G . S9 = VERUM A ) & ( S9 is Sub_atomic implies G . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies G . S9 = 'not' (G . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies G . S9 = (G . (Sub_the_left_argument_of S9)) '&' (G . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies G . S9 = Quant (S9,(G . (Sub_the_scope_of S9))) ) ) by Def38;
 F = G by A2, A4, Lm6;
hence  ( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) ) by A1, A2, A3; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
func CQC-Sub-WFF A ->  Subset of (QC-Sub-WFF A) equals :: SUBSTUT1:def 39
 {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  ;
coherence
  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  is Subset of (QC-Sub-WFF A)
proof
set X =  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  ;
  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  c= QC-Sub-WFF A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  or a in QC-Sub-WFF A )
assume  a in  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  ; ::_thesis: a in QC-Sub-WFF A
then  ex S being Element of QC-Sub-WFF A st
( a = S & S `1 is Element of CQC-WFF A ) ;
hence  a in QC-Sub-WFF A ; ::_thesis: verum
end;
hence   {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  is Subset of (QC-Sub-WFF A) ; ::_thesis: verum
end;
end;

:: deftheorem  defines CQC-Sub-WFF SUBSTUT1:def_39_:_
 for A being QC-alphabet holds CQC-Sub-WFF A =  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  ;

registration
let A be QC-alphabet ;
cluster CQC-Sub-WFF A ->  non empty ;
coherence
 not CQC-Sub-WFF A is empty
proof
set e = the Element of vSUB A;
reconsider S = [(VERUM A), the Element of vSUB A] as Element of QC-Sub-WFF A by Def16;
 S `1 = VERUM A by MCART_1:7;
then  [(VERUM A), the Element of vSUB A] in CQC-Sub-WFF A ;
hence  not CQC-Sub-WFF A is empty ; ::_thesis: verum
end;
end;

theorem Th33: :: SUBSTUT1:33
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds
CQC_Sub S is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds
CQC_Sub S is Element of CQC-WFF A
let S be Element of QC-Sub-WFF A; ::_thesis: ( S is A -Sub_VERUM implies CQC_Sub S is Element of CQC-WFF A )
assume A1: S is A -Sub_VERUM ; ::_thesis: CQC_Sub S is Element of CQC-WFF A
 ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( CQC_Sub S = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) by Def38;
hence  CQC_Sub S is Element of CQC-WFF A by A1; ::_thesis: verum
end;

Lm7:  for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P
let P be QC-pred_symbol of k,A; ::_thesis: for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P
let ll be CQC-variable_list of k,A; ::_thesis: the_pred_symbol_of (P ! ll) = P
A1: (<*P*> ^ ll) . 1 = P by FINSEQ_1:41;
 P ! ll is atomic by QC_LANG1:def_18;
then consider k being Element of NAT , ll9 being QC-variable_list of k,A, P9 being QC-pred_symbol of k,A such that
A2: ( the_pred_symbol_of (P ! ll) = P9 & P ! ll = P9 ! ll9 ) by QC_LANG1:def_22;
 ( P ! ll = <*P*> ^ ll & P9 ! ll9 = <*P9*> ^ ll9 ) by QC_LANG1:8;
hence  the_pred_symbol_of (P ! ll) = P by A2, A1, FINSEQ_1:41; ::_thesis: verum
end;

theorem Th34: :: SUBSTUT1:34
for A being QC-alphabet
for k being Element of NAT
for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
let k be Element of NAT ; ::_thesis: for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
let h be FinSequence; ::_thesis: ( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )
thus  ( h is CQC-variable_list of k,A implies ( h is FinSequence of bound_QC-variables A & len h = k ) ) ::_thesis: ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A )
proof
assume A1: h is CQC-variable_list of k,A ; ::_thesis: ( h is FinSequence of bound_QC-variables A & len h = k )
then  rng h c= bound_QC-variables A by RELAT_1:def_19;
hence  h is FinSequence of bound_QC-variables A by FINSEQ_1:def_4; ::_thesis: len h = k
thus  len h = k by A1, CARD_1:def_7; ::_thesis: verum
end;
thus  ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A ) ::_thesis: verum
proof
assume that
A2: h is FinSequence of bound_QC-variables A and
A3: len h = k ; ::_thesis: h is CQC-variable_list of k,A
 rng h c= bound_QC-variables A by A2, FINSEQ_1:def_4;
then  rng h c= QC-variables A by XBOOLE_1:1;
hence  h is CQC-variable_list of k,A by A2, A3, CARD_1:def_7, FINSEQ_1:def_4; ::_thesis: verum
end;
end;

theorem Th35: :: SUBSTUT1:35
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
let P be QC-pred_symbol of k,A; ::_thesis: for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
let ll be CQC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
let e be Element of vSUB A; ::_thesis: CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
set l = Sub_the_arguments_of (Sub_P (P,ll,e));
A1: Sub_the_arguments_of (Sub_P (P,ll,e)) is CQC-variable_list of k,A by Def29;
then reconsider l = Sub_the_arguments_of (Sub_P (P,ll,e)) as FinSequence of bound_QC-variables A by Th34;
reconsider s = CQC_Subst (l,((Sub_P (P,ll,e)) `2)) as FinSequence of bound_QC-variables A ;
 len l = k by A1, CARD_1:def_7;
then A2: len s = k by Def3;
 Sub_P (P,ll,e) = [(P ! ll),e] by Th9;
then  (Sub_P (P,ll,e)) `1 = P ! ll by MCART_1:7;
then reconsider P9 = the_pred_symbol_of ((Sub_P (P,ll,e)) `1) as QC-pred_symbol of k,A by Lm7;
reconsider s = s as CQC-variable_list of k,A by A2, Th34;
 ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( CQC_Sub (Sub_P (P,ll,e)) = F . (Sub_P (P,ll,e)) & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) by Def38;
then  CQC_Sub (Sub_P (P,ll,e)) = P9 ! s ;
hence  CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A ; ::_thesis: verum
end;

theorem Th36: :: SUBSTUT1:36
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds
CQC_Sub (Sub_not S) is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds
CQC_Sub (Sub_not S) is Element of CQC-WFF A
let S be Element of QC-Sub-WFF A; ::_thesis: ( CQC_Sub S is Element of CQC-WFF A implies CQC_Sub (Sub_not S) is Element of CQC-WFF A )
set S9 = Sub_not S;
assume A1: CQC_Sub S is Element of CQC-WFF A ; ::_thesis: CQC_Sub (Sub_not S) is Element of CQC-WFF A
 CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th29;
hence  CQC_Sub (Sub_not S) is Element of CQC-WFF A by A1, CQC_LANG:8; ::_thesis: verum
end;

theorem Th37: :: SUBSTUT1:37
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds
CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds
CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A
let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A implies CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A )
assume A1: ( S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A ) ; ::_thesis: CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A
 ( S1 `2 = S2 `2 implies CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) ) by Th31;
hence  CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A by A1, CQC_LANG:9; ::_thesis: verum
end;

theorem Th38: :: SUBSTUT1:38
for A being QC-alphabet
for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let x be bound_QC-variable of A; ::_thesis: for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let S be Element of QC-Sub-WFF A; ::_thesis: for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let xSQ be second_Q_comp of [S,x]; ::_thesis: ( CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable implies CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A )
set S9 = Sub_All ([S,x],xSQ);
assume that
A1: CQC_Sub S is Element of CQC-WFF A and
A2: [S,x] is quantifiable ; ::_thesis: CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
 Sub_the_scope_of (Sub_All ([S,x],xSQ)) = [S,x] `1 by A2, Th21;
then  Quant ((Sub_All ([S,x],xSQ)),(CQC_Sub (Sub_the_scope_of (Sub_All ([S,x],xSQ))))) = All ((S_Bound (@ (Sub_All ([S,x],xSQ)))),(CQC_Sub S)) ;
then  Quant ((Sub_All ([S,x],xSQ)),(CQC_Sub (Sub_the_scope_of (Sub_All ([S,x],xSQ))))) is Element of CQC-WFF A by A1, CQC_LANG:13;
hence  CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A by A2, Th14, Th32; ::_thesis: verum
end;

scheme :: SUBSTUT1:sch 5
SubCQCInd{ F1() ->  QC-alphabet , P1[ set ] } :
 for S being Element of CQC-Sub-WFF F1() holds P1[S]
provided
A1: for S, S9 being Element of CQC-Sub-WFF F1()
for x being bound_QC-variable of F1()
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1()
for e being Element of vSUB F1() holds
( P1[ Sub_P (P,ll,e)] & ( S is F1() -Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S9 `2 & P1[S] & P1[S9] implies P1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] ) )
proof
defpred S1[ Element of QC-Sub-WFF F1()] means ( $1 is Element of CQC-Sub-WFF F1() implies P1[$1] );
A2: for S being Element of QC-Sub-WFF F1() st S1[S] holds
S1[ Sub_not S]
proof
let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S1[S] implies S1[ Sub_not S] )
assume A3: S1[S] ; ::_thesis: S1[ Sub_not S]
assume  Sub_not S is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_not S]
then  Sub_not S in CQC-Sub-WFF F1() ;
then consider S9 being Element of QC-Sub-WFF F1() such that
A4: Sub_not S = S9 and
A5: S9 `1 is Element of CQC-WFF F1() ;
 S9 `1 = 'not' (S `1) by A4, MCART_1:7;
then  S `1 is Element of CQC-WFF F1() by A5, CQC_LANG:8;
then  S in CQC-Sub-WFF F1() ;
hence  P1[ Sub_not S] by A1, A3; ::_thesis: verum
end;
A6: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)]
let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)]
let ll be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)]
let e be Element of vSUB F1(); ::_thesis: S1[ Sub_P (P,ll,e)]
assume  Sub_P (P,ll,e) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_P (P,ll,e)]
then  Sub_P (P,ll,e) in CQC-Sub-WFF F1() ;
then A7: ex S1 being Element of QC-Sub-WFF F1() st
( Sub_P (P,ll,e) = S1 & S1 `1 is Element of CQC-WFF F1() ) ;
 Sub_P (P,ll,e) = [(P ! ll),e] by Th9;
then A8: P ! ll is Element of CQC-WFF F1() by A7, MCART_1:7;
then A9:  {  (ll . j) where j is Element of NAT : ( 1 <= j & j <= len ll & ll . j in fixed_QC-variables F1() )  }  = {} by CQC_LANG:7;
  {  (ll . i) where i is Element of NAT : ( 1 <= i & i <= len ll & ll . i in free_QC-variables F1() )  }  = {} by A8, CQC_LANG:7;
then  ll is CQC-variable_list of k,F1() by A9, CQC_LANG:5;
hence  P1[ Sub_P (P,ll,e)] by A1; ::_thesis: verum
end;
A10: for S1, S2 being Element of QC-Sub-WFF F1() st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds
S1[ Sub_& (S1,S2)]
proof
let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & S1[S1] & S1[S2] implies S1[ Sub_& (S1,S2)] )
assume that
A11: S1 `2 = S2 `2 and
A12: ( S1[S1] & S1[S2] ) ; ::_thesis: S1[ Sub_& (S1,S2)]
assume  Sub_& (S1,S2) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_& (S1,S2)]
then  Sub_& (S1,S2) in CQC-Sub-WFF F1() ;
then consider S9 being Element of QC-Sub-WFF F1() such that
A13: Sub_& (S1,S2) = S9 and
A14: S9 `1 is Element of CQC-WFF F1() ;
 Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A11, Def21;
then A15: S9 `1 = (S1 `1) '&' (S2 `1) by A13, MCART_1:7;
then  S2 `1 is Element of CQC-WFF F1() by A14, CQC_LANG:9;
then A16: S2 in CQC-Sub-WFF F1() ;
 S1 `1 is Element of CQC-WFF F1() by A14, A15, CQC_LANG:9;
then  S1 in CQC-Sub-WFF F1() ;
hence  P1[ Sub_& (S1,S2)] by A1, A11, A12, A16; ::_thesis: verum
end;
A17: for x being bound_QC-variable of F1()
for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
proof
let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All ([S,x],SQ)]
let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] )
assume that
A18: [S,x] is quantifiable and
A19: S1[S] ; ::_thesis: S1[ Sub_All ([S,x],SQ)]
assume  Sub_All ([S,x],SQ) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_All ([S,x],SQ)]
then  Sub_All ([S,x],SQ) in CQC-Sub-WFF F1() ;
then consider S9 being Element of QC-Sub-WFF F1() such that
A20: Sub_All ([S,x],SQ) = S9 and
A21: S9 `1 is Element of CQC-WFF F1() ;
 Sub_All ([S,x],SQ) = [(All (([S,x] `2),(([S,x] `1) `1))),SQ] by A18, Def24;
then  S9 `1 = All (([S,x] `2),(([S,x] `1) `1)) by A20, MCART_1:7;
then  ([S,x] `1) `1 is Element of CQC-WFF F1() by A21, CQC_LANG:13;
then  S in CQC-Sub-WFF F1() ;
hence  P1[ Sub_All ([S,x],SQ)] by A1, A18, A19; ::_thesis: verum
end;
A22: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
S1[S] by A1;
 for S being Element of QC-Sub-WFF F1() holds S1[S] from SUBSTUT1:sch_1(A6, A22, A2, A10, A17);
hence  for S being Element of CQC-Sub-WFF F1() holds P1[S] ; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let S be Element of CQC-Sub-WFF A;
:: original: CQC_Sub
redefine func CQC_Sub S ->  Element of CQC-WFF A;
coherence
 CQC_Sub S is Element of CQC-WFF A
proof
defpred S1[ Element of QC-Sub-WFF A] means  CQC_Sub $1 is Element of CQC-WFF A;
A1: for S, S9 being Element of CQC-Sub-WFF A
for x being bound_QC-variable of A
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A
for e being Element of vSUB A holds
( S1[ Sub_P (P,ll,e)] & ( S is A -Sub_VERUM implies S1[S] ) & ( S1[S] implies S1[ Sub_not S] ) & ( S `2 = S9 `2 & S1[S] & S1[S9] implies S1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] ) ) by Th33, Th35, Th36, Th37, Th38;
 for S being Element of CQC-Sub-WFF A holds S1[S] from SUBSTUT1:sch_5(A1);
hence  CQC_Sub S is Element of CQC-WFF A ; ::_thesis: verum
end;
end;

theorem :: SUBSTUT1:39
for A being QC-alphabet
for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;