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

A3: now

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

proof

now

assume dom (RestrictSub x,(All x,(S `1 )),xSQ) meets {x} ; :: thesis:
then consider b being set such that
A7: ( b in dom (RestrictSub x,(All x,(S `1 )),xSQ) & b in {x} ) by XBOOLE_0:3;
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 ) } ;
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 A8: 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 A7, 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 A8;
then consider y being bound_QC-variable such that
A9: ( y = b & y in still_not-bound_in (All x,(S `1 )) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) ;
thus contradiction by A7, A9, TARSKI:def 1; :: thesis:

end;

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

end;

then dom (@ (RestrictSub x,(All x,(S `1 )),xSQ)) misses dom F by A5, SUBSTUT1:def 2;
then A10: (@ (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 consider f being Function such that
A11: ( 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. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 )))} by RELAT_1:23;
rng F = {(x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 )))} by RELAT_1:23;
then A14: ((@ (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, FUNCT_7:10;
S `2 = (RestrictSub x,(All x,(S `1 )),xSQ) \/ F by A2, A4, SUBSTUT1:def 13;
then A15: @ (S `2 ) = (RestrictSub x,(All x,(S `1 )),xSQ) \/ F by SUBSTUT1:def 2;
x | a = F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))

proof

A16: dom (x | a) = {x} by FUNCOP_1:19;
dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) = dom F by A11, A13, RELAT_1:46;
then A17: dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) = {x} by RELAT_1:23;
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:
assume A18: b in dom (x | a) ; :: thesis:
A19: b = x by A16, A18, TARSKI:def 1;
then A20: (x | a) . b = a by FUNCOP_1:87;
b in dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) by A17, A18, FUNCOP_1:19;
then A21: (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;
F . b = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 )) by A6, A19, FUNCOP_1:87;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) . b by A1, A4, A20, A21, Th50, Th52; :: thesis:

end;

hence x | a = F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) by A17, FUNCOP_1:19, FUNCT_1:9; :: thesis:

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) by A10, A14, A15, SUBSTUT1:def 2; :: thesis:

end;

now

assume A22: not x in rng (RestrictSub x,(All x,(S `1 )),xSQ) ; :: thesis:
A23: dom {[x,x]} = {x} by RELAT_1:23;
A24: {[x,x]} = x .--> x by FUNCT_4:87;
reconsider F = {[x,x]} as Function ;
thus dom (RestrictSub x,(All x,(S `1 )),xSQ) misses {x} :: thesis:

proof

now

assume not dom (RestrictSub x,(All x,(S `1 )),xSQ) misses {x} ; :: thesis:
then (dom (RestrictSub x,(All x,(S `1 )),xSQ)) /\ {x} <> {} by XBOOLE_0:def 7;
then consider b being set such that
A25: b in (dom (RestrictSub x,(All x,(S `1 )),xSQ)) /\ {x} by XBOOLE_0:def 1;
A26: ( b in dom (RestrictSub x,(All x,(S `1 )),xSQ) & b in {x} ) by A25, XBOOLE_0:def 4;
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 ) } ;
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 A27: 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 A26, 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 A27;
then consider y being bound_QC-variable such that
A28: ( y = b & y in still_not-bound_in (All x,(S `1 )) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) ;
thus contradiction by A26, A28, TARSKI:def 1; :: thesis:

end;

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

end;

then dom (@ (RestrictSub x,(All x,(S `1 )),xSQ)) misses dom F by A23, SUBSTUT1:def 2;
then A29: (@ (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 consider f being Function such that
A30: ( v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a) = f & dom f = bound_QC-variables & rng f c= A ) by FUNCT_2:def 2;
A32: rng F = {x} by RELAT_1:23;
then A33: ((@ (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 A30, FUNCT_7:10;
S `2 = (RestrictSub x,(All x,(S `1 )),xSQ) \/ F by A2, A22, SUBSTUT1:def 13;
then A34: @ (S `2 ) = (RestrictSub x,(All x,(S `1 )),xSQ) \/ F by SUBSTUT1:def 2;
x | a = F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))

proof

A35: dom (x | a) = {x} by FUNCOP_1:19;
dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) = dom F by A30, A32, RELAT_1:46;
then A36: dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) = {x} by RELAT_1:23;
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:
assume A37: b in dom (x | a) ; :: thesis:
A38: b = x by A35, A37, TARSKI:def 1;
then A39: (x | a) . b = a by FUNCOP_1:87;
b in dom (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) by A36, A37, FUNCOP_1:19;
then A40: (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;
F . b = x by A24, A38, FUNCOP_1:87;
hence (x | a) . b = (F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a))) . b by A1, A22, A39, A40, Th50, Th53; :: thesis:

end;

hence x | a = F * (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) by A36, FUNCOP_1:19, FUNCT_1:9; :: thesis:

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) by A29, A33, A34, SUBSTUT1:def 2; :: thesis:

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: