let Al be QC-alphabet ; for k being Nat
for A being non empty set
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, 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 ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
let k be Nat; for A being non empty set
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, 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 ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
let A be non empty set ; for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, 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 ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
let ll be CQC-variable_list of k,Al; for v being Element of Valuations_in (Al,A)
for vS, 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 ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
let v be Element of Valuations_in (Al,A); for vS, 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 ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
let vS, vS1, vS2 be Val_Sub of A,Al; ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ll ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 implies (v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll )
assume that
A1:
for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ll
and
A2:
for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y
and
A3:
dom vS misses dom vS2
; (v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
set ll2 = (v . ((vS +* vS1) +* vS2)) *' ll;
set ll1 = (v . vS) *' ll;
A4:
len ((v . vS) *' ll) = k
by VALUAT_1:def 3;
then A5:
dom ((v . vS) *' ll) = Seg k
by FINSEQ_1:def 3;
A6:
len ((v . ((vS +* vS1) +* vS2)) *' ll) = k
by VALUAT_1:def 3;
for i being Nat st i in dom ((v . vS) *' ll) holds
((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
hence
(v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
by A4, A6, FINSEQ_2:9; verum