set f = (0,1) --> (1,0);
A1: rng ((0,1) --> (1,0)) = 2 by CARD_1:50, FUNCT_4:64;
dom ((0,1) --> (1,0)) = 2 by CARD_1:50, FUNCT_4:62;
then (0,1) --> (1,0) is Function of 2,2 by A1, FUNCT_2:def 1, RELSET_1:4;
hence (0,1) --> (1,0) is Permutation of 2 by A1, FUNCT_2:57; :: thesis: verum