let A be non empty Preorder; :: thesis: for D being non empty a_partition of the carrier of A st D = the carrier of (QuotientOrder A) holds
proj A = proj D
let D be non empty a_partition of the carrier of A; :: thesis: ( D = the carrier of (QuotientOrder A) implies proj A = proj D )
assume A1: D = the carrier of (QuotientOrder A) ; :: thesis: proj A = proj D
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: ( x in dom (proj A) implies (proj A) . x = (proj D) . x )
assume x in dom (proj A) ; :: thesis: (proj A) . x = (proj D) . x
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: verum

end;

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