:: SUBLEMMA semantic presentation

theorem Th1: :: SUBLEMMA:1
for b1, b2, b3, b4, b5 being Function st dom b4 c= dom b3 & dom b5 c= dom b3 holds
(b1 +* b2) +* b3 = ((b1 +* b4) +* (b2 +* b5)) +* b3
proof end;

theorem Th2: :: SUBLEMMA:2
for b1 being bound_QC-variable
for b2 being Function st b1 in dom b2 holds
(b2 | ((dom b2) \ {b1})) +* (b1 .--> (b2 . b1)) = b2
proof end;

definition
let c1 be non empty set ;
mode Val_Sub of a1 is PartFunc of bound_QC-variables ,a1;
end;

definition
let c1 be non empty set ;
let c2 be Element of Valuations_in c1;
let c3 be Val_Sub of c1;
func c2 . c3 -> Element of Valuations_in a1 equals :: SUBLEMMA:def 1
a2 +* a3;
coherence
c2 +* c3 is Element of Valuations_in c1
proof end;
end;

:: deftheorem Def1 defines . SUBLEMMA:def 1 :
for b1 being non empty set
for b2 being Element of Valuations_in b1
for b3 being Val_Sub of b1 holds b2 . b3 = b2 +* b3;

definition
let c1 be Element of CQC-Sub-WFF ;
redefine func `1 as c1 `1 -> Element of CQC-WFF ;
coherence
c1 `1 is Element of CQC-WFF
proof end;
end;

definition
let c1 be Element of CQC-Sub-WFF ;
let c2 be non empty set ;
let c3 be Element of Valuations_in c2;
func Val_S c3,c1 -> Val_Sub of a2 equals :: SUBLEMMA:def 2
(@ (a1 `2 )) * a3;
coherence
(@ (c1 `2 )) * c3 is Val_Sub of c2 ;
end;

:: deftheorem Def2 defines Val_S SUBLEMMA:def 2 :
for b1 being Element of CQC-Sub-WFF
for b2 being non empty set
for b3 being Element of Valuations_in b2 holds Val_S b3,b1 = (@ (b1 `2 )) * b3;

theorem Th3: :: SUBLEMMA:3
for b1 being Element of CQC-Sub-WFF st b1 is Sub_VERUM holds
CQC_Sub b1 = VERUM
proof end;

definition
let c1 be Element of CQC-Sub-WFF ;
let c2 be non empty set ;
let c3 be Element of Valuations_in c2;
let c4 be interpretation of c2;
pred c4,c3 |= c1 means :Def3: :: SUBLEMMA:def 3
a4,a3 |= a1 `1 ;
end;

:: deftheorem Def3 defines |= SUBLEMMA:def 3 :
for b1 being Element of CQC-Sub-WFF
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being interpretation of b2 holds
( b4,b3 |= b1 iff b4,b3 |= b1 `1 );

theorem Th4: :: SUBLEMMA:4
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of CQC-Sub-WFF st b3 is Sub_VERUM holds
for b4 being Element of Valuations_in b1 holds
( b2,b4 |= CQC_Sub b3 iff b2,b4 . (Val_S b4,b3) |= b3 )
proof end;

theorem Th5: :: SUBLEMMA:5
for b1, b2 being Nat
for b3 being CQC-variable_list of b1 st b2 in dom b3 holds
b3 . b2 is bound_QC-variable
proof end;

theorem Th6: :: SUBLEMMA:6
for b1 being Element of CQC-Sub-WFF st b1 is Sub_atomic holds
CQC_Sub b1 = (the_pred_symbol_of (b1 `1 )) ! (CQC_Subst (Sub_the_arguments_of b1),(b1 `2 ))
proof end;

theorem Th7: :: SUBLEMMA:7
for b1 being Nat
for b2, b3 being QC-pred_symbol of b1
for b4, b5 being CQC-variable_list of b1
for b6, b7 being CQC_Substitution st Sub_the_arguments_of (Sub_P b2,b4,b6) = Sub_the_arguments_of (Sub_P b3,b5,b7) holds
b4 = b5
proof end;

definition
let c1 be Nat;
let c2 be QC-pred_symbol of c1;
let c3 be CQC-variable_list of c1;
let c4 be CQC_Substitution;
redefine func Sub_P as Sub_P c2,c3,c4 -> Element of CQC-Sub-WFF ;
coherence
Sub_P c2,c3,c4 is Element of CQC-Sub-WFF
proof end;
end;

theorem Th8: :: SUBLEMMA:8
canceled;

theorem Th9: :: SUBLEMMA:9
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being CQC-variable_list of b1
for b4 being CQC_Substitution holds CQC_Sub (Sub_P b2,b3,b4) = b2 ! (CQC_Subst b3,b4)
proof end;

theorem Th10: :: SUBLEMMA:10
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being CQC-variable_list of b1
for b4 being CQC_Substitution holds b2 ! (CQC_Subst b3,b4) is Element of CQC-WFF
proof end;

theorem Th11: :: SUBLEMMA:11
for b1 being Nat
for b2 being CQC-variable_list of b1
for b3 being CQC_Substitution holds CQC_Subst b2,b3 is CQC-variable_list of b1
proof end;

definition
let c1 be Nat;
let c2 be CQC-variable_list of c1;
let c3 be CQC_Substitution;
redefine func CQC_Subst as CQC_Subst c2,c3 -> CQC-variable_list of a1;
coherence
CQC_Subst c2,c3 is CQC-variable_list of c1 by Th11;
end;

