let f1, f2 be Function of L,(); :: 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 () ;
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 ;
[x9,y9] in E2 by ;
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 ;
[x9,y9] in E1 by ;
hence [x,y] in E1 ; :: thesis: verum
end;
hence f1 . e = f2 . e by ; :: 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