let n be Ordinal; :: thesis: ex a being Ordinal st n = n *^ a
take 1 ; :: thesis: n = n *^ 1
thus n = n *^ 1 by ORDINAL2:39; :: thesis: verum