theorem Th12: :: SUBLEMMA:12
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF st not b1 in dom (b4 `2 ) holds
(b3 . (Val_S b3,b4)) . b1 = b3 . b1
proof end;

theorem Th13: :: SUBLEMMA:13
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF st b1 in dom (b4 `2 ) holds
(b3 . (Val_S b3,b4)) . b1 = (Val_S b3,b4) . b1
proof end;

theorem Th14: :: SUBLEMMA:14
for b1 being Nat
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being QC-pred_symbol of b1
for b5 being CQC-variable_list of b1
for b6 being CQC_Substitution holds (b3 . (Val_S b3,(Sub_P b4,b5,b6))) *' b5 = b3 *' (CQC_Subst b5,b6)
proof end;

theorem Th15: :: SUBLEMMA:15
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being CQC-variable_list of b1
for b4 being CQC_Substitution holds (Sub_P b2,b3,b4) `1 = b2 ! b3
proof end;

theorem Th16: :: SUBLEMMA:16
for b1 being Nat
for b2 being non empty set
for b3 being interpretation of b2
for b4 being QC-pred_symbol of b1
for b5 being CQC-variable_list of b1
for b6 being CQC_Substitution
for b7 being Element of Valuations_in b2 holds
( b3,b7 |= CQC_Sub (Sub_P b4,b5,b6) iff b3,b7 . (Val_S b7,(Sub_P b4,b5,b6)) |= Sub_P b4,b5,b6 )
proof end;

theorem Th17: :: SUBLEMMA:17
for b1 being Element of CQC-Sub-WFF holds
( (Sub_not b1) `1 = 'not' (b1 `1 ) & (Sub_not b1) `2 = b1 `2 )
proof end;

definition
let c1 be Element of CQC-Sub-WFF ;
redefine func Sub_not as Sub_not c1 -> Element of CQC-Sub-WFF ;
coherence
Sub_not c1 is Element of CQC-Sub-WFF
proof end;
end;

theorem Th18: :: SUBLEMMA:18
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of Valuations_in b1
for b4 being Element of CQC-Sub-WFF holds
( not b2,b3 . (Val_S b3,b4) |= b4 iff b2,b3 . (Val_S b3,b4) |= Sub_not b4 )
proof end;

theorem Th19: :: SUBLEMMA:19
for b1 being non empty set
for b2 being Element of Valuations_in b1
for b3 being Element of CQC-Sub-WFF holds Val_S b2,b3 = Val_S b2,(Sub_not b3)
proof end;

theorem Th20: :: SUBLEMMA:20
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of CQC-Sub-WFF st ( for b4 being Element of Valuations_in b1 holds
( b2,b4 |= CQC_Sub b3 iff b2,b4 . (Val_S b4,b3) |= b3 ) ) holds
for b4 being Element of Valuations_in b1 holds
( b2,b4 |= CQC_Sub (Sub_not b3) iff b2,b4 . (Val_S b4,(Sub_not b3)) |= Sub_not b3 )
proof end;

definition
let c1, c2 be Element of CQC-Sub-WFF ;
assume E19: c1 `2 = c2 `2 ;
func CQCSub_& c1,c2 -> Element of CQC-Sub-WFF equals :Def4: :: SUBLEMMA:def 4
 Sub_& a1,a2;
coherence
Sub_& c1,c2 is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def4 defines CQCSub_& SUBLEMMA:def 4 :
for b1, b2 being Element of CQC-Sub-WFF st b1 `2 = b2 `2 holds
CQCSub_& b1,b2 = Sub_& b1,b2;

theorem Th21: :: SUBLEMMA:21
for b1, b2 being Element of CQC-Sub-WFF st b1 `2 = b2 `2 holds
( (CQCSub_& b1,b2) `1 = (b1 `1 ) '&' (b2 `1 ) & (CQCSub_& b1,b2) `2 = b1 `2 )
proof end;

theorem Th22: :: SUBLEMMA:22
for b1, b2 being Element of CQC-Sub-WFF st b1 `2 = b2 `2 holds
(CQCSub_& b1,b2) `2 = b1 `2
proof end;

theorem Th23: :: SUBLEMMA:23
for b1 being non empty set
for b2 being Element of Valuations_in b1
for b3, b4 being Element of CQC-Sub-WFF st b3 `2 = b4 `2 holds
( Val_S b2,b3 = Val_S b2,(CQCSub_& b3,b4) & Val_S b2,b4 = Val_S b2,(CQCSub_& b3,b4) ) by Th22;

theorem Th24: :: SUBLEMMA:24
for b1, b2 being Element of CQC-Sub-WFF st b1 `2 = b2 `2 holds
CQC_Sub (CQCSub_& b1,b2) = (CQC_Sub b1) '&' (CQC_Sub b2)
proof end;

theorem Th25: :: SUBLEMMA:25
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of Valuations_in b1
for b4, b5 being Element of CQC-Sub-WFF st b4 `2 = b5 `2 holds
( ( b2,b3 . (Val_S b3,b4) |= b4 & b2,b3 . (Val_S b3,b5) |= b5 ) iff b2,b3 . (Val_S b3,(CQCSub_& b4,b5)) |= CQCSub_& b4,b5 )
proof end;

theorem Th26: :: SUBLEMMA:26
for b1 being non empty set
for b2 being interpretation of b1
for b3, b4 being Element of CQC-Sub-WFF st b3 `2 = b4 `2 & ( for b5 being Element of Valuations_in b1 holds
( b2,b5 |= CQC_Sub b3 iff b2,b5 . (Val_S b5,b3) |= b3 ) ) & ( for b5 being Element of Valuations_in b1 holds
( b2,b5 |= CQC_Sub b4 iff b2,b5 . (Val_S b5,b4) |= b4 ) ) holds
for b5 being Element of Valuations_in b1 holds
( b2,b5 |= CQC_Sub (CQCSub_& b3,b4) iff b2,b5 . (Val_S b5,(CQCSub_& b3,b4)) |= CQCSub_& b3,b4 )
proof end;

