let x, X be set ; :: thesis: ( x is Element of (GPerms X) iff x is Permutation of X )
A1: ( x is Permutation of X implies x in Funcs (X,X) ) by FUNCT_2:9;
H₁( GPerms X) c= H₁( GFuncs X) by Th23;
then A2: ( x is Element of (GPerms X) implies x is Element of (GFuncs X) ) ;
H₁( GFuncs X) = Funcs (X,X) by Def40;
hence ( x is Element of (GPerms X) iff x is Permutation of X ) by A1, A2, Def42; :: thesis: verum