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