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
A2: for b being Ordinal of U holds f1 . b = exp (a,b) and
A3: for b being Ordinal of U holds f2 . b = exp (a,b) ; :: thesis: f1 = f2

now :: thesis: for x being Element of On U holds f1 . x = f2 . x

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 A2, A3;
hence f1 . x = f2 . x ; :: thesis: verum

end;

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