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