defpred S₁[ object ] means ( $1 in M & $1 is Cardinal );
let f1, f2 be Cardinal-Function; :: thesis: ( ( for x being object holds
( x in dom f1 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f1 . K = exp (K,N) ) & ( for x being object holds
( x in dom f2 iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f2 . K = exp (K,N) ) implies f1 = f2 )
assume that
A5: for x being object holds
( x in dom f1 iff S₁[x] ) and
A6: for K being Cardinal st K in M holds
f1 . K = exp (K,N) and
A7: for x being object holds
( x in dom f2 iff S₁[x] ) and
A8: for K being Cardinal st K in M holds
f2 . K = exp (K,N) ; :: thesis: f1 = f2

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

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A10: x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider K = x as Cardinal by A5;
A11: K in M by A5, A10;
hence f1 . x = exp (K,N) by A6
.= f2 . x by A8, A11 ;
:: thesis: verum

end;

dom f1 = dom f2 from XBOOLE_0:sch 2(A5, A7);
hence f1 = f2 by A9; :: thesis: verum