let f1, f2 be Function of L,(EqRelLATT A); ( ( for e being Element of L ex E being Equivalence_Relation of A st
( E = f1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st
( E = f2 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) ) implies f1 = f2 )
assume that
A11:
for e being Element of L ex E being Equivalence_Relation of A st
( E = f1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) )
and
A12:
for e being Element of L ex E being Equivalence_Relation of A st
( E = f2 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) )
; f1 = f2
reconsider f19 = f1, f29 = f2 as Function of the carrier of L, the carrier of (EqRelLATT A) ;
for e being Element of L holds f1 . e = f2 . e
proof
let e be
Element of
L;
f1 . e = f2 . e
consider E1 being
Equivalence_Relation of
A such that A13:
E1 = f1 . e
and A14:
for
x,
y being
Element of
A holds
(
[x,y] in E1 iff
d . (
x,
y)
<= e )
by A11;
consider E2 being
Equivalence_Relation of
A such that A15:
E2 = f2 . e
and A16:
for
x,
y being
Element of
A holds
(
[x,y] in E2 iff
d . (
x,
y)
<= e )
by A12;
A17:
for
x,
y being
Element of
A holds
(
[x,y] in E1 iff
[x,y] in E2 )
for
x,
y being
object holds
(
[x,y] in E1 iff
[x,y] in E2 )
proof
let x,
y be
object ;
( [x,y] in E1 iff [x,y] in E2 )
A18:
field E1 = A
by EQREL_1:9;
hereby ( [x,y] in E2 implies [x,y] in E1 )
end;
assume A20:
[x,y] in E2
;
[x,y] in E1
field E2 = A
by EQREL_1:9;
then reconsider x9 =
x,
y9 =
y as
Element of
A by A20, RELAT_1:15;
[x9,y9] in E1
by A17, A20;
hence
[x,y] in E1
;
verum
end;
hence
f1 . e = f2 . e
by A13, A15, RELAT_1:def 2;
verum
end;
then
for e being object st e in the carrier of L holds
f19 . e = f29 . e
;
hence
f1 = f2
by FUNCT_2:12; verum