let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let p be Function of L,L; :: thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume that
A1: p is idempotent and
A2: p is monotone ; :: according to WAYBEL_1:def 13 :: thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let Lk be non empty Subset of L; :: thesis: ( Lk = { k where k is Element of L : p . k <= k } implies for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume A3: Lk = { k where k is Element of L : p . k <= k } ; :: thesis: for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let pk be Function of (subrelstr Lk),(subrelstr Lk); :: thesis: ( pk = p | Lk implies pk is kernel )
assume A4: pk = p | Lk ; :: thesis: pk is kernel
A5: dom pk = the carrier of (subrelstr Lk) by FUNCT_2:def 1;

hereby :: according to QUANTAL1:def 9,WAYBEL_1:def 13,WAYBEL_1:def 15 :: thesis: pk <= id (subrelstr Lk)

now

let x be Element of (subrelstr Lk); :: thesis: (pk * pk) . x = pk . x
A6: pk . x = p . x by A4, A5, FUNCT_1:70;
A7: x is Element of L by YELLOW_0:59;
p . (p . x) = pk . (pk . x) by A4, A5, A6, FUNCT_1:70
.= (pk * pk) . x by A5, FUNCT_1:23 ;
hence (pk * pk) . x = pk . x by A1, A6, A7, YELLOW_2:20; :: thesis: verum

end;

hence pk * pk = pk by FUNCT_2:113; :: thesis: pk is monotone
thus pk is monotone :: thesis: verum

proof

let x1, x2 be Element of (subrelstr Lk); :: according to WAYBEL_1:def 2 :: thesis: ( x1 <= x2 implies pk . x1 <= pk . x2 )
reconsider x1' = x1, x2' = x2 as Element of L by YELLOW_0:59;
A8: ( pk . x1 = p . x1' & pk . x2 = p . x2' ) by A4, A5, FUNCT_1:70;
assume x1 <= x2 ; :: thesis: pk . x1 <= pk . x2
then x1' <= x2' by YELLOW_0:60;
then p . x1' <= p . x2' by A2, Def2;
hence pk . x1 <= pk . x2 by A8, YELLOW_0:61; :: thesis: verum

end;

end;

now

let x be Element of (subrelstr Lk); :: thesis: pk . x <= (id (subrelstr Lk)) . x
reconsider x' = x as Element of L by YELLOW_0:59;
A9: pk . x = p . x' by A4, A5, FUNCT_1:70;
x in the carrier of (subrelstr Lk) ;
then x in Lk by YELLOW_0:def 15;
then ex c being Element of L st
( x = c & p . c <= c ) by A3;
then pk . x <= x by A9, YELLOW_0:61;
hence pk . x <= (id (subrelstr Lk)) . x by TMAP_1:91; :: thesis: verum

end;

hence pk <= id (subrelstr Lk) by YELLOW_2:10; :: thesis: verum