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 ;

now :: thesis: for x being object st x in X holds
(Card (X --> Y)) . x = (X --> (card Y)) . x

let x be object ; :: 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, 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; :: thesis: verum