per cases ( x in dom perm or not x in dom perm ) ;

suppose A1: x in dom perm ; :: thesis: perm . x is natural

perm is Permutation of (Seg n) by MATRIX_1:def 12;
then A2: rng perm = Seg n by FUNCT_2:def 3;
perm . x in rng perm by A1, FUNCT_1:def 3;
hence perm . x is natural by A2; :: thesis: verum

end;

suppose not x in dom perm ; :: thesis: perm . x is natural

hence perm . x is natural by FUNCT_1:def 2; :: thesis: verum

end;

end;