let D1, D2 be GroupMorphism_DOMAIN of G,H; :: thesis: ( ( for x being object holds
( x in D1 iff x is strict Morphism of G,H ) ) & ( for x being object holds
( x in D2 iff x is strict Morphism of G,H ) ) implies D1 = D2 )
assume that
A6: for x being object holds
( x in D1 iff x is strict Morphism of G,H ) and
A7: for x being object holds
( x in D2 iff x is strict Morphism of G,H ) ; :: thesis: D1 = D2
for x being object holds
( x in D1 iff x in D2 )

proof

let x be object ; :: thesis: ( x in D1 iff x in D2 )
thus ( x in D1 implies x in D2 ) :: thesis: ( x in D2 implies x in D1 )

proof

assume x in D1 ; :: thesis: x in D2
then x is strict Morphism of G,H by A6;
hence x in D2 by A7; :: thesis: verum

end;

thus ( x in D2 implies x in D1 ) :: thesis: verum

proof

assume x in D2 ; :: thesis: x in D1
then x is strict Morphism of G,H by A7;
hence x in D1 by A6; :: thesis: verum

end;

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum