reconsider L1 = L as FieldExtension of L by FIELD_4:6;
take L1 ; :: thesis: ( L1 is F -homomorphic & L1 is F -monomorphic )
thus ( L1 is F -homomorphic & L1 is F -monomorphic ) ; :: thesis: verum