let m, n be Nat; :: thesis: card (seq (m,n)) = n
card (seq (m,n)) = card n by CARD_1:5, CALCUL_2:6;
hence card (seq (m,n)) = n ; :: thesis: verum