let f1, f2 be distance_function of the carrier of L,L; :: thesis: ( ( for x, y being Element of L holds
( ( x <> y implies f1 . (x,y) = x "\/" y ) & ( x = y implies f1 . (x,y) = Bottom L ) ) ) & ( for x, y being Element of L holds
( ( x <> y implies f2 . (x,y) = x "\/" y ) & ( x = y implies f2 . (x,y) = Bottom L ) ) ) implies f1 = f2 )
assume that
A14: for x, y being Element of L holds
( ( x <> y implies f1 . (x,y) = x "\/" y ) & ( x = y implies f1 . (x,y) = Bottom L ) ) and
A15: for x, y being Element of L holds
( ( x <> y implies f2 . (x,y) = x "\/" y ) & ( x = y implies f2 . (x,y) = Bottom L ) ) ; :: thesis: f1 = f2
A16: for z being object st z in dom f1 holds
f1 . z = f2 . z
proof
let z be object ; :: thesis: ( z in dom f1 implies f1 . z = f2 . z )
assume A17: z in dom f1 ; :: thesis: f1 . z = f2 . z
then consider x, y being object such that
A18: z = [x,y] by RELAT_1:def 1;
reconsider x = x, y = y as Element of L by A17, A18, ZFMISC_1:87;
per cases ( x = y or x <> y ) ;
suppose A19: x = y ; :: thesis: f1 . z = f2 . z
thus f1 . z = f1 . (x,y) by A18
.= Bottom L by A14, A19
.= f2 . (x,y) by A15, A19
.= f2 . z by A18 ; :: thesis: verum
end;
suppose A20: x <> y ; :: thesis: f1 . z = f2 . z
thus f1 . z = f1 . (x,y) by A18
.= x "\/" y by A14, A20
.= f2 . (x,y) by A15, A20
.= f2 . z by A18 ; :: thesis: verum
end;
end;
end;
dom f1 = [: the carrier of L, the carrier of L:] by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1 ;
hence f1 = f2 by A16, FUNCT_1:2; :: thesis: verum