let it1, it2 be kernel Function of L,L; :: thesis: ( ( for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ) implies it1 = it2 )
assume that
A15: for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) and
A16: for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ; :: thesis: it1 = it2

now :: thesis: for x being object st x in the carrier of L holds
it1 . x = it2 . x

let x be object ; :: thesis: ( x in the carrier of L implies it1 . x = it2 . x )
assume x in the carrier of L ; :: thesis: it1 . x = it2 . x
then reconsider x9 = x as Element of L ;
thus it1 . x = inf (Class ((EqRel R),x9)) by A15
.= it2 . x by A16 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:12; :: thesis: verum