let F be Cardinal-Function; :: thesis: for x being set st x in dom F holds
card (F . x) = F . x
let x be set ; :: thesis: ( x in dom F implies card (F . x) = F . x )
assume x in dom F ; :: thesis: card (F . x) = F . x
then reconsider M = F . x as Cardinal by Def1;
card M = M by CARD_1:def 2;
hence card (F . x) = F . x ; :: thesis: verum