:: Coincidence Lemma and Substitution Lemma
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: SUBLEMMA:1
for f, g, h, h1, h2 being Function st dom h1 c= dom h & dom h2 c= dom h holds
(f +* g) +* h = ((f +* h1) +* (g +* h2)) +* h
proofend;

theorem Th2: :: SUBLEMMA:2
for Al being QC-alphabet
for x being bound_QC-variable of Al
for vS1 being Function st x in dom vS1 holds
(vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1
proofend;

definition
let Al be QC-alphabet ;
let A be non empty set ;
mode Val_Sub of A,Al is PartFunc of (bound_QC-variables Al),A;
end;

notation
let Al be QC-alphabet ;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let vS be Val_Sub of A,Al;
synonym v . vS for Al +* A;
end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let vS be Val_Sub of A,Al;
:: original:.
redefine funcv . vS ->  Element of Valuations_in (Al,A);
coherence
 . is Element of Valuations_in (Al,A)
proofend;
end;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
:: original:`1
redefine funcS `1  ->  Element of CQC-WFF Al;
coherence
 S `1 is Element of CQC-WFF Al
proofend;
end;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
func Val_S (v,S) ->  Val_Sub of A,Al equals :: SUBLEMMA:def 1
(@ (S `2)) * v;
coherence
 (@ (S `2)) * v is Val_Sub of A,Al ;
end;

:: deftheorem  defines Val_S SUBLEMMA:def_1_:_
 for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for A being non empty set
for v being Element of Valuations_in (Al,A) holds Val_S (v,S) = (@ (S `2)) * v;

theorem Th3: :: SUBLEMMA:3
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Al -Sub_VERUM holds
CQC_Sub S = VERUM Al
proofend;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let J be interpretation of Al,A;
predJ,v |= S means :Def2: :: SUBLEMMA:def 2
J,v |= S `1 ;
end;

:: deftheorem Def2 defines |= SUBLEMMA:def_2_:_
 for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds
( J,v |= S iff J,v |= S `1 );

theorem Th4: :: SUBLEMMA:4
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al st S is Al -Sub_VERUM holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
proofend;

theorem Th5: :: SUBLEMMA:5
for Al being QC-alphabet
for k, i being Element of NAT
for ll being CQC-variable_list of k,Al st i in dom ll holds
ll . i is bound_QC-variable of Al
proofend;

theorem Th6: :: SUBLEMMA:6
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_atomic holds
CQC_Sub S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2)))
proofend;

theorem :: SUBLEMMA:7
for Al being QC-alphabet
for k being Element of NAT
for P, P9 being QC-pred_symbol of k,Al
for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9
proofend;

definition
let k be Element of NAT ;
let Al be QC-alphabet ;
let P be QC-pred_symbol of k,Al;
let ll be CQC-variable_list of k,Al;
let Sub be CQC_Substitution of Al;
:: original:Sub_P
redefine func Sub_P (P,ll,Sub) ->  Element of CQC-Sub-WFF Al;
coherence
 Sub_P (P,ll,Sub) is Element of CQC-Sub-WFF Al
proofend;
end;

theorem Th8: :: SUBLEMMA:8
for Al being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
proofend;

theorem :: SUBLEMMA:9
for Al being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
proofend;

theorem Th10: :: SUBLEMMA:10
for Al being QC-alphabet
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al
proofend;

registration
let Al be QC-alphabet ;
let k be Element of NAT ;
let ll be CQC-variable_list of k,Al;
let Sub be CQC_Substitution of Al;
cluster CQC_Subst (ll,Sub) ->  bound_QC-variables Al -valued k -element ;
coherence
 ( CQC_Subst (ll,Sub) is bound_QC-variables Al -valued & CQC_Subst (ll,Sub) is k -element ) by Th10;
end;

theorem Th11: :: SUBLEMMA:11
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st not x in dom (S `2) holds
(v . (Val_S (v,S))) . x = v . x
proofend;

theorem Th12: :: SUBLEMMA:12
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
(v . (Val_S (v,S))) . x = (Val_S (v,S)) . x
proofend;

theorem Th13: :: SUBLEMMA:13
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))
proofend;

theorem Th14: :: SUBLEMMA:14
for Al being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds (Sub_P (P,ll,Sub)) `1 = P ! ll
proofend;

theorem Th15: :: SUBLEMMA:15
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (Sub_P (P,ll,Sub)) iff J,v . (Val_S (v,(Sub_P (P,ll,Sub)))) |= Sub_P (P,ll,Sub) )
proofend;

