let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
let p be Function of L,L; :: thesis: ( p is projection implies for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc) )
assume A1: p is projection ; :: thesis: for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
let Lc, Lk be non empty Subset of L; :: thesis: ( Lc = { c where c is Element of L : c <= p . c } implies p | Lc is Function of (subrelstr Lc),(subrelstr Lc) )
assume A2: Lc = { c where c is Element of L : c <= p . c } ; :: thesis: p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
set Lk = { k where k is Element of L : p . k <= k } ;
rng p = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th42;
then rng (p | Lc) = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th44;
then A3: rng (p | Lc) c= Lc by XBOOLE_1:17;
( Lc = the carrier of (subrelstr Lc) & p | Lc is Function of Lc, the carrier of L ) by FUNCT_2:32, YELLOW_0:def 15;
hence p | Lc is Function of (subrelstr Lc),(subrelstr Lc) by A3, FUNCT_2:6; :: thesis: verum