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] 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
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] 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
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] 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let S be Element of CQC-Sub-WFF ; :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} ) )
assume A1: [S,x] is quantifiable ; :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
set finSub = RestrictSub (x,(All (x,(S `1))),xSQ);
let a be Element of A; :: thesis: ( 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
set S1 = CQCSub_All ([S,x],xSQ);
set z = S_Bound (@ (CQCSub_All ([S,x],xSQ)));
A2: S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ))) by A1, Th42;

A3: now

reconsider F = {[x,x]} as Function ;
A4: dom (x | a) = {x} by FUNCOP_1:19;
assume A5: not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: ( dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} & 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) )
then S `2 = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by A2, SUBSTUT1:def 13;
then A6: @ (S `2) = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by SUBSTUT1:def 2;

A7: now

set q = All (x,(S `1));
set X = { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } ;
assume not dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} ; :: thesis: contradiction
then (dom (RestrictSub (x,(All (x,(S `1))),xSQ))) /\ {x} <> {} by XBOOLE_0:def 7;
then consider b being set such that
A8: b in (dom (RestrictSub (x,(All (x,(S `1))),xSQ))) /\ {x} by XBOOLE_0:def 1;
RestrictSub (x,(All (x,(S `1))),xSQ) = xSQ | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 6;
then RestrictSub (x,(All (x,(S `1))),xSQ) = (@ xSQ) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 2;
then @ (RestrictSub (x,(All (x,(S `1))),xSQ)) = (@ xSQ) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 2;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) = (dom (@ xSQ)) /\ { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by RELAT_1:90;
then A9: dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by XBOOLE_1:17;
b in dom (RestrictSub (x,(All (x,(S `1))),xSQ)) by A8, XBOOLE_0:def 4;
then b in dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) by SUBSTUT1:def 2;
then b in { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by A9;
then A10: ex y being bound_QC-variable st
( y = b & y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) ;
b in {x} by A8, XBOOLE_0:def 4;
hence contradiction by A10, TARSKI:def 1; :: thesis: verum

end;

hence dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} ; :: thesis: 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)
dom {[x,x]} = {x} by RELAT_1:23;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) misses dom F by A7, SUBSTUT1:def 2;
then A11: (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) \/ F = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F by FUNCT_4:32;
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) is Element of Funcs (bound_QC-variables,A) by VALUAT_1:def 1;
then A12: ex f being Function st
( v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) = f & dom f = bound_QC-variables & rng f c= A ) by FUNCT_2:def 2;
A13: rng F = {x} by RELAT_1:23;
then dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = dom F by A12, RELAT_1:46;
then A14: dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = {x} by RELAT_1:23;
A15: {[x,x]} = x .--> x by FUNCT_4:87;
for b being set st b in dom (x | a) holds
(x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b

proof

let b be set ; :: thesis: ( b in dom (x | a) implies (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b )
assume A16: b in dom (x | a) ; :: thesis: (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b
b in dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) by A14, A16, FUNCOP_1:19;
then A17: (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (F . b) by FUNCT_1:22;
b = x by A4, A16, TARSKI:def 1;
then ( (x | a) . b = a & F . b = x ) by A15, FUNCOP_1:87;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b by A1, A5, A17, Th50, Th53; :: thesis: verum

end;

then A18: x | a = F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) by A14, FUNCOP_1:19, FUNCT_1:9;
((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F) * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) = ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) +* (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) by A12, A13, FUNCT_7:10;
hence 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) by A11, A6, A18, SUBSTUT1:def 2; :: thesis: verum

end;

now

reconsider F = {[x,(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))]} as Function ;
assume A19: x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: ( dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} & 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) )

A20: now

set q = All (x,(S `1));
set X = { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } ;
assume dom (RestrictSub (x,(All (x,(S `1))),xSQ)) meets {x} ; :: thesis: contradiction
then consider b being set such that
A21: b in dom (RestrictSub (x,(All (x,(S `1))),xSQ)) and
A22: b in {x} by XBOOLE_0:3;
RestrictSub (x,(All (x,(S `1))),xSQ) = xSQ | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 6;
then RestrictSub (x,(All (x,(S `1))),xSQ) = (@ xSQ) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 2;
then @ (RestrictSub (x,(All (x,(S `1))),xSQ)) = (@ xSQ) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by SUBSTUT1:def 2;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) = (dom (@ xSQ)) /\ { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by RELAT_1:90;
then A23: dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by XBOOLE_1:17;
b in dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) by A21, SUBSTUT1:def 2;
then b in { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by A23;
then ex y being bound_QC-variable st
( y = b & y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) ;
hence contradiction by A22, TARSKI:def 1; :: thesis: verum

end;

hence dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} ; :: thesis: 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)
dom {[x,(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))]} = {x} by RELAT_1:23;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) misses dom F by A20, SUBSTUT1:def 2;
then A24: (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) \/ F = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F by FUNCT_4:32;
A25: dom (x | a) = {x} by FUNCOP_1:19;
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) is Element of Funcs (bound_QC-variables,A) by VALUAT_1:def 1;
then A26: ex f being Function st
( v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) = f & dom f = bound_QC-variables & rng f c= A ) by FUNCT_2:def 2;
rng F = {(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))} by RELAT_1:23;
then dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = dom F by A26, RELAT_1:46;
then A27: dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = {x} by RELAT_1:23;
A28: {[x,(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))]} = x .--> (x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))) by FUNCT_4:87;
for b being set st b in dom (x | a) holds
(x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b

proof

let b be set ; :: thesis: ( b in dom (x | a) implies (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b )
assume A29: b in dom (x | a) ; :: thesis: (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b
b in dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) by A27, A29, FUNCOP_1:19;
then A30: (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (F . b) by FUNCT_1:22;
b = x by A25, A29, TARSKI:def 1;
then ( (x | a) . b = a & F . b = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))) ) by A28, FUNCOP_1:87;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b by A1, A19, A30, Th50, Th52; :: thesis: verum

end;

then A31: x | a = F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) by A27, FUNCOP_1:19, FUNCT_1:9;
rng F = {(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))} by RELAT_1:23;
then A32: ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F) * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) = ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) +* (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) by A26, FUNCT_7:10;
S `2 = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by A2, A19, SUBSTUT1:def 13;
then @ (S `2) = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by SUBSTUT1:def 2;
hence 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) by A24, A32, A31, SUBSTUT1:def 2; :: thesis: verum

end;

hence ( 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} ) by A3; :: thesis: verum