theorem Th16: :: SUBLEMMA:16
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al holds
( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 )
proofend;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
:: original:Sub_not
redefine func Sub_not S ->  Element of CQC-Sub-WFF Al;
coherence
 Sub_not S is Element of CQC-Sub-WFF Al
proofend;
end;

theorem Th17: :: SUBLEMMA:17
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al holds
( not J,v . (Val_S (v,S)) |= S iff J,v . (Val_S (v,S)) |= Sub_not S )
proofend;

theorem Th18: :: SUBLEMMA:18
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al holds Val_S (v,S) = Val_S (v,(Sub_not S))
proofend;

theorem Th19: :: SUBLEMMA:19
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al st ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (Sub_not S) iff J,v . (Val_S (v,(Sub_not S))) |= Sub_not S )
proofend;

definition
let Al be QC-alphabet ;
let S1, S2 be Element of CQC-Sub-WFF Al;
assume A1: S1 `2 = S2 `2 ;
func CQCSub_& (S1,S2) ->  Element of CQC-Sub-WFF Al equals :Def3: :: SUBLEMMA:def 3
 Sub_& (S1,S2);
coherence
 Sub_& (S1,S2) is Element of CQC-Sub-WFF Al
proofend;
end;

:: deftheorem Def3 defines CQCSub_& SUBLEMMA:def_3_:_
 for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQCSub_& (S1,S2) = Sub_& (S1,S2);

theorem Th20: :: SUBLEMMA:20
for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
( (CQCSub_& (S1,S2)) `1 = (S1 `1) '&' (S2 `1) & (CQCSub_& (S1,S2)) `2 = S1 `2 )
proofend;

theorem Th21: :: SUBLEMMA:21
for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
(CQCSub_& (S1,S2)) `2 = S1 `2
proofend;

theorem :: SUBLEMMA:22
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
( Val_S (v,S1) = Val_S (v,(CQCSub_& (S1,S2))) & Val_S (v,S2) = Val_S (v,(CQCSub_& (S1,S2))) ) by Th21;

theorem Th23: :: SUBLEMMA:23
for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
proofend;

theorem Th24: :: SUBLEMMA:24
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
( ( J,v . (Val_S (v,S1)) |= S1 & J,v . (Val_S (v,S2)) |= S2 ) iff J,v . (Val_S (v,(CQCSub_& (S1,S2)))) |= CQCSub_& (S1,S2) )
proofend;

theorem Th25: :: SUBLEMMA:25
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S1 iff J,v . (Val_S (v,S1)) |= S1 ) ) & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S2 iff J,v . (Val_S (v,S2)) |= S2 ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_& (S1,S2)) iff J,v . (Val_S (v,(CQCSub_& (S1,S2)))) |= CQCSub_& (S1,S2) )
proofend;

theorem Th26: :: SUBLEMMA:26
for Al being QC-alphabet
for B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
( (Sub_All (B,SQ)) `1 = All ((B `2),((B `1) `1)) & (Sub_All (B,SQ)) `2 = SQ )
proofend;

definition
let Al be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
attrB is CQC-WFF-like  means :Def4: :: SUBLEMMA:def 4
B `1 in CQC-Sub-WFF Al;
end;

:: deftheorem Def4 defines CQC-WFF-like SUBLEMMA:def_4_:_
 for Al being QC-alphabet
for B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] holds
( B is CQC-WFF-like iff B `1 in CQC-Sub-WFF Al );

registration
let Al be QC-alphabet ;
cluster CQC-WFF-like for Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
existence
 ex b1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] st b1 is CQC-WFF-like
