let f be Function; :: thesis: for x, y being object holds card (f +~ (x,y)) = card f
let x, y be object ; :: thesis: card (f +~ (x,y)) = card f
thus card (f +~ (x,y)) = card (dom (f +~ (x,y))) by Th60
.= card (dom f) by FUNCT_4:99
.= card f by Th60 ; :: thesis: verum