let X be set ; :: thesis: ( X is permutational implies X is functional )
assume X is permutational ; :: thesis: X is functional
then A1: ex n being Nat st
for x being set st x in X holds
x is Permutation of (Seg n) by MATRIX_1:def 10;
let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in X or x is set )
thus ( not x in X or x is set ) by A1; :: thesis: verum