assume a1: F_dp1 (t,a) is one-to-one ; :: thesis: contradiction
consider x1, x2 being object such that
A2: ( x1 in dom (F_dp1 (t,a)) & x2 in dom (F_dp1 (t,a)) & x1 <> x2 & (F_dp1 (t,a)) . x1 = (F_dp1 (t,a)) . x2 ) by Th27;
thus contradiction by a1, A2; :: thesis: verum