proofend;
end;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let x be bound_QC-variable of Al;
:: original:[
redefine func[S,x] ->  CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
coherence
 [S,x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
proofend;
end;

definition
let Al be QC-alphabet ;
let B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
:: original:`1
redefine funcB `1  ->  Element of CQC-Sub-WFF Al;
coherence
 B `1 is Element of CQC-Sub-WFF Al by Def4;
end;

definition
let Al be QC-alphabet ;
let B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;
func CQCSub_All (B,SQ) ->  Element of CQC-Sub-WFF Al equals :Def5: :: SUBLEMMA:def 5
 Sub_All (B,SQ);
coherence
 Sub_All (B,SQ) is Element of CQC-Sub-WFF Al
proofend;
end;

:: deftheorem Def5 defines CQCSub_All SUBLEMMA:def_5_:_
 for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) = Sub_All (B,SQ);

theorem Th27: :: SUBLEMMA:27
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) is Sub_universal
proofend;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
assume X1: S is Sub_universal ;
func CQCSub_the_scope_of S ->  Element of CQC-Sub-WFF Al equals :Def6: :: SUBLEMMA:def 6
 Sub_the_scope_of S;
coherence
 Sub_the_scope_of S is Element of CQC-Sub-WFF Al
proofend;
end;

:: deftheorem Def6 defines CQCSub_the_scope_of SUBLEMMA:def_6_:_
 for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQCSub_the_scope_of S = Sub_the_scope_of S;

definition
let Al be QC-alphabet ;
let S1 be Element of CQC-Sub-WFF Al;
let p be Element of CQC-WFF Al;
assume that
A1: S1 is Sub_universal and
A2: p = CQC_Sub (CQCSub_the_scope_of S1) ;
func CQCQuant (S1,p) ->  Element of CQC-WFF Al equals :Def7: :: SUBLEMMA:def 7
 Quant (S1,p);
coherence
 Quant (S1,p) is Element of CQC-WFF Al
proofend;
end;

:: deftheorem Def7 defines CQCQuant SUBLEMMA:def_7_:_
 for Al being QC-alphabet
for S1 being Element of CQC-Sub-WFF Al
for p being Element of CQC-WFF Al st S1 is Sub_universal & p = CQC_Sub (CQCSub_the_scope_of S1) holds
CQCQuant (S1,p) = Quant (S1,p);

theorem Th28: :: SUBLEMMA:28
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S)))
proofend;

theorem Th29: :: SUBLEMMA:29
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1
proofend;

begin

theorem Th30: :: SUBLEMMA:30
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
proofend;

theorem Th31: :: SUBLEMMA:31
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S))
proofend;

theorem :: SUBLEMMA:32
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
proofend;

theorem :: SUBLEMMA:33
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al st x in dom (@ (S `2)) holds
(@ (S `2)) . x is bound_QC-variable of Al
proofend;

theorem Th34: :: SUBLEMMA:34
for Al being QC-alphabet holds [:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al)
proofend;

theorem Th35: :: SUBLEMMA:35
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All (B,SQ) = Sub_All (B1,SQ1) holds
( B `2 = B1 `2 & SQ = SQ1 )
proofend;

theorem Th36: :: SUBLEMMA:36
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & CQCSub_All (B,SQ) = Sub_All (B1,SQ1) holds
( B `2 = B1 `2 & SQ = SQ1 )
proofend;

theorem :: SUBLEMMA:37
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x
proofend;

theorem Th38: :: SUBLEMMA:38
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
( not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
proofend;

theorem Th39: :: SUBLEMMA:39
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
proofend;

theorem Th40: :: SUBLEMMA:40
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
proofend;

theorem Th41: :: SUBLEMMA:41
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
proofend;

theorem :: SUBLEMMA:42
for Al being QC-alphabet holds still_not-bound_in (VERUM Al) c= Bound_Vars (VERUM Al)
proofend;

theorem Th43: :: SUBLEMMA:43
for Al being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)
proofend;

theorem Th44: :: SUBLEMMA:44
for Al being QC-alphabet
for p being Element of CQC-WFF Al st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in ('not' p) c= Bound_Vars ('not' p)
proofend;

theorem Th45: :: SUBLEMMA:45
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al st still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q holds
still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q)
proofend;

theorem Th46: :: SUBLEMMA:46
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in (All (x,p)) c= Bound_Vars (All (x,p))
proofend;

theorem Th47: :: SUBLEMMA:47
for Al being QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p c= Bound_Vars p
proofend;

notation
let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let a be Element of A;
synonym x | a for Al .--> A;
end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let a be Element of A;
:: original:|
redefine funcx | a ->  Val_Sub of A,Al;
coherence
 | is Val_Sub of A,Al
proofend;
end;

theorem Th48: :: SUBLEMMA:48
for Al being QC-alphabet
for b being set
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A st x <> b holds
(v . (x | a)) . b = v . b
proofend;

theorem Th49: :: SUBLEMMA:49
for Al being QC-alphabet
for x, y being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A st x = y holds
(v . (x | a)) . y = a
proofend;

theorem Th50: :: SUBLEMMA:50
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
proofend;

definition
let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let x be bound_QC-variable of Al;
let xSQ be second_Q_comp of [S,x];
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
func NEx_Val (v,S,x,xSQ) ->  Val_Sub of A,Al equals :: SUBLEMMA:def 8
(@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;
coherence
 (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v is Val_Sub of A,Al ;
end;

:: deftheorem  defines NEx_Val SUBLEMMA:def_8_:_
 for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al
for x being bound_QC-variable of Al
for xSQ being second_Q_comp of [S,x]
for A being non empty set
for v being Element of Valuations_in (Al,A) holds NEx_Val (v,S,x,xSQ) = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let v, w be Val_Sub of A,Al;
:: original:.
redefine funcv +* w ->  Val_Sub of A,Al;
coherence
 . is Val_Sub of A,Al
proofend;
end;

theorem Th51: :: SUBLEMMA:51
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable &amp; x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
proofend;

theorem Th52: :: SUBLEMMA:52
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable &amp; not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x
proofend;

theorem Th53: :: SUBLEMMA:53
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds
( Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S) = (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a) &amp; dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
proofend;

theorem Th54: :: SUBLEMMA:54
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) iff for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S )
proofend;

theorem Th55: :: SUBLEMMA:55
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
proofend;

theorem Th56: :: SUBLEMMA:56
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S ) iff for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )
proofend;

begin

theorem Th57: :: SUBLEMMA:57
for Al being QC-alphabet
for l1 being FinSequence of QC-variables Al st rng l1 c= bound_QC-variables Al holds
still_not-bound_in l1 = rng l1
proofend;

theorem Th58: :: SUBLEMMA:58
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A holds
( dom v = bound_QC-variables Al &amp; dom (x | a) = {x} )
proofend;

theorem Th59: :: SUBLEMMA:59
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
proofend;

theorem Th60: :: SUBLEMMA:60
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
proofend;

theorem Th61: :: SUBLEMMA:61
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
proofend;

theorem Th62: :: SUBLEMMA:62
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) &amp; ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in q) = w | (still_not-bound_in q) holds
( J,v |= q iff J,w |= q ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (p '&amp;' q)) = w | (still_not-bound_in (p '&amp;' q)) holds
( J,v |= p '&amp;' q iff J,w |= p '&amp;' q )
proofend;

theorem Th63: :: SUBLEMMA:63
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A
for X being set st X c= bound_QC-variables Al holds
( dom (v | X) = dom ((v . (x | a)) | X) &amp; dom (v | X) = X )
proofend;

theorem :: SUBLEMMA:64
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
proofend;

theorem :: SUBLEMMA:65
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x}
proofend;

theorem Th66: :: SUBLEMMA:66
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,A)
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
proofend;

theorem Th67: :: SUBLEMMA:67
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
proofend;

:: Coincidence Lemma (Ebb et al, Chapter III, 5.1)
theorem Th68: :: SUBLEMMA:68
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p )
proofend;

theorem Th69: :: SUBLEMMA:69
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
proofend;

theorem Th70: :: SUBLEMMA:70
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) iff for a being Element of A holds J,v . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )
proofend;

theorem Th71: :: SUBLEMMA:71
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] holds dom (NEx_Val (v,S,x,xSQ)) = dom (RestrictSub (x,(All (x,(S `1))),xSQ))
proofend;

