theorem :: CARD_3:48

for x being object
for f being Function st x in product f holds
x is Function ;