set cL = the carrier of L;
consider x being Element of the carrier of L;
A1: dom k = the carrier of L by FUNCT_2:def 1;
then A2: ( [(k . x),(k . x)] in id the carrier of L & [:k,k:] . x,x = [(k . x),(k . x)] ) by FUNCT_3:def 9, RELAT_1:def 10;
dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def 9;
then [x,x] in dom [:k,k:] by A1, ZFMISC_1:def 2;
hence [:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:] by A2, FUNCT_1:def 13; :: thesis: verum