:: deftheorem defines pr1 MCART_1:def 12 :
for f, b₂ being Function holds
( b₂ = pr1 f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = (f . x) `1 ) ) );