let p be set ; :: thesis: Card <*p*> = <*(card p)*>
set Cp = <*(card p)*>;
A1: dom <*(card p)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
now :: thesis: for x being object st x in dom <*(card p)*> holds
<*(card p)*> . x is Cardinal
let x be object ; :: thesis: ( x in dom <*(card p)*> implies <*(card p)*> . x is Cardinal )
assume x in dom <*(card p)*> ; :: thesis: <*(card p)*> . x is Cardinal
then x = 1 by A1, TARSKI:def 1;
hence <*(card p)*> . x is Cardinal by FINSEQ_1:40; :: thesis: verum
end;
then reconsider Cp = <*(card p)*> as Cardinal-Function by CARD_3:def 1;
A2: dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
now :: thesis: for x being object st x in dom <*p*> holds
<*(card p)*> . x = card (<*p*> . x)
let x be object ; :: thesis: ( x in dom <*p*> implies <*(card p)*> . x = card (<*p*> . x) )
assume x in dom <*p*> ; :: thesis: <*(card p)*> . x = card (<*p*> . x)
then A3: x = 1 by A2, TARSKI:def 1;
hence <*(card p)*> . x = card p by FINSEQ_1:40
.= card (<*p*> . x) by A3, FINSEQ_1:40 ;
:: thesis: verum
end;
then Card <*p*> = Cp by A1, A2, CARD_3:def 2;
hence Card <*p*> = <*(card p)*> ; :: thesis: verum