Description: Alternate proof of dmfex : shorter but using ax-rep . (Contributed by NM, 27-Aug-2006) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Proof shortened by AV, 23-Aug-2024) (Proof modification is discouraged.) (New usage is discouraged.)