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
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
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
p | Lk is Function of (subrelstr Lk),(subrelstr Lk) )
assume A1: p is projection ; :: thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
let Lk be non empty Subset of L; :: thesis: ( Lk = { k where k is Element of L : p . k <= k } implies p | Lk is Function of (subrelstr Lk),(subrelstr Lk) )
assume A2: Lk = { k where k is Element of L : p . k <= k } ; :: thesis: p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
set Lc = { c where c is Element of L : c <= p . c } ;
rng p = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th45;
then rng (p | Lk) = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th47;
then A3: rng (p | Lk) c= Lk by XBOOLE_1:17;
A4: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def 15;
p | Lk is Function of Lk,the carrier of L by FUNCT_2:38;
hence p | Lk is Function of (subrelstr Lk),(subrelstr Lk) by A3, A4, FUNCT_2:8; :: thesis: verum