deffunc H₁( set ) -> set = exp ((card $1),N);
defpred S₁[ object ] means $1 is Cardinal;
consider X being set such that
A3: for x being object holds
( x in X iff ( x in M & S₁[x] ) ) from XBOOLE_0:sch 1();
consider f being Cardinal-Function such that
A4: ( dom f = X & ( for x being set st x in X holds
f . x = H₁(x) ) ) from CARD_3:sch 1();
take f ; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
f . K = exp (K,N) ) )
thus for x being object holds
( x in dom f iff ( x in M & x is Cardinal ) ) by A3, A4; :: thesis: for K being Cardinal st K in M holds
f . K = exp (K,N)
let K be Cardinal; :: thesis: ( K in M implies f . K = exp (K,N) )
assume K in M ; :: thesis: f . K = exp (K,N)
then ( K = card K & K in X ) by A3;
hence f . K = exp (K,N) by A4; :: thesis: verum