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
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
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
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
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
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
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
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
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
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) ) )
set S1 = CQCSub_All ([S,x],xSQ);
assume [S,x] is quantifiable ; :: thesis: ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
then A1: Val_S (v,(CQCSub_All ([S,x],xSQ))) = (((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* ((@ xSQ) | (RSub1 (All (x,(S `1)))))) +* ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))) * v by Th85;
take vS1 = ((@ xSQ) | (RSub1 (All (x,(S `1))))) * v; :: thesis: ex vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
take vS2 = ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) * v; :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
rng ((@ xSQ) | (RSub1 (All (x,(S `1))))) c= bound_QC-variables Al ;
then A2: rng ((@ xSQ) | (RSub1 (All (x,(S `1))))) c= dom v by Th58;
thus for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )

proof

let y be bound_QC-variable of Al; :: thesis: ( y in dom vS1 implies not y in still_not-bound_in (All (x,(S `1))) )
assume y in dom vS1 ; :: thesis: not y in still_not-bound_in (All (x,(S `1)))
then y in dom ((@ xSQ) | (RSub1 (All (x,(S `1))))) by A2, RELAT_1:27;
then y in (dom (@ xSQ)) /\ (RSub1 (All (x,(S `1)))) by RELAT_1:61;
then y in RSub1 (All (x,(S `1))) by XBOOLE_0:def 4;
then ex y1 being bound_QC-variable of Al st
( y1 = y & not y1 in still_not-bound_in (All (x,(S `1))) ) by Def9;
hence not y in still_not-bound_in (All (x,(S `1))) ; :: thesis: verum

end;

rng ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) c= bound_QC-variables Al ;
then A3: rng ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) c= dom v by Th58;
thus for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y :: thesis: ( dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 & v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )

proof

let y be bound_QC-variable of Al; :: thesis: ( y in dom vS2 implies vS2 . y = v . y )
assume y in dom vS2 ; :: thesis: vS2 . y = v . y
then A4: y in dom ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) by A3, RELAT_1:27;
then y in (dom (@ xSQ)) /\ (RSub2 ((All (x,(S `1))),xSQ)) by RELAT_1:61;
then y in RSub2 ((All (x,(S `1))),xSQ) by XBOOLE_0:def 4;
then ex y1 being bound_QC-variable of Al st
( y1 = y & y1 in still_not-bound_in (All (x,(S `1))) & y1 = (@ xSQ) . y1 ) by Def10;
then v . y = v . (((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) . y) by A4, FUNCT_1:47;
hence vS2 . y = v . y by A4, FUNCT_1:13; :: thesis: verum

end;

thus dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 :: thesis: v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2)

proof

set X = { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } ;
RestrictSub (x,(All (x,(S `1))),xSQ) = xSQ | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } by SUBSTUT1:def 6;
then RestrictSub (x,(All (x,(S `1))),xSQ) = (@ xSQ) | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } by SUBSTUT1:def 2;
then dom (NEx_Val (v,S,x,xSQ)) = dom ((@ xSQ) | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } ) by Th71;
then A5: dom (NEx_Val (v,S,x,xSQ)) = (dom (@ xSQ)) /\ { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } by RELAT_1:61;
dom vS2 = dom ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ))) by A3, RELAT_1:27;
then A6: dom vS2 = (dom (@ xSQ)) /\ (RSub2 ((All (x,(S `1))),xSQ)) by RELAT_1:61;

now :: thesis: not dom (NEx_Val (v,S,x,xSQ)) meets dom vS2

assume dom (NEx_Val (v,S,x,xSQ)) meets dom vS2 ; :: thesis: contradiction
then consider b being object such that
A7: b in dom (NEx_Val (v,S,x,xSQ)) and
A8: b in dom vS2 by XBOOLE_0:3;
b in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,(S `1))) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } by A5, A7, XBOOLE_0:def 4;
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 RSub2 ((All (x,(S `1))),xSQ) by A6, A8, XBOOLE_0:def 4;
then ex y1 being bound_QC-variable of Al st
( y1 = b & y1 in still_not-bound_in (All (x,(S `1))) & y1 = (@ xSQ) . y1 ) by Def10;
hence contradiction by A9, SUBSTUT1:def 2; :: thesis: verum

end;

hence dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 ; :: thesis: verum

end;

((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* ((@ xSQ) | (RSub1 (All (x,(S `1)))))) * v = ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v) +* (((@ xSQ) | (RSub1 (All (x,(S `1))))) * v) by A2, FUNCT_7:9;
hence v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) by A1, A3, FUNCT_7:9; :: thesis: verum