let a be Real; :: thesis: for t being 1 _greater Nat holds card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))
let t be 1 _greater Nat; :: thesis: card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))
A1: card (dom (F_dp1 (t,a))) = card (Seg (len (F_dp1 (t,a)))) by FINSEQ_1:def 3
.= card (Seg (t + 1)) by Def4
.= t + 1 by FINSEQ_1:57 ;
per cases ( rng (F_dp1 (t,a)) = Segm t or rng (F_dp1 (t,a)) c< Segm t ) ;
suppose A3: rng (F_dp1 (t,a)) = Segm t ; :: thesis: card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))
card (Segm t) in nextcard (card (Segm t)) by CARD_1:18;
then card (Segm t) in card (Segm (t + 1)) by NAT_1:42;
hence card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a))) by A1, A3; :: thesis: verum
end;
suppose A6: rng (F_dp1 (t,a)) c< Segm t ; :: thesis: card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a)))
Segm t c= Segm (t + 1) by NAT_1:39, XREAL_1:31;
then rng (F_dp1 (t,a)) c< Segm (t + 1) by A6, XBOOLE_1:58;
then card (rng (F_dp1 (t,a))) in Segm (card (Segm (t + 1))) by CARD_2:48;
hence card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a))) by A1; :: thesis: verum
end;
end;