let Al be QC-alphabet ; for k being Nat
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let k be Nat; for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let A be non empty set ; for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let v be Element of Valuations_in (Al,A); for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))
let ll be CQC-variable_list of k,Al; v *' ll = ll * (v | (still_not-bound_in ll))
rng ll c= bound_QC-variables Al
by RELAT_1:def 19;
then A1:
rng ll = still_not-bound_in ll
by Th57;
dom (v | (still_not-bound_in ll)) = (dom v) /\ (still_not-bound_in ll)
by RELAT_1:61;
then
dom (v | (still_not-bound_in ll)) = (bound_QC-variables Al) /\ (still_not-bound_in ll)
by Th58;
then
rng ll = dom (v | (still_not-bound_in ll))
by A1, XBOOLE_1:28;
then A2:
dom (ll * (v | (still_not-bound_in ll))) = dom ll
by RELAT_1:27;
then A3:
dom (ll * (v | (still_not-bound_in ll))) = Seg (len ll)
by FINSEQ_1:def 3;
then reconsider f = ll * (v | (still_not-bound_in ll)) as FinSequence by FINSEQ_1:def 2;
len f = len ll
by A3, FINSEQ_1:def 3;
then A4:
len f = k
by SUBSTUT1:34;
then A5:
dom f = Seg k
by FINSEQ_1:def 3;
A6:
for j being Nat st j in dom f holds
f . j = (v *' ll) . j
proof
A7:
rng ll c= bound_QC-variables Al
by RELAT_1:def 19;
let j be
Nat;
( j in dom f implies f . j = (v *' ll) . j )
assume A8:
j in dom f
;
f . j = (v *' ll) . j
reconsider j =
j as
Nat ;
ll . j in rng ll
by A2, A8, FUNCT_1:3;
then
ll . j in bound_QC-variables Al
by A7;
then A9:
ll . j in dom v
by Th58;
ll . j in still_not-bound_in ll
by A1, A2, A8, FUNCT_1:3;
then
ll . j in (dom v) /\ (still_not-bound_in ll)
by A9, XBOOLE_0:def 4;
then A10:
(v | (still_not-bound_in ll)) . (ll . j) = v . (ll . j)
by FUNCT_1:48;
( 1
<= j &
j <= k )
by A5, A8, FINSEQ_1:1;
then
(v | (still_not-bound_in ll)) . (ll . j) = (v *' ll) . j
by A10, VALUAT_1:def 3;
hence
f . j = (v *' ll) . j
by A2, A8, FUNCT_1:13;
verum
end;
len (v *' ll) = k
by VALUAT_1:def 3;
hence
v *' ll = ll * (v | (still_not-bound_in ll))
by A4, A6, FINSEQ_2:9; verum