let f1, f2 be Ordinal-Sequence of U; :: thesis: ( ( for b being Ordinal of U holds f1 . b = exp (a,b) ) & ( for b being Ordinal of U holds f2 . b = exp (a,b) ) implies f1 = f2 )
assume that
A1: for b being Ordinal of U holds f1 . b = exp (a,b) and
A2: for b being Ordinal of U holds f2 . b = exp (a,b) ; :: thesis: f1 = f2

now

let x be Element of On U; :: thesis: f1 . x = f2 . x
x in U by ORDINAL1:def 9;
then ( f1 . x = exp (a,x) & f2 . x = exp (a,x) ) by A1, A2;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum