reconsider a = a as Ordinal of U by A1;
deffunc H1( Ordinal of U) -> Ordinal of U = exp (a,$1);
ex f being Ordinal-Sequence of U st
for b being Ordinal of U holds f . b = H1(b)
from ORDINAL4:sch 2();
hence
ex b1 being Ordinal-Sequence of U st
for b being Ordinal of U holds b1 . b = exp (a,b)
; verum