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 Lk = { k where k is Element of L : p . k <= k } ;
set Lc = { c where c is Element of L : c <= p . c } ;
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, Th42;
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:70; :: 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 object ; :: 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 A4: y in rng p ; :: thesis: y in rng (p | { c where c is Element of L : c <= p . c } )
then A5: y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def 4;
then A6: ex lc being Element of L st
( y = lc & lc <= p . lc ) ;
y in { k where k is Element of L : p . k <= k } by A2, A4, XBOOLE_0:def 4;
then ex lk being Element of L st
( y = lk & p . lk <= lk ) ;
then y = p . y by A6, ORDERS_2:2;
hence y in rng (p | { c where c is Element of L : c <= p . c } ) by A3, A5, A6, FUNCT_1:50; :: thesis: verum
end;
thus rng (p | { k where k is Element of L : p . k <= k } ) c= rng p by RELAT_1:70; :: 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 object ; :: 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 A7: y in rng p ; :: thesis: y in rng (p | { k where k is Element of L : p . k <= k } )
then y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def 4;
then A8: ex lc being Element of L st
( y = lc & lc <= p . lc ) ;
A9: y in { k where k is Element of L : p . k <= k } by A2, A7, XBOOLE_0:def 4;
then ex lk being Element of L st
( y = lk & p . lk <= lk ) ;
then y = p . y by A8, ORDERS_2:2;
hence y in rng (p | { k where k is Element of L : p . k <= k } ) by A3, A9, A8, FUNCT_1:50; :: thesis: verum