let x, X be set ; :: thesis: ( x is Element of (GPerms X) iff x is Permutation of X )
H₁( GPerms X) c= H₁( GFuncs X) by Th25;
then ( H₁( GFuncs X) = Funcs X,X & ( x is Permutation of X implies x in Funcs X,X ) & ( x is Element of (GPerms X) implies x is Element of (GFuncs X) ) ) by Def40, FUNCT_2:12, TARSKI:def 3;
hence ( x is Element of (GPerms X) iff x is Permutation of X ) by Def42; :: thesis: verum