let L be non empty Poset; :: thesis: for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
let f be Function of L,L; :: thesis: ( f is projection implies ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i ) )
reconsider T = Image f as non empty Poset ;
reconsider q = corestr f as Function of L,T ;
reconsider i = inclusion f as Function of T,L ;
assume f is projection ; :: thesis: ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
then A1: ( f is monotone & f is idempotent ) ;
take T ; :: thesis: ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
take q ; :: thesis: ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
take i ; :: thesis: ( q is monotone & q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
thus q is monotone by A1, Th31; :: thesis: ( q is onto & i is monotone & i is one-to-one & f = i * q & id T = q * i )
thus q is onto ; :: thesis: ( i is monotone & i is one-to-one & f = i * q & id T = q * i )
thus ( i is monotone & i is one-to-one ) ; :: thesis: ( f = i * q & id T = q * i )
thus f = i * q by Th32; :: thesis: id T = q * i
thus id T = q * i by A1, Th33; :: thesis: verum