Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)