let L be non empty Poset; :: thesis:
let f be Function of L,L; :: thesis:
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:
then A1: ( f is monotone & f is idempotent ) ;
take T ; :: thesis:
take q ; :: thesis:
take i ; :: thesis:
thus q is monotone by A1, Th31; :: thesis:
thus q is onto ; :: thesis:
thus ( i is monotone & i is V13() ) ; :: thesis:
thus f = i * q by Th32; :: thesis:
thus id T = q * i by A1, Th33; :: thesis: