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₁,b₂ -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₁ -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);
B1: 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) ;
B0: ( dom LH = X & dom RH = X ) by FUNCT_2:def 1;

now

let x be Element of X; :: thesis: LH . x = RH . x
reconsider F1 = LH . x, F2 = RH . x as Element of Class F ;
C3: ( F1 = (F -class) . (g . x) & F2 = (g quotient (E,F)) . ((E -class) . x) ) by B0, FUNCT_1:12;
then F2 = (g quotient (E,F)) . (EqClass (E,x)) by DefClass;
then [(EqClass (E,x)),F2] in g quotient (E,F) by B1, FUNCT_1:1;
then consider e being Element of Class E, f being Element of Class F such that
C0: ( [(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
C1: ( a in e & b in f & [a,b] in g ) by C0;
Z2: ( EqClass (E,x) = e & F2 = f ) by C0, ZFMISC_1:27;
then C2: ( a in EqClass (E,x) & [a,x] in E & b in F2 ) by C1, EQREL_1:19;
a in X by C1;
then a in dom g by FUNCT_2:def 1;
then b = g . a by C1, FUNCT_1:def 2;
then [b,(g . x)] in F by C2, DefCompatible;
then b in EqClass (F,(g . x)) by EQREL_1:19;
then b in F1 by C3, DefClass;
then F1 meets F2 by C1, Z2, XBOOLE_0:3;
hence LH . x = RH . x by EQREL_1:def 4; :: thesis: verum

end;

hence (F -class) * g = (g quotient (E,F)) * (E -class) by FUNCT_2:63; :: thesis: verum