let X1, X2 be Subset of I; ( ( for i being object holds
( i in X1 iff ( a . i <> 1_ G & i in I ) ) ) & ( for i being object holds
( i in X2 iff ( a . i <> 1_ G & i in I ) ) ) implies X1 = X2 )
assume that
A2:
for i being object holds
( i in X1 iff ( a . i <> 1_ G & i in I ) )
and
A3:
for i being object holds
( i in X2 iff ( a . i <> 1_ G & i in I ) )
; X1 = X2
hence
X1 = X2
by TARSKI:2; verum