theorem :: FUNCT_5:66

for X being set
for x, y being object st x <> y holds
( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] )