let c be Cardinal; :: thesis: for x being object holds card (c --> x) = c
let x be object ; :: thesis: card (c --> x) = c
thus card (c --> x) = card c by Th3
.= c ; :: thesis: verum