reconsider X = v .--> val as PartFunc of , ;
dom (v .--> val) = {v} by FUNCOP_1:19;
then reconsider X = X as PartFunc of , by RELSET_1:13;
rng (v .--> val) = {val} by FUNCOP_1:14;
then reconsider X = X as PartFunc of , by RELSET_1:14;
G .set VLabelSelector ,X is real-vlabeled ;
hence G .set VLabelSelector ,(v .--> val) is [VLabeled] ; :: thesis: verum