let X, Y be non empty set ; for E being Equivalence_Relation of X
for F being Equivalence_Relation of Y
for g being b1,b2 -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)
let E be Equivalence_Relation of X; for F being Equivalence_Relation of Y
for g being E,b1 -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)
let F be Equivalence_Relation of Y; 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; (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 for x being Element of X holds LH . x = RH . xlet x be
Element of
X;
LH . x = RH . xreconsider 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;
verum end;
hence
(F -class) * g = (g quotient (E,F)) * (E -class)
by FUNCT_2:63; verum