theorem Th27: :: SUBLEMMA:27
for b1 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1 st b1 is quantifiable holds
( (Sub_All b1,b2) `1 = All (b1 `2 ),((b1 `1 ) `1 ) & (Sub_All b1,b2) `2 = b2 )
proof end;

definition
let c1 be Element of [:QC-Sub-WFF ,bound_QC-variables :];
attr a1 is CQC-WFF-like means :Def5: :: SUBLEMMA:def 5
a1 `1 in CQC-Sub-WFF ;
end;

:: deftheorem Def5 defines CQC-WFF-like SUBLEMMA:def 5 :
for b1 being Element of [:QC-Sub-WFF ,bound_QC-variables :] holds
( b1 is CQC-WFF-like iff b1 `1 in CQC-Sub-WFF );

registration
cluster CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
existence
ex b1 being Element of [:QC-Sub-WFF ,bound_QC-variables :] st b1 is CQC-WFF-like
proof end;
end;

definition
let c1 be Element of CQC-Sub-WFF ;
let c2 be bound_QC-variable;
redefine func [ as [c1,c2] -> CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
coherence
[c1,c2] is CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
proof end;
end;

definition
let c1 be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
redefine func `1 as c1 `1 -> Element of CQC-Sub-WFF ;
coherence
c1 `1 is Element of CQC-Sub-WFF by Def5;
end;

definition
let c1 be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
let c2 be second_Q_comp of c1;
assume E28: c1 is quantifiable ;
func CQCSub_All c1,c2 -> Element of CQC-Sub-WFF equals :Def6: :: SUBLEMMA:def 6
 Sub_All a1,a2;
coherence
Sub_All c1,c2 is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def6 defines CQCSub_All SUBLEMMA:def 6 :
for b1 being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1 st b1 is quantifiable holds
CQCSub_All b1,b2 = Sub_All b1,b2;

theorem Th28: :: SUBLEMMA:28
for b1 being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1 st b1 is quantifiable holds
CQCSub_All b1,b2 is Sub_universal
proof end;

definition
let c1 be Element of CQC-Sub-WFF ;
assume E30: c1 is Sub_universal ;
func CQCSub_the_scope_of c1 -> Element of CQC-Sub-WFF equals :Def7: :: SUBLEMMA:def 7
 Sub_the_scope_of a1;
coherence
Sub_the_scope_of c1 is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def7 defines CQCSub_the_scope_of SUBLEMMA:def 7 :
for b1 being Element of CQC-Sub-WFF st b1 is Sub_universal holds
CQCSub_the_scope_of b1 = Sub_the_scope_of b1;

definition
let c1 be Element of CQC-Sub-WFF ;
let c2 be Element of CQC-WFF ;
assume E31: ( c1 is Sub_universal & c2 = CQC_Sub (CQCSub_the_scope_of c1) ) ;
func CQCQuant c1,c2 -> Element of CQC-WFF equals :Def8: :: SUBLEMMA:def 8
 Quant a1,a2;
coherence
Quant c1,c2 is Element of CQC-WFF
proof end;
end;

:: deftheorem Def8 defines CQCQuant SUBLEMMA:def 8 :
for b1 being Element of CQC-Sub-WFF
for b2 being Element of CQC-WFF st b1 is Sub_universal & b2 = CQC_Sub (CQCSub_the_scope_of b1) holds
CQCQuant b1,b2 = Quant b1,b2;

theorem Th29: :: SUBLEMMA:29
for b1 being Element of CQC-Sub-WFF st b1 is Sub_universal holds
CQC_Sub b1 = CQCQuant b1,(CQC_Sub (CQCSub_the_scope_of b1))
proof end;

theorem Th30: :: SUBLEMMA:30
for b1 being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1 st b1 is quantifiable holds
CQCSub_the_scope_of (CQCSub_All b1,b2) = b1 `1
proof end;

theorem Th31: :: SUBLEMMA:31
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
( CQCSub_the_scope_of (CQCSub_All [b2,b1],b3) = b2 & CQCQuant (CQCSub_All [b2,b1],b3),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [b2,b1],b3))) = CQCQuant (CQCSub_All [b2,b1],b3),(CQC_Sub b2) )
proof end;

theorem Th32: :: SUBLEMMA:32
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
CQCQuant (CQCSub_All [b2,b1],b3),(CQC_Sub b2) = All (S_Bound (@ (CQCSub_All [b2,b1],b3))),(CQC_Sub b2)
proof end;

theorem Th33: :: SUBLEMMA:33
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF st b1 in dom (b4 `2 ) holds
b3 . ((@ (b4 `2 )) . b1) = (b3 . (Val_S b3,b4)) . b1
proof end;

theorem Th34: :: SUBLEMMA:34
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF st b1 in dom (@ (b2 `2 )) holds
(@ (b2 `2 )) . b1 is bound_QC-variable
proof end;

theorem Th35: :: SUBLEMMA:35
[:QC-WFF ,vSUB :] c= dom QSub
proof end;

theorem Th36: :: SUBLEMMA:36
for b1 being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1
for b3 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b4 being second_Q_comp of b3 st b1 is quantifiable & b3 is quantifiable & Sub_All b1,b2 = Sub_All b3,b4 holds
( b1 `2 = b3 `2 & b2 = b4 )
proof end;

theorem Th37: :: SUBLEMMA:37
for b1 being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b2 being second_Q_comp of b1
for b3 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b4 being second_Q_comp of b3 st b1 is quantifiable & b3 is quantifiable & CQCSub_All b1,b2 = Sub_All b3,b4 holds
( b1 `2 = b3 `2 & b2 = b4 )
proof end;

theorem Th38: :: SUBLEMMA:38
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
Sub_the_bound_of (CQCSub_All [b2,b1],b3) = b1
proof end;

theorem Th39: :: SUBLEMMA:39
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable & b1 in rng (RestrictSub b1,(All b1,(b2 `1 )),b3) holds
( not S_Bound (@ (CQCSub_All [b2,b1],b3)) in rng (RestrictSub b1,(All b1,(b2 `1 )),b3) & not S_Bound (@ (CQCSub_All [b2,b1],b3)) in Bound_Vars (b2 `1 ) )
proof end;

theorem Th40: :: SUBLEMMA:40
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable & not b1 in rng (RestrictSub b1,(All b1,(b2 `1 )),b3) holds
not S_Bound (@ (CQCSub_All [b2,b1],b3)) in rng (RestrictSub b1,(All b1,(b2 `1 )),b3)
proof end;

theorem Th41: :: SUBLEMMA:41
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
not S_Bound (@ (CQCSub_All [b2,b1],b3)) in rng (RestrictSub b1,(All b1,(b2 `1 )),b3)
proof end;

theorem Th42: :: SUBLEMMA:42
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
b2 `2 = ExpandSub b1,(b2 `1 ),(RestrictSub b1,(All b1,(b2 `1 )),b3)
proof end;

theorem Th43: :: SUBLEMMA:43
still_not-bound_in VERUM c= Bound_Vars VERUM by QC_LANG3:7, SUBSTUT1:2;

theorem Th44: :: SUBLEMMA:44
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being CQC-variable_list of b1 holds still_not-bound_in (b2 ! b3) c= Bound_Vars (b2 ! b3)
proof end;

theorem Th45: :: SUBLEMMA:45
for b1 being Element of CQC-WFF st still_not-bound_in b1 c= Bound_Vars b1 holds
still_not-bound_in ('not' b1) c= Bound_Vars ('not' b1)
proof end;

theorem Th46: :: SUBLEMMA:46
for b1, b2 being Element of CQC-WFF st still_not-bound_in b1 c= Bound_Vars b1 & still_not-bound_in b2 c= Bound_Vars b2 holds
still_not-bound_in (b1 '&' b2) c= Bound_Vars (b1 '&' b2)
proof end;

theorem Th47: :: SUBLEMMA:47
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable st still_not-bound_in b1 c= Bound_Vars b1 holds
still_not-bound_in (All b2,b1) c= Bound_Vars (All b2,b1)
proof end;

theorem Th48: :: SUBLEMMA:48
for b1 being Element of CQC-WFF holds still_not-bound_in b1 c= Bound_Vars b1
proof end;

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be bound_QC-variable;
func c3 | c2 -> Val_Sub of a1 equals :: SUBLEMMA:def 9
a3 .--> a2;
coherence
c3 .--> c2 is Val_Sub of c1
proof end;
end;

:: deftheorem Def9 defines | SUBLEMMA:def 9 :
for b1 being non empty set
for b2 being Element of b1
for b3 being bound_QC-variable holds b3 | b2 = b3 .--> b2;

theorem Th49: :: SUBLEMMA:49
for b1 being set
for b2 being bound_QC-variable
for b3 being non empty set
for b4 being Element of Valuations_in b3
for b5 being Element of b3 st b2 <> b1 holds
(b4 . (b2 | b5)) . b1 = b4 . b1
proof end;

theorem Th50: :: SUBLEMMA:50
for b1, b2 being bound_QC-variable
for b3 being non empty set
for b4 being Element of Valuations_in b3
for b5 being Element of b3 st b1 = b2 holds
(b4 . (b1 | b5)) . b2 = b5
proof end;

theorem Th51: :: SUBLEMMA:51
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4 being interpretation of b3
for b5 being Element of Valuations_in b3 holds
( b4,b5 |= All b2,b1 iff for b6 being Element of b3 holds b4,b5 . (b2 | b6) |= b1 )
proof end;

definition
let c1 be Element of CQC-Sub-WFF ;
let c2 be bound_QC-variable;
let c3 be second_Q_comp of [c1,c2];
let c4 be non empty set ;
let c5 be Element of Valuations_in c4;
func NEx_Val c5,c1,c2,c3 -> Val_Sub of a4 equals :: SUBLEMMA:def 10
(@ (RestrictSub a2,(All a2,(a1 `1 )),a3)) * a5;
coherence
(@ (RestrictSub c2,(All c2,(c1 `1 )),c3)) * c5 is Val_Sub of c4 ;
end;

:: deftheorem Def10 defines NEx_Val SUBLEMMA:def 10 :
for b1 being Element of CQC-Sub-WFF
for b2 being bound_QC-variable
for b3 being second_Q_comp of [b1,b2]
for b4 being non empty set
for b5 being Element of Valuations_in b4 holds NEx_Val b5,b1,b2,b3 = (@ (RestrictSub b2,(All b2,(b1 `1 )),b3)) * b5;

definition
let c1 be non empty set ;
let c2, c3 be Val_Sub of c1;
redefine func +* as c2 +* c3 -> Val_Sub of a1;
coherence
c2 +* c3 is Val_Sub of c1
proof end;
end;

theorem Th52: :: SUBLEMMA:52
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable & b1 in rng (RestrictSub b1,(All b1,(b2 `1 )),b3) holds
S_Bound (@ (CQCSub_All [b2,b1],b3)) = x. (upVar (RestrictSub b1,(All b1,(b2 `1 )),b3),(b2 `1 ))
proof end;

theorem Th53: :: SUBLEMMA:53
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable & not b1 in rng (RestrictSub b1,(All b1,(b2 `1 )),b3) holds
S_Bound (@ (CQCSub_All [b2,b1],b3)) = b1
proof end;

theorem Th54: :: SUBLEMMA:54
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] st [b4,b1] is quantifiable holds
for b6 being Element of b2 holds
( Val_S (b3 . ((S_Bound (@ (CQCSub_All [b4,b1],b5))) | b6)),b4 = (NEx_Val (b3 . ((S_Bound (@ (CQCSub_All [b4,b1],b5))) | b6)),b4,b1,b5) +* (b1 | b6) & dom (RestrictSub b1,(All b1,(b4 `1 )),b5) misses {b1} )
proof end;

theorem Th55: :: SUBLEMMA:55
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being Element of CQC-Sub-WFF
for b6 being second_Q_comp of [b5,b1] st [b5,b1] is quantifiable holds
( ( for b7 being Element of b2 holds b3,(b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)) . (Val_S (b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)),b5) |= b5 ) iff for b7 being Element of b2 holds b3,(b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)) . ((NEx_Val (b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)),b5,b1,b6) +* (b1 | b7)) |= b5 )
proof end;

theorem Th56: :: SUBLEMMA:56
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] st [b4,b1] is quantifiable holds
for b6 being Element of b2 holds NEx_Val (b3 . ((S_Bound (@ (CQCSub_All [b4,b1],b5))) | b6)),b4,b1,b5 = NEx_Val b3,b4,b1,b5
proof end;

theorem Th57: :: SUBLEMMA:57
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being Element of CQC-Sub-WFF
for b6 being second_Q_comp of [b5,b1] st [b5,b1] is quantifiable holds
( ( for b7 being Element of b2 holds b3,(b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)) . ((NEx_Val (b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)),b5,b1,b6) +* (b1 | b7)) |= b5 ) iff for b7 being Element of b2 holds b3,(b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)) . ((NEx_Val b4,b5,b1,b6) +* (b1 | b7)) |= b5 )
proof end;

