defpred S₁[ object ] means ( $1 in M & $1 is Cardinal );
let f1, f2 be Cardinal-Function; :: thesis:
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:

let x be object ; :: thesis:
assume A10: x in dom f1 ; :: thesis:
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:

end;