let f1, f2 be Ordinal-Sequence; :: thesis: ( dom f1 = dom A & ( for a being object st a in dom A holds
f1 . a = b -exponent (A . a) ) & dom f2 = dom A & ( for a being object st a in dom A holds
f2 . a = b -exponent (A . a) ) implies f1 = f2 )
assume that
A4: dom f1 = dom A and
A5: for a being object st a in dom A holds
f1 . a = b -exponent (A . a) and
A6: dom f2 = dom A and
A7: for a being object st a in dom A holds
f2 . a = b -exponent (A . a) ; :: thesis: f1 = f2

now :: thesis: for a being object st a in dom f1 holds
f1 . a = f2 . a

let a be object ; :: thesis: ( a in dom f1 implies f1 . a = f2 . a )
assume A8: a in dom f1 ; :: thesis: f1 . a = f2 . a
hence f1 . a = b -exponent (A . a) by A4, A5
.= f2 . a by A4, A7, A8 ;
:: thesis: verum

end;

hence f1 = f2 by A4, A6, FUNCT_1:2; :: thesis: verum