theorem Th58: :: SUBLEMMA:58
for b1 being FinSequence of QC-variables st rng b1 c= bound_QC-variables holds
still_not-bound_in b1 = rng b1
proof end;

theorem Th59: :: SUBLEMMA:59
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of b2 holds
( dom b3 = bound_QC-variables & dom (b1 | b4) = {b1} )
proof end;

theorem Th60: :: SUBLEMMA:60
for b1 being Nat
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being CQC-variable_list of b1 holds b3 *' b4 = b4 * (b3 | (still_not-bound_in b4))
proof end;

theorem Th61: :: SUBLEMMA:61
for b1 being Nat
for b2 being non empty set
for b3 being interpretation of b2
for b4 being QC-pred_symbol of b1
for b5 being CQC-variable_list of b1
for b6, b7 being Element of Valuations_in b2 st b6 | (still_not-bound_in (b4 ! b5)) = b7 | (still_not-bound_in (b4 ! b5)) holds
( b3,b6 |= b4 ! b5 iff b3,b7 |= b4 ! b5 )
proof end;

theorem Th62: :: SUBLEMMA:62
for b1 being Element of CQC-WFF
for b2 being non empty set
for b3 being interpretation of b2 st ( for b4, b5 being Element of Valuations_in b2 st b4 | (still_not-bound_in b1) = b5 | (still_not-bound_in b1) holds
( b3,b4 |= b1 iff b3,b5 |= b1 ) ) holds
for b4, b5 being Element of Valuations_in b2 st b4 | (still_not-bound_in ('not' b1)) = b5 | (still_not-bound_in ('not' b1)) holds
( b3,b4 |= 'not' b1 iff b3,b5 |= 'not' b1 )
proof end;

