let X, Y be non empty set ; :: thesis: for E being Equivalence_Relation of X

for F being Equivalence_Relation of Y

for g being b_{1},b_{2} -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)

let E be Equivalence_Relation of X; :: thesis: for F being Equivalence_Relation of Y

for g being E,b_{1} -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)

let F be Equivalence_Relation of Y; :: thesis: for g being E,F -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)

let g be E,F -respecting Function of X,Y; :: thesis: (F -class) * g = (g quotient (E,F)) * (E -class)

set G = g quotient (E,F);

A1: dom (g quotient (E,F)) = Class E by FUNCT_2:def 1;

reconsider LH = (F -class) * g, RH = (g quotient (E,F)) * (E -class) as Function of X,(Class F) ;

A2: ( dom LH = X & dom RH = X ) by FUNCT_2:def 1;

for F being Equivalence_Relation of Y

for g being b

let E be Equivalence_Relation of X; :: thesis: for F being Equivalence_Relation of Y

for g being E,b

let F be Equivalence_Relation of Y; :: thesis: for g being E,F -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)

let g be E,F -respecting Function of X,Y; :: thesis: (F -class) * g = (g quotient (E,F)) * (E -class)

set G = g quotient (E,F);

A1: dom (g quotient (E,F)) = Class E by FUNCT_2:def 1;

reconsider LH = (F -class) * g, RH = (g quotient (E,F)) * (E -class) as Function of X,(Class F) ;

A2: ( dom LH = X & dom RH = X ) by FUNCT_2:def 1;

now :: thesis: for x being Element of X holds LH . x = RH . x

hence
(F -class) * g = (g quotient (E,F)) * (E -class)
by FUNCT_2:63; :: thesis: verumlet x be Element of X; :: thesis: LH . x = RH . x

reconsider F1 = LH . x, F2 = RH . x as Element of Class F ;

A3: ( F1 = (F -class) . (g . x) & F2 = (g quotient (E,F)) . ((E -class) . x) ) by A2, FUNCT_1:12;

then F2 = (g quotient (E,F)) . (EqClass (E,x)) by Def13;

then [(EqClass (E,x)),F2] in g quotient (E,F) by A1, FUNCT_1:1;

then consider e being Element of Class E, f being Element of Class F such that

A4: ( [(EqClass (E,x)),F2] = [e,f] & ex a, b being set st

( a in e & b in f & [a,b] in g ) ) ;

consider a, b being set such that

A5: ( a in e & b in f & [a,b] in g ) by A4;

A6: ( EqClass (E,x) = e & F2 = f ) by A4, XTUPLE_0:1;

then A7: ( a in EqClass (E,x) & [a,x] in E & b in F2 ) by A5, EQREL_1:19;

a in X by A5;

then a in dom g by FUNCT_2:def 1;

then b = g . a by A5, FUNCT_1:def 2;

then [b,(g . x)] in F by A7, Def9;

then b in EqClass (F,(g . x)) by EQREL_1:19;

then b in F1 by A3, Def13;

hence LH . x = RH . x by EQREL_1:def 4, A5, A6, XBOOLE_0:3; :: thesis: verum

end;reconsider F1 = LH . x, F2 = RH . x as Element of Class F ;

A3: ( F1 = (F -class) . (g . x) & F2 = (g quotient (E,F)) . ((E -class) . x) ) by A2, FUNCT_1:12;

then F2 = (g quotient (E,F)) . (EqClass (E,x)) by Def13;

then [(EqClass (E,x)),F2] in g quotient (E,F) by A1, FUNCT_1:1;

then consider e being Element of Class E, f being Element of Class F such that

A4: ( [(EqClass (E,x)),F2] = [e,f] & ex a, b being set st

( a in e & b in f & [a,b] in g ) ) ;

consider a, b being set such that

A5: ( a in e & b in f & [a,b] in g ) by A4;

A6: ( EqClass (E,x) = e & F2 = f ) by A4, XTUPLE_0:1;

then A7: ( a in EqClass (E,x) & [a,x] in E & b in F2 ) by A5, EQREL_1:19;

a in X by A5;

then a in dom g by FUNCT_2:def 1;

then b = g . a by A5, FUNCT_1:def 2;

then [b,(g . x)] in F by A7, Def9;

then b in EqClass (F,(g . x)) by EQREL_1:19;

then b in F1 by A3, Def13;

hence LH . x = RH . x by EQREL_1:def 4, A5, A6, XBOOLE_0:3; :: thesis: verum