let X, Y be set ; :: thesis: Card (X --> Y) = X --> (card Y)
A1: dom (Card (X --> Y)) = dom (X --> Y) by Def2;
then A2: dom (Card (X --> Y)) = X by FUNCOP_1:13;
A3: dom (X --> (card Y)) = X by FUNCOP_1:13;

now

let x be set ; :: thesis: ( x in X implies (Card (X --> Y)) . x = (X --> (card Y)) . x )
assume A4: x in X ; :: thesis: (Card (X --> Y)) . x = (X --> (card Y)) . x
then A5: (Card (X --> Y)) . x = card ((X --> Y) . x) by A1, A2, Def2;
(X --> (card Y)) . x = card Y by A4, FUNCOP_1:7;
hence (Card (X --> Y)) . x = (X --> (card Y)) . x by A4, A5, FUNCOP_1:7; :: thesis: verum

end;

hence Card (X --> Y) = X --> (card Y) by A2, A3, FUNCT_1:2; :: thesis: verum