let x be bound_QC-variable; :: thesis: for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
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 ))
let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
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 ))
let v be Element of Valuations_in A; :: thesis: for S being Element of CQC-Sub-WFF
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 ))
let S be Element of CQC-Sub-WFF ; :: thesis: 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 ))
let xSQ be second_Q_comp of [S,x]; :: thesis: 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 ))
let a be Element of A; :: thesis: ( [S,x] is quantifiable implies ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 )) = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 )) )
set S1 = CQCSub_All [S,x],xSQ;
set z = S_Bound (@ (CQCSub_All [S,x],xSQ));
set finSub = RestrictSub x,(All x,(S `1 )),xSQ;
set V1 = (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a));
set V2 = v . ((NEx_Val v,S,x,xSQ) +* (x | a));
set X = still_not-bound_in (S `1 );
A1: dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) = (dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) \/ (dom ((NEx_Val v,S,x,xSQ) +* (x | a))) by FUNCT_4:def 1;
dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) = bound_QC-variables by Th59;
then dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) = dom v by Th59;
then A2: dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) = dom (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) by A1, FUNCT_4:def 1;
assume A3: [S,x] is quantifiable ; :: thesis: ((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 ))

A4: now

assume not x in rng (RestrictSub x,(All x,(S `1 )),xSQ) ; :: thesis: ((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 ))
then A5: S_Bound (@ (CQCSub_All [S,x],xSQ)) = x by A3, Th53;
for b being set st b in dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) holds
((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b

proof

let b be set ; :: thesis: ( b in dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) implies ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b )
assume A6: b in dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b

A7: now

assume A8: b <> S_Bound (@ (CQCSub_All [S,x],xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b

A9: now

not b in {x} by A5, A8, TARSKI:def 1;
then A10: not b in dom (x | a) by Th59;
assume not b in dom (NEx_Val v,S,x,xSQ) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b
then not b in (dom (NEx_Val v,S,x,xSQ)) \/ (dom (x | a)) by A10, XBOOLE_0:def 3;
then A11: not b in dom ((NEx_Val v,S,x,xSQ) +* (x | a)) by FUNCT_4:def 1;
reconsider x = b as bound_QC-variable by A6;
((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . b by A11, FUNCT_4:12;
then ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = v . x by A8, Th49;
hence ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b by A11, FUNCT_4:12; :: thesis: verum

end;

now

dom ((NEx_Val v,S,x,xSQ) +* (x | a)) = (dom (NEx_Val v,S,x,xSQ)) \/ (dom (x | a)) by FUNCT_4:def 1;
then A12: dom (NEx_Val v,S,x,xSQ) c= dom ((NEx_Val v,S,x,xSQ) +* (x | a)) by XBOOLE_1:7;
assume A13: b in dom (NEx_Val v,S,x,xSQ) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b
then ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = ((NEx_Val v,S,x,xSQ) +* (x | a)) . b by A12, FUNCT_4:14;
hence ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b by A13, A12, FUNCT_4:14; :: thesis: verum

end;

hence ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b by A9; :: thesis: verum

end;

now

assume b = S_Bound (@ (CQCSub_All [S,x],xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b
then b in {x} by A5, TARSKI:def 1;
then A14: b in dom (x | a) by Th59;
dom ((NEx_Val v,S,x,xSQ) +* (x | a)) = (dom (NEx_Val v,S,x,xSQ)) \/ (dom (x | a)) by FUNCT_4:def 1;
then A15: dom (x | a) c= dom ((NEx_Val v,S,x,xSQ) +* (x | a)) by XBOOLE_1:7;
then ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = ((NEx_Val v,S,x,xSQ) +* (x | a)) . b by A14, FUNCT_4:14;
hence ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b by A14, A15, FUNCT_4:14; :: thesis: verum

end;

hence ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b = (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) . b by A7; :: thesis: verum

end;

hence ((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 )) by A2, FUNCT_1:9; :: thesis: verum

end;

now

assume A16: x in rng (RestrictSub x,(All x,(S `1 )),xSQ) ; :: thesis: ((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 ))
A17: dom (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) = ((dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) \/ (dom ((NEx_Val v,S,x,xSQ) +* (x | a)))) /\ (still_not-bound_in (S `1 )) by A1, RELAT_1:90;
A18: for b being set st b in dom (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) holds
(((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b

proof

A19: still_not-bound_in (S `1 ) c= Bound_Vars (S `1 ) by Th48;
let b be set ; :: thesis: ( b in dom (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) implies (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b )
assume A20: b in dom (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b
b in still_not-bound_in (S `1 ) by A17, A20, XBOOLE_0:def 4;
then A21: b <> S_Bound (@ (CQCSub_All [S,x],xSQ)) by A3, A16, A19, Th39;
A22: (v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 )) = (v | (still_not-bound_in (S `1 ))) +* (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) by FUNCT_4:75;
A23: ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 )) = ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) | (still_not-bound_in (S `1 ))) +* (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) by FUNCT_4:75;
then A24: dom (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) = (dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) | (still_not-bound_in (S `1 )))) \/ (dom (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 )))) by FUNCT_4:def 1;

A25: now

assume A26: not b in dom (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b
then A27: b in dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) | (still_not-bound_in (S `1 ))) by A20, A24, XBOOLE_0:def 3;
then b in (dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) /\ (still_not-bound_in (S `1 )) by RELAT_1:90;
then A28: b in still_not-bound_in (S `1 ) by XBOOLE_0:def 4;
b in bound_QC-variables by A20;
then b in dom v by Th59;
then A29: b in (dom v) /\ (still_not-bound_in (S `1 )) by A28, XBOOLE_0:def 4;
(((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) | (still_not-bound_in (S `1 ))) . b by A23, A26, FUNCT_4:12;
then (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . b by A27, FUNCT_1:70;
then A30: (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = v . b by A21, Th49;
((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = (v | (still_not-bound_in (S `1 ))) . b by A22, A26, FUNCT_4:12;
hence (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b by A30, A29, FUNCT_1:71; :: thesis: verum

end;

now

assume A31: b in dom (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b
then (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) . b by A23, FUNCT_4:14;
hence (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b by A22, A31, FUNCT_4:14; :: thesis: verum

end;

hence (((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b = ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) . b by A25; :: thesis: verum

end;

dom ((v . ((NEx_Val v,S,x,xSQ) +* (x | a))) | (still_not-bound_in (S `1 ))) = (dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a)))) /\ (still_not-bound_in (S `1 )) by A2, RELAT_1:90;
hence ((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 )) by A18, FUNCT_1:9, RELAT_1:90; :: thesis: verum

end;

hence ((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 )) by A4; :: thesis: verum