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
A12: 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
A13: 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
A14: for e being Element of L holds f1 . e = f2 . e

proof

let e be Element of L; :: thesis: f1 . e = f2 . e
consider E1 being Equivalence_Relation of A such that
A15: ( E1 = f1 . e & ( for x, y being Element of A holds
( [x,y] in E1 iff d . x,y <= e ) ) ) by A12;
consider E2 being Equivalence_Relation of A such that
A16: ( E2 = f2 . e & ( for x, y being Element of A holds
( [x,y] in E2 iff d . x,y <= e ) ) ) by A13;
A17: for x, y being Element of A holds
( [x,y] in E1 iff [x,y] in E2 )

proof

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 A15;
hence ( [x,y] in E1 iff [x,y] in E2 ) by A16; :: thesis: verum

end;

for x, y being set holds
( [x,y] in E1 iff [x,y] in E2 )

proof

let x, y be set ; :: thesis: ( [x,y] in E1 iff [x,y] in E2 )
A18: ( field E1 = A & field E2 = A ) by EQREL_1:16;

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

assume A19: [x,y] in E1 ; :: thesis: [x,y] in E2
then reconsider x' = x, y' = y as Element of A by A18, RELAT_1:30;
[x',y'] in E2 by A17, A19;
hence [x,y] in E2 ; :: thesis: verum

end;

assume A20: [x,y] in E2 ; :: thesis: [x,y] in E1
then reconsider x' = x, y' = y as Element of A by A18, RELAT_1:30;
[x',y'] in E1 by A17, A20;
hence [x,y] in E1 ; :: thesis: verum

end;

hence f1 . e = f2 . e by A15, A16, RELAT_1:def 2; :: thesis: verum

end;

reconsider f1' = f1, f2' = f2 as Function of the carrier of L,the carrier of (EqRelLATT A) ;
for e being set st e in the carrier of L holds
f1' . e = f2' . e by A14;
hence f1 = f2 by FUNCT_2:18; :: thesis: verum