set cL = the carrier of L;
set x = the Element of the carrier of L;
A1: dom k = the carrier of L by FUNCT_2:def 1;
then A2: ( [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] in id the carrier of L & [:k,k:] . ( the Element of the carrier of L, the Element of the carrier of L) = [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] ) by FUNCT_3:def 8, RELAT_1:def 10;
dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def 8;
then [ the Element of the carrier of L, the Element of the carrier of L] 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 7; :: thesis: verum