let G1, G2 be non empty strict SubStr of GFuncs X; :: thesis:
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:
A6: H₁(G2) c= H₁( GFuncs X) by Th23;
A7: H₁(G1) c= H₁( GFuncs X) by Th23;
H₁(G1) = H₁(G2)

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in H₁(G1) ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in H₁(G2) ; :: thesis:
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:

end;