let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A holds
( dom v = bound_QC-variables Al & dom (x | a) = {x} )
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A holds
( dom v = bound_QC-variables Al & dom (x | a) = {x} )
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for a being Element of A holds
( dom v = bound_QC-variables Al & dom (x | a) = {x} )
let v be Element of Valuations_in (Al,A); :: thesis: for a being Element of A holds
( dom v = bound_QC-variables Al & dom (x | a) = {x} )
let a be Element of A; :: thesis: ( dom v = bound_QC-variables Al & dom (x | a) = {x} )
v is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then ex f being Function st
( v = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 2;
hence dom v = bound_QC-variables Al ; :: thesis: dom (x | a) = {x}
thus dom (x | a) = {x} ; :: thesis: verum