let x be bound_QC-variable; :: thesis:
let A be non empty set ; :: thesis:
let v be Element of Valuations_in A; :: thesis:
let S be Element of CQC-Sub-WFF ; :: thesis:
let xSQ be second_Q_comp of [S,x]; :: thesis:
let a be Element of A; :: thesis:
assume A1: [S,x] is quantifiable ; :: thesis:
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 );
A2: 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 A3: 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 A2, FUNCT_4:def 1;

A4: now

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

A7: now

assume A8: b <> S_Bound (@ (CQCSub_All [S,x],xSQ)) ; :: thesis:

A9: now

assume A10: not b in dom (NEx_Val v,S,x,xSQ) ; :: thesis:
not b in {x} by A5, A8, TARSKI:def 1;
then not b in dom (x | a) by Th59;
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;
then A12: ((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 FUNCT_4:12;
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 . x by A8, A12, 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:

end;

now

assume A13: b in dom (NEx_Val v,S,x,xSQ) ; :: thesis:
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 A14: dom (NEx_Val v,S,x,xSQ) 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 A13, 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, A14, FUNCT_4:14; :: thesis:

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:

end;

now

assume b = S_Bound (@ (CQCSub_All [S,x],xSQ)) ; :: thesis:
then b in {x} by A5, TARSKI:def 1;
then A15: 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 A16: 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 A15, 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 A15, A16, FUNCT_4:14; :: thesis:

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:

end;

end;

now

assume A17: x in rng (RestrictSub x,(All x,(S `1 )),xSQ) ; :: thesis:
A18: 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 A2, RELAT_1:90;
B19: 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 A3, RELAT_1:90;
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

let b be set ; :: thesis:
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:
A21: ( b in (dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) \/ (dom ((NEx_Val v,S,x,xSQ) +* (x | a))) & b in still_not-bound_in (S `1 ) ) by A18, A20, XBOOLE_0:def 4;
still_not-bound_in (S `1 ) c= Bound_Vars (S `1 ) by Th48;
then A22: b <> S_Bound (@ (CQCSub_All [S,x],xSQ)) by A1, A17, A21, Th39;
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;
A24: (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;
A25: 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 A23, FUNCT_4:def 1;

A26: now

assume A27: not b in dom (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) ; :: thesis:
then A28: (((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, FUNCT_4:12;
A29: b in dom ((v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) | (still_not-bound_in (S `1 ))) by A20, A25, A27, XBOOLE_0:def 3;
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 A28, 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 A22, Th49;
A31: ((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 A24, A27, FUNCT_4:12;
b in (dom (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) /\ (still_not-bound_in (S `1 )) by A29, RELAT_1:90;
then ( b in bound_QC-variables & b in still_not-bound_in (S `1 ) ) by XBOOLE_0:def 4;
then ( b in dom v & b in still_not-bound_in (S `1 ) ) by Th59;
then b in (dom v) /\ (still_not-bound_in (S `1 )) by XBOOLE_0:def 4;
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, A31, FUNCT_1:71; :: thesis:

end;

now

assume A32: b in dom (((NEx_Val v,S,x,xSQ) +* (x | a)) | (still_not-bound_in (S `1 ))) ; :: thesis:
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 A24, A32, FUNCT_4:14; :: thesis:

end;

end;