theorem :: FUNCT_5:58

for X being set
for x being object holds
( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) )