let G1, G2 be non empty strict SubStr of GFuncs X; :: thesis: ( ( for f being Element of (GFuncs X) holds
( f in the carrier of G1 iff f is Permutation of X ) ) & ( for f being Element of (GFuncs X) holds
( f in the carrier of G2 iff f is Permutation of X ) ) implies G1 = G2 )
assume that
A8: for f being Element of (GFuncs X) holds
( f in H₁(G1) iff f is Permutation of X ) and
A9: for f being Element of (GFuncs X) holds
( f in H₁(G2) iff f is Permutation of X ) ; :: thesis: G1 = G2
A10: H₁(G2) c= H₁( GFuncs X) by Th25;
A11: H₁(G1) c= H₁( GFuncs X) by Th25;
H₁(G1) = H₁(G2)

proof

thus H₁(G1) c= H₁(G2) :: according to XBOOLE_0:def 10 :: thesis: H₁(G2) c= H₁(G1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(G1) or x in H₁(G2) )
assume A12: x in H₁(G1) ; :: thesis: x in H₁(G2)
then reconsider f = x as Element of (GFuncs X) by A11;
f is Permutation of X by A8, A12;
hence x in H₁(G2) by A9; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(G2) or x in H₁(G1) )
assume A13: x in H₁(G2) ; :: thesis: x in H₁(G1)
then reconsider f = x as Element of (GFuncs X) by A10;
f is Permutation of X by A9, A13;
hence x in H₁(G1) by A8; :: thesis: verum

end;

hence G1 = G2 by Th28; :: thesis: verum