set A = the AlgebraicClosure of F;
take the AlgebraicClosure of F ; :: thesis: ( the AlgebraicClosure of F is F -homomorphic & the AlgebraicClosure of F is F -monomorphic )
thus the AlgebraicClosure of F is F -homomorphic ; :: thesis: the AlgebraicClosure of F is F -monomorphic
thus the AlgebraicClosure of F is F -monomorphic ; :: thesis: verum