theorem Th27: :: DIOPHAN1:37

for a being Real
for t being 1 _greater Nat ex x1, x2 being object st
( 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 )