set p = the a_partition of X;
take id the a_partition of X ; :: thesis: ( rng (id the a_partition of X) is a_partition of X & id the a_partition of X is one-to-one )
thus ( rng (id the a_partition of X) is a_partition of X & id the a_partition of X is one-to-one ) ; :: thesis: verum