theorem Th63: :: SUBLEMMA:63
for b1, b2 being Element of CQC-WFF
for b3 being non empty set
for b4 being interpretation of b3 st ( for b5, b6 being Element of Valuations_in b3 st b5 | (still_not-bound_in b1) = b6 | (still_not-bound_in b1) holds
( b4,b5 |= b1 iff b4,b6 |= b1 ) ) & ( for b5, b6 being Element of Valuations_in b3 st b5 | (still_not-bound_in b2) = b6 | (still_not-bound_in b2) holds
( b4,b5 |= b2 iff b4,b6 |= b2 ) ) holds
for b5, b6 being Element of Valuations_in b3 st b5 | (still_not-bound_in (b1 '&' b2)) = b6 | (still_not-bound_in (b1 '&' b2)) holds
( b4,b5 |= b1 '&' b2 iff b4,b6 |= b1 '&' b2 )
proof end;

theorem Th64: :: SUBLEMMA:64
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of b2
for b5 being set st b5 c= bound_QC-variables holds
( dom (b3 | b5) = dom ((b3 . (b1 | b4)) | b5) & dom (b3 | b5) = b5 )
proof end;

theorem Th65: :: SUBLEMMA:65
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4, b5 being Element of Valuations_in b3
for b6 being Element of b3 st b4 | (still_not-bound_in b1) = b5 | (still_not-bound_in b1) holds
(b4 . (b2 | b6)) | (still_not-bound_in b1) = (b5 . (b2 | b6)) | (still_not-bound_in b1)
proof end;

theorem Th66: :: SUBLEMMA:66
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable holds still_not-bound_in b1 c= (still_not-bound_in (All b2,b1)) \/ {b2}
proof end;

