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 )
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