let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )
let p be Function of L,L; :: thesis: ( p is projection implies ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) )
assume A1: p is projection ; :: thesis: ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )
set Lc = { c where c is Element of L : c <= p . c } ;
set Lk = { k where k is Element of L : p . k <= k } ;
A2: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A1, Th45;
A3: dom p = the carrier of L by FUNCT_2:def 1;
thus rng (p | { c where c is Element of L : c <= p . c } ) = rng p :: thesis: rng (p | { k where k is Element of L : p . k <= k } ) = rng p

proof

thus rng (p | { c where c is Element of L : c <= p . c } ) c= rng p by RELAT_1:99; :: according to XBOOLE_0:def 10 :: thesis: rng p c= rng (p | { c where c is Element of L : c <= p . c } )
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in rng (p | { c where c is Element of L : c <= p . c } ) )
assume y in rng p ; :: thesis: y in rng (p | { c where c is Element of L : c <= p . c } )
then A4: ( y in { c where c is Element of L : c <= p . c } & y in { k where k is Element of L : p . k <= k } ) by A2, XBOOLE_0:def 4;
then consider lc being Element of L such that
A5: ( y = lc & lc <= p . lc ) ;
consider lk being Element of L such that
A6: ( y = lk & p . lk <= lk ) by A4;
y = p . y by A5, A6, ORDERS_2:25;
hence y in rng (p | { c where c is Element of L : c <= p . c } ) by A3, A4, A5, FUNCT_1:73; :: thesis: verum

end;

thus rng (p | { k where k is Element of L : p . k <= k } ) c= rng p by RELAT_1:99; :: according to XBOOLE_0:def 10 :: thesis: rng p c= rng (p | { k where k is Element of L : p . k <= k } )
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in rng (p | { k where k is Element of L : p . k <= k } ) )
assume y in rng p ; :: thesis: y in rng (p | { k where k is Element of L : p . k <= k } )
then A7: ( y in { c where c is Element of L : c <= p . c } & y in { k where k is Element of L : p . k <= k } ) by A2, XBOOLE_0:def 4;
then consider lc being Element of L such that
A8: ( y = lc & lc <= p . lc ) ;
consider lk being Element of L such that
A9: ( y = lk & p . lk <= lk ) by A7;
y = p . y by A8, A9, ORDERS_2:25;
hence y in rng (p | { k where k is Element of L : p . k <= k } ) by A3, A7, A8, FUNCT_1:73; :: thesis: verum