let k be Element of NAT ; :: thesis: for A being non empty set
for ll being CQC-variable_list of
for v being Element of Valuations_in A
for vS, 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 ll ) & ( for y being bound_QC-variable 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
for v being Element of Valuations_in A
for vS, 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 ll ) & ( for y being bound_QC-variable 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 ; :: thesis: for v being Element of Valuations_in A
for vS, 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 ll ) & ( for y being bound_QC-variable 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 A; :: thesis: for vS, 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 ll ) & ( for y being bound_QC-variable 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; :: thesis: ( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ll ) & ( for y being bound_QC-variable 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 A1: ( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ll ) & ( for y being bound_QC-variable st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 ) ; :: thesis: (v . vS) *' ll = (v . ((vS +* vS1) +* vS2)) *' ll
set ll1 = (v . vS) *' ll;
set ll2 = (v . ((vS +* vS1) +* vS2)) *' ll;
A2: ( len ((v . vS) *' ll) = k & len ((v . ((vS +* vS1) +* vS2)) *' ll) = k ) by VALUAT_1:def 8;
then X: dom ((v . vS) *' ll) = Seg k by FINSEQ_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 A3: i in dom ((v . vS) *' ll) ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
A4: i in dom ((v . ((vS +* vS1) +* vS2)) *' ll) by A2, A3, X, FINSEQ_1:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A5: dom ((v . ((vS +* vS1) +* vS2)) *' ll) c= dom ll by RELAT_1:44;

A6: now

assume A7: 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:13;
then not ll . i in dom vS by FUNCT_4:13;
then A8: (v +* vS) . (ll . i) = v . (ll . i) by FUNCT_4:12;
A9: ((v . vS) *' ll) . i = v . (ll . i) by A3, A8, FUNCT_1:22;
(v +* ((vS +* vS1) +* vS2)) . (ll . i) = v . (ll . i) by A7, FUNCT_4:12;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A4, A9, FUNCT_1:22; :: thesis: verum

end;

now

assume A10: ll . i in dom ((vS +* vS1) +* vS2) ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
reconsider x = ll . i as bound_QC-variable by A4, A5, Th5;

A11: now

assume A12: not x in dom vS2 ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then A13: x in dom (vS +* vS1) by A10, FUNCT_4:13;
A14: ((vS +* vS1) +* vS2) . x = (vS +* vS1) . x by A12, FUNCT_4:12;

A15: now

assume A16: not x in dom vS1 ; :: thesis: ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i
then ((vS +* vS1) +* vS2) . x = vS . x by A14, FUNCT_4:12;
then A17: (v +* ((vS +* vS1) +* vS2)) . x = vS . x by A10, FUNCT_4:14;
x in dom vS by A13, A16, FUNCT_4:13;
then (v . ((vS +* vS1) +* vS2)) . x = (v +* vS) . x by A17, FUNCT_4:14;
then ((v . ((vS +* vS1) +* vS2)) *' ll) . i = (v . vS) . x by A4, FUNCT_1:22;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A3, FUNCT_1:22; :: thesis: verum

end;

now

assume x in dom vS1 ; :: thesis: contradiction
then A19: not x in still_not-bound_in ll by A1;
len ll = k by SUBSTUT1:34;
then ( 1 <= i & i <= len ll & x in bound_QC-variables ) by A3, X, FINSEQ_1:3;
then consider j being Element of NAT such that
A20: ( j = i & 1 <= j & j <= len ll & ll . j = ll . i & ll . j in bound_QC-variables ) ;
x in { (ll . n) where n is Element of NAT : ( 1 <= n & n <= len ll & ll . n in bound_QC-variables ) } by A20;
then x in variables_in ll,bound_QC-variables by QC_LANG3:def 2;
hence contradiction by A19, QC_LANG3:6; :: thesis: verum

end;

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

end;

now

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:14;
then ((vS +* vS1) +* vS2) . x = v . x by A1, A21;
then (v +* ((vS +* vS1) +* vS2)) . x = v . x by A10, FUNCT_4:14;
then A22: ((v . ((vS +* vS1) +* vS2)) *' ll) . i = v . x by A4, FUNCT_1:22;
not x in dom vS by A1, A21, XBOOLE_0:3;
then (v +* vS) . x = v . x by FUNCT_4:12;
hence ((v . vS) *' ll) . i = ((v . ((vS +* vS1) +* vS2)) *' ll) . i by A22, A3, FUNCT_1:22; :: thesis: verum

end;

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

end;

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

end;

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