theorem Lm10: :: DIOPHAN1:36

for a being Real
for t being 1 _greater Nat holds
( card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a))) & rng (F_dp1 (t,a)) <> {} )