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 ) by RELAT_1:45; :: thesis: verum