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 Th41;
then A5: kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L) by Th37;
reconsider kc' = kernel_congruence k as Equivalence_Relation of by A4, Def2;
field kc' = the carrier of L by ORDERS_1:97;
then A6: kc' 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 9;
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 9;

now

let x be set ; :: 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 x' = x as Element of ;
A10: k . (k . x') = (k * k) . x' by A1, FUNCT_1:23
.= k . x' by QUANTAL1:def 9 ;
A11: ( [(k . x'),(k . x')] in id the carrier of L & [:k,k:] . (k . x'),x' = [(k . (k . x')),(k . x')] ) by A1, FUNCT_3:def 9, RELAT_1:def 10;
[(k . x'),x'] in dom [:k,k:] by A1, A9, ZFMISC_1:def 2;
then A12: [(k . x'),x'] in kernel_congruence k by A10, A11, FUNCT_1:def 13;
A13: (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x') = ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x' by A8, FUNCT_1:23
.= (kernel_op (kernel_congruence k)) . x' by QUANTAL1:def 9 ;
(kernel_op (kernel_congruence k)) . (k . x') <= (id L) . (k . x') by A2, YELLOW_2:10;
then A14: (kernel_op (kernel_congruence k)) . (k . x') <= k . x' by FUNCT_1:35;
A15: ( [((kernel_op (kernel_congruence k)) . x'),((kernel_op (kernel_congruence k)) . x')] in id the carrier of L & [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . x',((kernel_op (kernel_congruence k)) . x') = [((kernel_op (kernel_congruence k)) . x'),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x'))] ) by A8, FUNCT_3:def 9, RELAT_1:def 10;
[x',((kernel_op (kernel_congruence k)) . x')] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] by A8, A7, ZFMISC_1:def 2;
then [x',((kernel_op (kernel_congruence k)) . x')] in kernel_congruence k by A5, A13, A15, FUNCT_1:def 13;
then A16: [(k . x'),((kernel_op (kernel_congruence k)) . x')] in kernel_congruence k by A6, A12, RELAT_2:def 8;
then [:k,k:] . (k . x'),((kernel_op (kernel_congruence k)) . x') in id the carrier of L by FUNCT_1:def 13;
then [(k . (k . x')),(k . ((kernel_op (kernel_congruence k)) . x'))] in id the carrier of L by A1, FUNCT_3:def 9;
then A17: k . ((kernel_op (kernel_congruence k)) . x') = k . (k . x') by RELAT_1:def 10
.= (k * k) . x' by A1, FUNCT_1:23
.= k . x' by QUANTAL1:def 9 ;
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (k . x'),((kernel_op (kernel_congruence k)) . x') in id the carrier of L by A5, A16, FUNCT_1:def 13;
then [((kernel_op (kernel_congruence k)) . (k . x')),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x'))] in id the carrier of L by A8, FUNCT_3:def 9;
then A18: (kernel_op (kernel_congruence k)) . (k . x') = (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x') by RELAT_1:def 10
.= ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x' by A8, FUNCT_1:23
.= (kernel_op (kernel_congruence k)) . x' by QUANTAL1:def 9 ;
k . ((kernel_op (kernel_congruence k)) . x') <= (id L) . ((kernel_op (kernel_congruence k)) . x') by A3, YELLOW_2:10;
then k . ((kernel_op (kernel_congruence k)) . x') <= (kernel_op (kernel_congruence k)) . x' by FUNCT_1:35;
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:18; :: thesis: verum