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