let X, x be set ; :: thesis: ( x in X implies (disjoin (Card (id X))) . x = [:(card x),{x}:] )
assume A1: x in X ; :: thesis: (disjoin (Card (id X))) . x = [:(card x),{x}:]
then A2: x in dom (id X) ;
then x in dom (Card (id X)) by CARD_3:def 2;
hence (disjoin (Card (id X))) . x = [:((Card (id X)) . x),{x}:] by CARD_3:def 3
.= [:(card ((id X) . x)),{x}:] by A2, CARD_3:def 2
.= [:(card x),{x}:] by A1, FUNCT_1:18 ;
:: thesis: verum