let n be Nat; :: thesis: for IT being Element of Permutations n st n >= 1 holds
( IT is even iff IT " is even )
let IT be Element of Permutations n; :: thesis: ( n >= 1 implies ( IT is even iff IT " is even ) )
assume A1: n >= 1 ; :: thesis: ( IT is even iff IT " is even )
hence ( IT is even implies IT " is even ) by Lm2; :: thesis: ( IT " is even implies IT is even )

now :: thesis: ( IT " is even implies IT is even )

assume IT " is even ; :: thesis: IT is even
then (IT ") " is even by A1, Lm2;
hence IT is even by FUNCT_1:43; :: thesis: verum

end;

hence ( IT " is even implies IT is even ) ; :: thesis: verum