let A be non empty Preorder; :: thesis:
let D be non empty a_partition of the carrier of A; :: thesis:
assume A1: D = the carrier of (QuotientOrder A) ; :: thesis:
dom (proj D) = the carrier of A by FUNCT_2:def 1;
then A2: dom (proj A) = dom (proj D) by FUNCT_2:def 1;
for x being object st x in dom (proj A) holds
(proj A) . x = (proj D) . x

proof

let x be object ; :: thesis:
assume x in dom (proj A) ; :: thesis:
then reconsider z = x as Element of A ;
A3: z in (proj D) . z by EQREL_1:def 9;
(proj D) . z in the carrier of (QuotientOrder A) by A1;
then (proj D) . z in Class (EqRelOf A) by Def7;
then consider y being object such that
A4: y in the carrier of A and
A5: (proj D) . z = Class ((EqRelOf A),y) by EQREL_1:def 3;
(proj D) . z = Class ((EqRelOf A),z) by A4, A3, A5, EQREL_1:23
.= (proj A) . z by Def8 ;
hence (proj A) . x = (proj D) . x ; :: thesis:

end;

hence proj A = proj D by A2, FUNCT_1:2; :: thesis: