let Al be QC-alphabet ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: (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

proof

let i be Nat; :: thesis: ( i in dom ((v . vS) *' ll) implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )
assume A7: i in dom ((v . vS) *' ll) ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
A8: i in dom ((v . ((vS +* vS1) +* vS2)) *' ll) by A6, A5, A7, FINSEQ_1:def 3;
reconsider i = i as Nat ;
A9: dom ((v . ((vS +* vS1) +* vS2)) *' ll) c= dom ll by RELAT_1:25;

A10: now :: thesis: ( ll . i in dom ((vS +* vS1) +* vS2) implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )

reconsider x = ll . i as bound_QC-variable of Al by A8, A9, Th5;
assume A11: ll . i in dom ((vS +* vS1) +* vS2) ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i

A12: now :: thesis: ( not x in dom vS2 implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )

A13: now :: thesis: not x in dom vS1

len ll = k by SUBSTUT1:34;
then A14: i <= len ll by A5, A7, FINSEQ_1:1;
1 <= i by A5, A7, FINSEQ_1:1;
then x in { (ll . n) where n is Nat : ( 1 <= n & n <= len ll & ll . n in bound_QC-variables Al ) } by A14;
then A15: x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:def 1;
assume x in dom vS1 ; :: thesis: contradiction
then not x in still_not-bound_in ll by A1;
hence contradiction by A15, QC_LANG3:2; :: thesis: verum

end;

assume A16: not x in dom vS2 ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then A17: ((vS +* vS1) +* vS2) . x = (vS +* vS1) . x by FUNCT_4:11;
A18: x in dom (vS +* vS1) by A11, A16, FUNCT_4:12;

now :: thesis: ( not x in dom vS1 implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )

assume A19: not x in dom vS1 ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then ((vS +* vS1) +* vS2) . x = vS . x by A17, FUNCT_4:11;
then A20: (v +* ((vS +* vS1) +* vS2)) . x = vS . x by A11, FUNCT_4:13;
x in dom vS by A18, A19, FUNCT_4:12;
then (v . ((vS +* vS1) +* vS2)) . x = (v +* vS) . x by A20, FUNCT_4:13;
then ((v . ((vS +* vS1) +* vS2)) *' ll) . i = (v . vS) . x by A8, FUNCT_1:12;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A7, FUNCT_1:12; :: thesis: verum

end;

hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A13; :: thesis: verum

end;

now :: thesis: ( x in dom vS2 implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )

assume A21: x in dom vS2 ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then ((vS +* vS1) +* vS2) . x = vS2 . x by FUNCT_4:13;
then ((vS +* vS1) +* vS2) . x = v . x by A2, A21;
then (v +* ((vS +* vS1) +* vS2)) . x = v . x by A11, FUNCT_4:13;
then A22: ((v . ((vS +* vS1) +* vS2)) *' ll) . i = v . x by A8, FUNCT_1:12;
not x in dom vS by A3, A21, XBOOLE_0:3;
then (v +* vS) . x = v . x by FUNCT_4:11;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A7, A22, FUNCT_1:12; :: thesis: verum

end;

hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A12; :: thesis: verum

end;

now :: thesis: ( not ll . i in dom ((vS +* vS1) +* vS2) implies ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i )

assume A23: not ll . i in dom ((vS +* vS1) +* vS2) ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then not ll . i in dom (vS +* vS1) by FUNCT_4:12;
then not ll . i in dom vS by FUNCT_4:12;
then (v +* vS) . (ll . i) = v . (ll . i) by FUNCT_4:11;
then A24: ((v . vS) *' ll) . i = v . (ll . i) by A7, FUNCT_1:12;
(v +* ((vS +* vS1) +* vS2)) . (ll . i) = v . (ll . i) by A23, FUNCT_4:11;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A8, A24, FUNCT_1:12; :: thesis: verum

end;

hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A10; :: thesis: verum

end;

hence (v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll by A4, A6, FINSEQ_2:9; :: thesis: verum