let L be non empty Poset; :: thesis: for f being Function of L,L st f is kernel holds
ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
let f be Function of L,L; :: thesis: ( f is kernel implies ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) )
assume A1: f is kernel ; :: thesis: ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
reconsider T = Image f as non empty Poset ;
reconsider g = corestr f as Function of L,T ;
reconsider d = inclusion f as Function of T,L ;
take T ; :: thesis: ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
take g ; :: thesis: ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
take d ; :: thesis: ( [g,d] is Galois & f = d * g )
thus [g,d] is Galois by A1, Th42; :: thesis: f = d * g
thus f = d * g by Th35; :: thesis: verum