theorem Th72: :: SUBLEMMA:72
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] holds
( ( for a being Element of A holds J,v . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) iff for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S )
proofend;

theorem Th73: :: SUBLEMMA:73
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] holds
( ( for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ) iff for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S `1 )
proofend;

theorem Th74: :: SUBLEMMA:74
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ll ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
proofend;

theorem Th75: :: SUBLEMMA:75
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
proofend;

theorem Th76: :: SUBLEMMA:76
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= 'not' p iff J,v . ((vS +* vS1) +* vS2) |= 'not' p )
proofend;

theorem Th77: :: SUBLEMMA:77
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) &amp; ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&amp;' q) ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= p '&amp;' q iff J,v . ((vS +* vS1) +* vS2) |= p '&amp;' q )
proofend;

theorem Th78: :: SUBLEMMA:78
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
proofend;

theorem Th79: :: SUBLEMMA:79
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) &amp; dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
proofend;

theorem Th80: :: SUBLEMMA:80
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= All (x,p) iff J,v . ((vS +* vS1) +* vS2) |= All (x,p) )
proofend;

theorem Th81: :: SUBLEMMA:81
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p )
proofend;

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
func RSub1 p ->  set  means :Def9: :: SUBLEMMA:def 9
 for b being set holds
( b in it iff ex x being bound_QC-variable of Al st
( x = b &amp; not x in still_not-bound_in p ) );
existence
 ex b1 being set st
for b being set holds
( b in b1 iff ex x being bound_QC-variable of Al st
( x = b &amp; not x in still_not-bound_in p ) )
proofend;
uniqueness
 for b1, b2 being set st ( for b being set holds
( b in b1 iff ex x being bound_QC-variable of Al st
( x = b &amp; not x in still_not-bound_in p ) ) ) &amp; ( for b being set holds
( b in b2 iff ex x being bound_QC-variable of Al st
( x = b &amp; not x in still_not-bound_in p ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines RSub1 SUBLEMMA:def_9_:_
 for Al being QC-alphabet
for p being Element of CQC-WFF Al
for b3 being set holds
( b3 = RSub1 p iff for b being set holds
( b in b3 iff ex x being bound_QC-variable of Al st
( x = b &amp; not x in still_not-bound_in p ) ) );

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
let Sub be CQC_Substitution of Al;
func RSub2 (p,Sub) ->  set  means :Def10: :: SUBLEMMA:def 10
 for b being set holds
( b in it iff ex x being bound_QC-variable of Al st
( x = b &amp; x in still_not-bound_in p &amp; x = (@ Sub) . x ) );
existence
 ex b1 being set st
for b being set holds
( b in b1 iff ex x being bound_QC-variable of Al st
( x = b &amp; x in still_not-bound_in p &amp; x = (@ Sub) . x ) )
proofend;
uniqueness
 for b1, b2 being set st ( for b being set holds
( b in b1 iff ex x being bound_QC-variable of Al st
( x = b &amp; x in still_not-bound_in p &amp; x = (@ Sub) . x ) ) ) &amp; ( for b being set holds
( b in b2 iff ex x being bound_QC-variable of Al st
( x = b &amp; x in still_not-bound_in p &amp; x = (@ Sub) . x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines RSub2 SUBLEMMA:def_10_:_
 for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al
for b4 being set holds
( b4 = RSub2 (p,Sub) iff for b being set holds
( b in b4 iff ex x being bound_QC-variable of Al st
( x = b &amp; x in still_not-bound_in p &amp; x = (@ Sub) . x ) ) );

theorem Th82: :: SUBLEMMA:82
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))
proofend;

theorem Th83: :: SUBLEMMA:83
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))))
proofend;

theorem Th84: :: SUBLEMMA:84
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))
proofend;

theorem Th85: :: SUBLEMMA:85
for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
@ ((CQCSub_All ([S,x],xSQ)) `2) = ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* ((@ xSQ) | (RSub1 (All (x,(S `1)))))) +* ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))
proofend;

theorem Th86: :: SUBLEMMA:86
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) &amp; ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) &amp; dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 &amp; v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
proofend;

theorem Th87: :: SUBLEMMA:87
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
proofend;

theorem Th88: :: SUBLEMMA:88
for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable &amp; ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
proofend;

scheme :: SUBLEMMA:sch 1
SubCQCInd1{ 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)] &amp; ( S is F1() -Sub_VERUM implies P1[S] ) &amp; ( P1[S] implies P1[ Sub_not S] ) &amp; ( S `2 = S9 `2 &amp; P1[S] &amp; P1[S9] implies P1[ CQCSub_&amp; (S,S9)] ) &amp; ( [S,x] is quantifiable &amp; P1[S] implies P1[ CQCSub_All ([S,x],SQ)] ) )
proofend;

:: Substitution Lemma (Ebb et al, Chapter III, 8.3)
theorem :: SUBLEMMA:89
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
proofend;