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

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

hence
proj A = proj D
by A2, FUNCT_1:2; :: thesis: verum
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;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