set P = the a_partition of A;
take id the a_partition of A ; :: thesis: rng (id the a_partition of A) is a_partition of A
thus rng (id the a_partition of A) is a_partition of A ; :: thesis: verum