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