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);
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

let 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;

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