A1: dom (l ") = rng l by FUNCT_1:55;
rng (l ") = dom l by FUNCT_1:55;
hence l " is PartFunc of Vars,NAT by A1, RELSET_1:11; :: thesis: verum