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
ex vS1, vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
ex vS1, vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 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
ex vS1, vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
ex vS1, vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 Th89;
take vS1 = ((@ xSQ) | (RSub1 (All x,(S `1 )))) * v; :: thesis: ex vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 ;
then A2: rng ((@ xSQ) | (RSub1 (All x,(S `1 )))) c= dom v by Th59;
thus for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) :: thesis: ( ( for y being bound_QC-variable 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; :: 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:46;
then y in (dom (@ xSQ)) /\ (RSub1 (All x,(S `1 ))) by RELAT_1:90;
then y in RSub1 (All x,(S `1 )) by XBOOLE_0:def 4;
then ex y1 being bound_QC-variable st
( y1 = y & not y1 in still_not-bound_in (All x,(S `1 )) ) by Def10;
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 ;
then A3: rng ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) c= dom v by Th59;
thus for y being bound_QC-variable 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; :: 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:46;
then y in (dom (@ xSQ)) /\ (RSub2 (All x,(S `1 )),xSQ) by RELAT_1:90;
then y in RSub2 (All x,(S `1 )),xSQ by XBOOLE_0:def 4;
then ex y1 being bound_QC-variable st
( y1 = y & y1 in still_not-bound_in (All x,(S `1 )) & y1 = (@ xSQ) . y1 ) by Def11;
then v . y = v . (((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) . y) by A4, FUNCT_1:70;
hence vS2 . y = v . y by A4, FUNCT_1:23; :: 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 : ( 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 : ( 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 : ( 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 : ( y in still_not-bound_in (All x,(S `1 )) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } ) by Th73;
then A5: dom (NEx_Val v,S,x,xSQ) = (dom (@ xSQ)) /\ { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,(S `1 )) & y is Element of dom xSQ & y <> x & y <> xSQ . y ) } by RELAT_1:90;
dom vS2 = dom ((@ xSQ) | (RSub2 (All x,(S `1 )),xSQ)) by A3, RELAT_1:46;
then A6: dom vS2 = (dom (@ xSQ)) /\ (RSub2 (All x,(S `1 )),xSQ) by RELAT_1:90;

now

assume dom (NEx_Val v,S,x,xSQ) meets dom vS2 ; :: thesis: contradiction
then consider b being set 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 : ( 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 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 st
( y1 = b & y1 in still_not-bound_in (All x,(S `1 )) & y1 = (@ xSQ) . y1 ) by Def11;
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:10;
hence v . (Val_S v,(CQCSub_All [S,x],xSQ)) = v . (((NEx_Val v,S,x,xSQ) +* vS1) +* vS2) by A1, A3, FUNCT_7:10; :: thesis: verum