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
A4: for f being Element of (GFuncs X) holds
( f in H₁(G1) iff f is Permutation of X ) and
A5: for f being Element of (GFuncs X) holds
( f in H₁(G2) iff f is Permutation of X ) ; :: thesis: G1 = G2
A6: H₁(G2) c= H₁( GFuncs X) by Th23;
A7: H₁(G1) c= H₁( GFuncs X) by Th23;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(G1) or x in H₁(G2) )
assume A8: x in H₁(G1) ; :: thesis: x in H₁(G2)
then reconsider f = x as Element of (GFuncs X) by A7;
f is Permutation of X by A4, A8;
hence x in H₁(G2) by A5; :: thesis: verum

end;

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

end;

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