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)
set Lc = { c where c is Element of L : c <= p . c } ;
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)
rng p = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th42;
then rng (p | Lk) = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th44;
then A3: rng (p | Lk) c= Lk by XBOOLE_1:17;
( Lk = the carrier of (subrelstr Lk) & p | Lk is Function of Lk, the carrier of L ) by FUNCT_2:32, YELLOW_0:def 15;
hence p | Lk is Function of (subrelstr Lk),(subrelstr Lk) by A3, FUNCT_2:6; :: thesis: verum