theorem Th67: :: SUBLEMMA:67
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4, b5 being Element of Valuations_in b3
for b6 being Element of b3 st b4 | ((still_not-bound_in b1) \ {b2}) = b5 | ((still_not-bound_in b1) \ {b2}) holds
(b4 . (b2 | b6)) | (still_not-bound_in b1) = (b5 . (b2 | b6)) | (still_not-bound_in b1)
proof end;

theorem Th68: :: SUBLEMMA:68
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4 being interpretation of b3 st ( for b5, b6 being Element of Valuations_in b3 st b5 | (still_not-bound_in b1) = b6 | (still_not-bound_in b1) holds
( b4,b5 |= b1 iff b4,b6 |= b1 ) ) holds
for b5, b6 being Element of Valuations_in b3 st b5 | (still_not-bound_in (All b2,b1)) = b6 | (still_not-bound_in (All b2,b1)) holds
( b4,b5 |= All b2,b1 iff b4,b6 |= All b2,b1 )
proof end;

theorem Th69: :: SUBLEMMA:69
canceled;

theorem Th70: :: SUBLEMMA:70
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of CQC-WFF
for b4, b5 being Element of Valuations_in b1 st b4 | (still_not-bound_in b3) = b5 | (still_not-bound_in b3) holds
( b2,b4 |= b3 iff b2,b5 |= b3 )
proof end;

theorem Th71: :: SUBLEMMA:71
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1]
for b6 being Element of b2 st [b4,b1] is quantifiable holds
((b3 . ((S_Bound (@ (CQCSub_All [b4,b1],b5))) | b6)) . ((NEx_Val b3,b4,b1,b5) +* (b1 | b6))) | (still_not-bound_in (b4 `1 )) = (b3 . ((NEx_Val b3,b4,b1,b5) +* (b1 | b6))) | (still_not-bound_in (b4 `1 ))
proof end;

theorem Th72: :: SUBLEMMA:72
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being Element of CQC-Sub-WFF
for b6 being second_Q_comp of [b5,b1] st [b5,b1] is quantifiable holds
( ( for b7 being Element of b2 holds b3,(b4 . ((S_Bound (@ (CQCSub_All [b5,b1],b6))) | b7)) . ((NEx_Val b4,b5,b1,b6) +* (b1 | b7)) |= b5 ) iff for b7 being Element of b2 holds b3,b4 . ((NEx_Val b4,b5,b1,b6) +* (b1 | b7)) |= b5 )
proof end;

