theorem Lm10: :: DIOPHAN1:34

for a being Real
for t being 1 _greater Nat holds card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))