let Al be QC-alphabet ; :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let x be bound_QC-variable of Al; :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let A be non empty set ; :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let v be Element of Valuations_in (Al,A); :: thesis: 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) & dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
let S be Element of CQC-Sub-WFF Al; :: 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, Th41;

A3: now :: thesis: ( not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies ( 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) ) )

reconsider F = {[x,x]} as Function ;
assume A4: 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 A5: @ (S `2) = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by SUBSTUT1:def 2;

A6: now :: thesis: dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x}

set q = All (x,(S `1));
set X = { y1 where y1 is bound_QC-variable of Al : ( 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} <> {} ;
then consider b being object such that
A7: 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 of Al : ( 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 of Al : ( 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 of Al : ( 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 of Al : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by RELAT_1:61;
then A8: dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= { y1 where y1 is bound_QC-variable of Al : ( 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 A7, 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 of Al : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by A8;
then A9: ex y being bound_QC-variable of Al 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 A7, XBOOLE_0:def 4;
hence contradiction by A9, 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:9;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) misses dom F by A6, SUBSTUT1:def 2;
then A10: (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) \/ F = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F by FUNCT_4:31;
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then A11: ex f being Function st
( v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 2;
A12: rng F = {x} by RELAT_1:9;
then dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = dom F by A11, RELAT_1:27;
then A13: dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = {x} by RELAT_1:9;
A14: {[x,x]} = x .--> x by FUNCT_4:82;
for b being object 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 object ; :: thesis: ( b in dom (x | a) implies (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b )
assume A15: b in dom (x | a) ; :: thesis: (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b
A16: (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (F . b) by A13, A15, FUNCT_1:12;
b = x by A15, TARSKI:def 1;
then ( (x | a) . b = a & F . b = x ) by A14, FUNCOP_1:72;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b by A1, A4, A16, Th49, Th52; :: thesis: verum

end;

then A17: x | a = F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) by A13, FUNCT_1:2;
((@ (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 A11, A12, FUNCT_7:9;
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 A10, A5, A17, SUBSTUT1:def 2; :: thesis: verum

end;

now :: thesis: ( x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies ( 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) ) )

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

A19: now :: thesis: not dom (RestrictSub (x,(All (x,(S `1))),xSQ)) meets {x}

set q = All (x,(S `1));
set X = { y1 where y1 is bound_QC-variable of Al : ( 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 object such that
A20: b in dom (RestrictSub (x,(All (x,(S `1))),xSQ)) and
A21: b in {x} by XBOOLE_0:3;
RestrictSub (x,(All (x,(S `1))),xSQ) = xSQ | { y1 where y1 is bound_QC-variable of Al : ( 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 of Al : ( 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 of Al : ( 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 of Al : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by RELAT_1:61;
then A22: dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= { y1 where y1 is bound_QC-variable of Al : ( 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 A20, SUBSTUT1:def 2;
then b in { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,(S `1))) & y1 is Element of dom xSQ & y1 <> x & y1 <> xSQ . y1 ) } by A22;
then ex y being bound_QC-variable of Al 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 A21, 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:9;
then dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) misses dom F by A19, SUBSTUT1:def 2;
then A23: (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) \/ F = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* F by FUNCT_4:31;
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then A24: ex f being Function st
( v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) = f & dom f = bound_QC-variables Al & 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:9;
then dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = dom F by A24, RELAT_1:27;
then A25: dom (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) = {x} by RELAT_1:9;
A26: {[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:82;
for b being object 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 object ; :: thesis: ( b in dom (x | a) implies (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b )
assume A27: b in dom (x | a) ; :: thesis: (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b
A28: (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (F . b) by A25, A27, FUNCT_1:12;
b = x by A27, TARSKI:def 1;
then ( (x | a) . b = a & F . b = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))) ) by A26, FUNCOP_1:72;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) . b by A1, A18, A28, Th49, Th51; :: thesis: verum

end;

then A29: x | a = F * (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) by A25, FUNCT_1:2;
rng F = {(x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))))} by RELAT_1:9;
then A30: ((@ (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 A24, FUNCT_7:9;
S `2 = (RestrictSub (x,(All (x,(S `1))),xSQ)) \/ F by A2, A18, 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 A23, A30, A29, 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