let L be complete continuous LATTICE; :: thesis: for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
let k be directed-sups-preserving kernel Function of L,L; :: thesis: k = kernel_op (kernel_congruence k)
set kc = kernel_congruence k;
set cL = the carrier of L;
set km = kernel_op (kernel_congruence k);
A1: dom k = the carrier of L by FUNCT_2:def 1;
A2: kernel_op (kernel_congruence k) <= id L by WAYBEL_1:def 15;
A3: k <= id L by WAYBEL_1:def 15;
A4: kernel_congruence k is CLCongruence by Th40;
then A5: kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L) by Th36;
reconsider kc9 = kernel_congruence k as Equivalence_Relation of the carrier of L by A4;
field kc9 = the carrier of L by ORDERS_1:12;
then A6: kc9 is_transitive_in the carrier of L by RELAT_2:def 16;
A7: dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] = [:(dom (kernel_op (kernel_congruence k))),(dom (kernel_op (kernel_congruence k))):] by FUNCT_3:def 8;
A8: dom (kernel_op (kernel_congruence k)) = the carrier of L by FUNCT_2:def 1;
A9: dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def 8;

now :: thesis: for x being object st x in the carrier of L holds
k . x = (kernel_op (kernel_congruence k)) . x

let x be object ; :: thesis: ( x in the carrier of L implies k . x = (kernel_op (kernel_congruence k)) . x )
assume x in the carrier of L ; :: thesis: k . x = (kernel_op (kernel_congruence k)) . x
then reconsider x9 = x as Element of L ;
A10: k . (k . x9) = (k * k) . x9 by A1, FUNCT_1:13
.= k . x9 by QUANTAL1:def 9 ;
A11: ( [(k . x9),(k . x9)] in id the carrier of L & [:k,k:] . ((k . x9),x9) = [(k . (k . x9)),(k . x9)] ) by A1, FUNCT_3:def 8, RELAT_1:def 10;
[(k . x9),x9] in dom [:k,k:] by A1, A9, ZFMISC_1:def 2;
then A12: [(k . x9),x9] in kernel_congruence k by A10, A11, FUNCT_1:def 7;
A13: (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) = ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13
.= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def 9 ;
(kernel_op (kernel_congruence k)) . (k . x9) <= (id L) . (k . x9) by A2, YELLOW_2:9;
then A14: (kernel_op (kernel_congruence k)) . (k . x9) <= k . x9 by FUNCT_1:18;
A15: ( [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . x9)] in id the carrier of L & [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (x9,((kernel_op (kernel_congruence k)) . x9)) = [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] ) by A8, FUNCT_3:def 8, RELAT_1:def 10;
[x9,((kernel_op (kernel_congruence k)) . x9)] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] by A8, A7, ZFMISC_1:def 2;
then [x9,((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A5, A13, A15, FUNCT_1:def 7;
then A16: [(k . x9),((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A6, A12;
then [:k,k:] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by FUNCT_1:def 7;
then [(k . (k . x9)),(k . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A1, FUNCT_3:def 8;
then A17: k . ((kernel_op (kernel_congruence k)) . x9) = k . (k . x9) by RELAT_1:def 10
.= (k * k) . x9 by A1, FUNCT_1:13
.= k . x9 by QUANTAL1:def 9 ;
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by A5, A16, FUNCT_1:def 7;
then [((kernel_op (kernel_congruence k)) . (k . x9)),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A8, FUNCT_3:def 8;
then A18: (kernel_op (kernel_congruence k)) . (k . x9) = (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) by RELAT_1:def 10
.= ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13
.= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def 9 ;
k . ((kernel_op (kernel_congruence k)) . x9) <= (id L) . ((kernel_op (kernel_congruence k)) . x9) by A3, YELLOW_2:9;
then k . ((kernel_op (kernel_congruence k)) . x9) <= (kernel_op (kernel_congruence k)) . x9 by FUNCT_1:18;
hence k . x = (kernel_op (kernel_congruence k)) . x by A17, A18, A14, YELLOW_0:def 3; :: thesis: verum

end;

hence k = kernel_op (kernel_congruence k) by FUNCT_2:12; :: thesis: verum