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