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

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