theorem Th73: :: SUBLEMMA:73
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] holds dom (NEx_Val b3,b4,b1,b5) = dom (RestrictSub b1,(All b1,(b4 `1 )),b5)
proof end;

theorem Th74: :: SUBLEMMA:74
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1]
for b6 being Element of b2 st [b4,b1] is quantifiable holds
b3 . ((NEx_Val b3,b4,b1,b5) +* (b1 | b6)) = (b3 . (NEx_Val b3,b4,b1,b5)) . (b1 | b6) by FUNCT_4:15;

theorem Th75: :: SUBLEMMA:75
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being Element of CQC-Sub-WFF
for b6 being second_Q_comp of [b5,b1] st [b5,b1] is quantifiable holds
( ( for b7 being Element of b2 holds b3,b4 . ((NEx_Val b4,b5,b1,b6) +* (b1 | b7)) |= b5 ) iff for b7 being Element of b2 holds b3,(b4 . (NEx_Val b4,b5,b1,b6)) . (b1 | b7) |= b5 )
proof end;

theorem Th76: :: SUBLEMMA:76
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being Element of CQC-Sub-WFF
for b6 being second_Q_comp of [b5,b1] holds
( ( for b7 being Element of b2 holds b3,(b4 . (NEx_Val b4,b5,b1,b6)) . (b1 | b7) |= b5 ) iff for b7 being Element of b2 holds b3,(b4 . (NEx_Val b4,b5,b1,b6)) . (b1 | b7) |= b5 `1 )
proof end;

theorem Th77: :: SUBLEMMA:77
canceled;

theorem Th78: :: SUBLEMMA:78
for b1 being Nat
for b2 being non empty set
for b3 being CQC-variable_list of b1
for b4 being Element of Valuations_in b2
for b5, b6, b7 being Val_Sub of b2 st ( for b8 being bound_QC-variable st b8 in dom b6 holds
not b8 in still_not-bound_in b3 ) & ( for b8 being bound_QC-variable st b8 in dom b7 holds
b7 . b8 = b4 . b8 ) & dom b5 misses dom b7 holds
(b4 . b5) *' b3 = (b4 . ((b5 +* b6) +* b7)) *' b3
proof end;

theorem Th79: :: SUBLEMMA:79
for b1 being Nat
for b2 being non empty set
for b3 being interpretation of b2
for b4 being QC-pred_symbol of b1
for b5 being CQC-variable_list of b1
for b6 being Element of Valuations_in b2
for b7, b8, b9 being Val_Sub of b2 st ( for b10 being bound_QC-variable st b10 in dom b8 holds
not b10 in still_not-bound_in (b4 ! b5) ) & ( for b10 being bound_QC-variable st b10 in dom b9 holds
b9 . b10 = b6 . b10 ) & dom b7 misses dom b9 holds
( b3,b6 . b7 |= b4 ! b5 iff b3,b6 . ((b7 +* b8) +* b9) |= b4 ! b5 )
proof end;

theorem Th80: :: SUBLEMMA:80
for b1 being Element of CQC-WFF
for b2 being non empty set
for b3 being interpretation of b2 st ( for b4 being Element of Valuations_in b2
for b5, b6, b7 being Val_Sub of b2 st ( for b8 being bound_QC-variable st b8 in dom b6 holds
not b8 in still_not-bound_in b1 ) & ( for b8 being bound_QC-variable st b8 in dom b7 holds
b7 . b8 = b4 . b8 ) & dom b5 misses dom b7 holds
( b3,b4 . b5 |= b1 iff b3,b4 . ((b5 +* b6) +* b7) |= b1 ) ) holds
for b4 being Element of Valuations_in b2
for b5, b6, b7 being Val_Sub of b2 st ( for b8 being bound_QC-variable st b8 in dom b6 holds
not b8 in still_not-bound_in ('not' b1) ) & ( for b8 being bound_QC-variable st b8 in dom b7 holds
b7 . b8 = b4 . b8 ) & dom b5 misses dom b7 holds
( b3,b4 . b5 |= 'not' b1 iff b3,b4 . ((b5 +* b6) +* b7) |= 'not' b1 )
proof end;

theorem Th81: :: SUBLEMMA:81
for b1, b2 being Element of CQC-WFF
for b3 being non empty set
for b4 being interpretation of b3 st ( for b5 being Element of Valuations_in b3
for b6, b7, b8 being Val_Sub of b3 st ( for b9 being bound_QC-variable st b9 in dom b7 holds
not b9 in still_not-bound_in b1 ) & ( for b9 being bound_QC-variable st b9 in dom b8 holds
b8 . b9 = b5 . b9 ) & dom b6 misses dom b8 holds
( b4,b5 . b6 |= b1 iff b4,b5 . ((b6 +* b7) +* b8) |= b1 ) ) & ( for b5 being Element of Valuations_in b3
for b6, b7, b8 being Val_Sub of b3 st ( for b9 being bound_QC-variable st b9 in dom b7 holds
not b9 in still_not-bound_in b2 ) & ( for b9 being bound_QC-variable st b9 in dom b8 holds
b8 . b9 = b5 . b9 ) & dom b6 misses dom b8 holds
( b4,b5 . b6 |= b2 iff b4,b5 . ((b6 +* b7) +* b8) |= b2 ) ) holds
for b5 being Element of Valuations_in b3
for b6, b7, b8 being Val_Sub of b3 st ( for b9 being bound_QC-variable st b9 in dom b7 holds
not b9 in still_not-bound_in (b1 '&' b2) ) & ( for b9 being bound_QC-variable st b9 in dom b8 holds
b8 . b9 = b5 . b9 ) & dom b6 misses dom b8 holds
( b4,b5 . b6 |= b1 '&' b2 iff b4,b5 . ((b6 +* b7) +* b8) |= b1 '&' b2 )
proof end;

theorem Th82: :: SUBLEMMA:82
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4 being Val_Sub of b3 st ( for b5 being bound_QC-variable st b5 in dom b4 holds
not b5 in still_not-bound_in (All b2,b1) ) holds
for b5 being bound_QC-variable st b5 in (dom b4) \ {b2} holds
not b5 in still_not-bound_in b1
proof end;

theorem Th83: :: SUBLEMMA:83
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Val_Sub of b2
for b5 being Function st ( for b6 being bound_QC-variable st b6 in dom b5 holds
b5 . b6 = b3 . b6 ) & dom b4 misses dom b5 holds
for b6 being bound_QC-variable st b6 in (dom b5) \ {b1} holds
(b5 | ((dom b5) \ {b1})) . b6 = (b3 . b4) . b6
proof end;

theorem Th84: :: SUBLEMMA:84
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being non empty set
for b4 being interpretation of b3 st ( for b5 being Element of Valuations_in b3
for b6, b7, b8 being Val_Sub of b3 st ( for b9 being bound_QC-variable st b9 in dom b7 holds
not b9 in still_not-bound_in b1 ) & ( for b9 being bound_QC-variable st b9 in dom b8 holds
b8 . b9 = b5 . b9 ) & dom b6 misses dom b8 holds
( b4,b5 . b6 |= b1 iff b4,b5 . ((b6 +* b7) +* b8) |= b1 ) ) holds
for b5 being Element of Valuations_in b3
for b6, b7, b8 being Val_Sub of b3 st ( for b9 being bound_QC-variable st b9 in dom b7 holds
not b9 in still_not-bound_in (All b2,b1) ) & ( for b9 being bound_QC-variable st b9 in dom b8 holds
b8 . b9 = b5 . b9 ) & dom b6 misses dom b8 holds
( b4,b5 . b6 |= All b2,b1 iff b4,b5 . ((b6 +* b7) +* b8) |= All b2,b1 )
proof end;

theorem Th85: :: SUBLEMMA:85
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of CQC-WFF
for b4 being Element of Valuations_in b1
for b5, b6, b7 being Val_Sub of b1 st ( for b8 being bound_QC-variable st b8 in dom b6 holds
not b8 in still_not-bound_in b3 ) & ( for b8 being bound_QC-variable st b8 in dom b7 holds
b7 . b8 = b4 . b8 ) & dom b5 misses dom b7 holds
( b2,b4 . b5 |= b3 iff b2,b4 . ((b5 +* b6) +* b7) |= b3 )
proof end;

definition
let c1 be Element of CQC-WFF ;
func RSub1 c1 -> set means :Def11: :: SUBLEMMA:def 11
for b1 being set holds
( b1 in a2 iff ex b2 being bound_QC-variable st
( b2 = b1 & not b2 in still_not-bound_in a1 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being bound_QC-variable st
( b3 = b2 & not b3 in still_not-bound_in c1 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being bound_QC-variable st
( b4 = b3 & not b4 in still_not-bound_in c1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being bound_QC-variable st
( b4 = b3 & not b4 in still_not-bound_in c1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines RSub1 SUBLEMMA:def 11 :
for b1 being Element of CQC-WFF
for b2 being set holds
( b2 = RSub1 b1 iff for b3 being set holds
( b3 in b2 iff ex b4 being bound_QC-variable st
( b4 = b3 & not b4 in still_not-bound_in b1 ) ) );

definition
let c1 be Element of CQC-WFF ;
let c2 be CQC_Substitution;
func RSub2 c1,c2 -> set means :Def12: :: SUBLEMMA:def 12
for b1 being set holds
( b1 in a3 iff ex b2 being bound_QC-variable st
( b2 = b1 & b2 in still_not-bound_in a1 & b2 = (@ a2) . b2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being bound_QC-variable st
( b3 = b2 & b3 in still_not-bound_in c1 & b3 = (@ c2) . b3 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being bound_QC-variable st
( b4 = b3 & b4 in still_not-bound_in c1 & b4 = (@ c2) . b4 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being bound_QC-variable st
( b4 = b3 & b4 in still_not-bound_in c1 & b4 = (@ c2) . b4 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines RSub2 SUBLEMMA:def 12 :
for b1 being Element of CQC-WFF
for b2 being CQC_Substitution
for b3 being set holds
( b3 = RSub2 b1,b2 iff for b4 being set holds
( b4 in b3 iff ex b5 being bound_QC-variable st
( b5 = b4 & b5 in still_not-bound_in b1 & b5 = (@ b2) . b5 ) ) );

theorem Th86: :: SUBLEMMA:86
for b1 being Element of CQC-WFF
for b2 being CQC_Substitution holds dom ((@ b2) | (RSub1 b1)) misses dom ((@ b2) | (RSub2 b1,b2))
proof end;

theorem Th87: :: SUBLEMMA:87
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being CQC_Substitution holds @ (RestrictSub b2,(All b2,b1),b3) = (@ b3) \ (((@ b3) | (RSub1 (All b2,b1))) +* ((@ b3) | (RSub2 (All b2,b1),b3)))
proof end;

theorem Th88: :: SUBLEMMA:88
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being CQC_Substitution holds dom (@ (RestrictSub b2,b1,b3)) misses (dom ((@ b3) | (RSub1 b1))) \/ (dom ((@ b3) | (RSub2 b1,b3)))
proof end;

theorem Th89: :: SUBLEMMA:89
for b1 being bound_QC-variable
for b2 being Element of CQC-Sub-WFF
for b3 being second_Q_comp of [b2,b1] st [b2,b1] is quantifiable holds
@ ((CQCSub_All [b2,b1],b3) `2 ) = ((@ (RestrictSub b1,(All b1,(b2 `1 )),b3)) +* ((@ b3) | (RSub1 (All b1,(b2 `1 ))))) +* ((@ b3) | (RSub2 (All b1,(b2 `1 )),b3))
proof end;

theorem Th90: :: SUBLEMMA:90
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] st [b4,b1] is quantifiable holds
ex b6, b7 being Val_Sub of b2 st
( ( for b8 being bound_QC-variable st b8 in dom b6 holds
not b8 in still_not-bound_in (All b1,(b4 `1 )) ) & ( for b8 being bound_QC-variable st b8 in dom b7 holds
b7 . b8 = b3 . b8 ) & dom (NEx_Val b3,b4,b1,b5) misses dom b7 & b3 . (Val_S b3,(CQCSub_All [b4,b1],b5)) = b3 . (((NEx_Val b3,b4,b1,b5) +* b6) +* b7) )
proof end;

theorem Th91: :: SUBLEMMA:91
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] st [b4,b1] is quantifiable holds
for b6 being Element of Valuations_in b2 holds
( b3,b6 . (NEx_Val b6,b4,b1,b5) |= All b1,(b4 `1 ) iff b3,b6 . (Val_S b6,(CQCSub_All [b4,b1],b5)) |= CQCSub_All [b4,b1],b5 )
proof end;

theorem Th92: :: SUBLEMMA:92
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of CQC-Sub-WFF
for b5 being second_Q_comp of [b4,b1] st [b4,b1] is quantifiable & ( for b6 being Element of Valuations_in b2 holds
( b3,b6 |= CQC_Sub b4 iff b3,b6 . (Val_S b6,b4) |= b4 ) ) holds
for b6 being Element of Valuations_in b2 holds
( b3,b6 |= CQC_Sub (CQCSub_All [b4,b1],b5) iff b3,b6 . (Val_S b6,(CQCSub_All [b4,b1],b5)) |= CQCSub_All [b4,b1],b5 )
proof end;

scheme :: SUBLEMMA:sch 1
s1{ P1[ set ] } :
for b1 being Element of CQC-Sub-WFF holds P1[b1]
provided
E90: for b1, b2 being Element of CQC-Sub-WFF
for b3 being bound_QC-variable
for b4 being second_Q_comp of [b1,b3]
for b5 being Nat
for b6 being CQC-variable_list of b5
for b7 being QC-pred_symbol of b5
for b8 being Element of vSUB holds
( P1[ Sub_P b7,b6,b8] & ( b1 is Sub_VERUM implies P1[b1] ) & ( P1[b1] implies P1[ Sub_not b1] ) & ( b1 `2 = b2 `2 & P1[b1] & P1[b2] implies P1[ CQCSub_& b1,b2] ) & ( [b1,b3] is quantifiable & P1[b1] implies P1[ CQCSub_All [b1,b3],b4] ) )
proof end;

theorem Th93: :: SUBLEMMA:93
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of CQC-Sub-WFF
for b4 being Element of Valuations_in b1 holds
( b2,b4 |= CQC_Sub b3 iff b2,b4 . (Val_S b4,b3) |= b3 )
proof end;