let f1, f2 be Function of L,(EqRelLATT A); :: thesis: ( ( 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 ) ) ) ; :: thesis: 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

f19 . e = f29 . e ;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum

( 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 ) ) ) ; :: thesis: 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

then
for e being object st e in the carrier of L holds
let e be Element of L; :: thesis: 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 )

( [x,y] in E1 iff [x,y] in E2 )

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

proof

for x, y being object holds
let x, y be Element of A; :: thesis: ( [x,y] in E1 iff [x,y] in E2 )

( [x,y] in E1 iff d . (x,y) <= e ) by A14;

hence ( [x,y] in E1 iff [x,y] in E2 ) by A16; :: thesis: verum

end;( [x,y] in E1 iff d . (x,y) <= e ) by A14;

hence ( [x,y] in E1 iff [x,y] in E2 ) by A16; :: thesis: verum

( [x,y] in E1 iff [x,y] in E2 )

proof

hence
f1 . e = f2 . e
by A13, A15, RELAT_1:def 2; :: thesis: verum
let x, y be object ; :: thesis: ( [x,y] in E1 iff [x,y] in E2 )

A18: field E1 = A by EQREL_1:9;

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 ; :: thesis: verum

end;A18: field E1 = A by EQREL_1:9;

hereby :: thesis: ( [x,y] in E2 implies [x,y] in E1 )

assume A20:
[x,y] in E2
; :: thesis: [x,y] in E1assume A19:
[x,y] in E1
; :: thesis: [x,y] in E2

then reconsider x9 = x, y9 = y as Element of A by A18, RELAT_1:15;

[x9,y9] in E2 by A17, A19;

hence [x,y] in E2 ; :: thesis: verum

end;then reconsider x9 = x, y9 = y as Element of A by A18, RELAT_1:15;

[x9,y9] in E2 by A17, A19;

hence [x,y] in E2 ; :: thesis: verum

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 ; :: thesis: verum

f19 . e = f29 . e ;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum