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

proof

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 )

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

end;

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

proof

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

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

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

assume A20: [x,y] in E2 ; :: thesis: [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 ; :: thesis: verum

end;

hence f1 . e = f2 . e by A13, A15, RELAT_1:def 2; :: thesis: 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; :: thesis: verum