consider G0, H0 being strict Element of V;
set M = Morphs G0,H0;
set S = { (Morphs G,H) where G, H is strict Element of V : verum } ;
A1: ZERO G0,H0 is Element of Morphs G0,H0 by Def27;
Morphs G0,H0 in { (Morphs G,H) where G, H is strict Element of V : verum } ;
then reconsider T = union { (Morphs G,H) where G, H is strict Element of V : verum } as non empty set by A1, TARSKI:def 4;
A2: for x being set holds
( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )

proof

let x be set ; :: thesis: ( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus ( x in T implies ex G, H being strict Element of V st x is strict Morphism of G,H ) :: thesis: ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T )

proof

assume x in T ; :: thesis: ex G, H being strict Element of V st x is strict Morphism of G,H
then consider Y being set such that
A3: x in Y and
A4: Y in { (Morphs G,H) where G, H is strict Element of V : verum } by TARSKI:def 4;
consider G, H being strict Element of V such that
A5: Y = Morphs G,H by A4;
take G ; :: thesis: ex H being strict Element of V st x is strict Morphism of G,H
take H ; :: thesis: x is strict Morphism of G,H
thus x is strict Morphism of G,H by A3, A5, Def27; :: thesis: verum

end;

thus ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T ) :: thesis: verum

proof

given G, H being strict Element of V such that A6: x is strict Morphism of G,H ; :: thesis: x in T
set M = Morphs G,H;
A7: x in Morphs G,H by A6, Def27;
Morphs G,H in { (Morphs G,H) where G, H is strict Element of V : verum } ;
hence x in T by A7, TARSKI:def 4; :: thesis: verum

end;

end;

now

let x be set ; :: thesis: ( x in T implies x is strict GroupMorphism )
assume x in T ; :: thesis: x is strict GroupMorphism
then ex G, H being strict Element of V st x is strict Morphism of G,H by A2;
hence x is strict GroupMorphism ; :: thesis: verum

end;

then reconsider T' = T as GroupMorphism_DOMAIN by Def23;
take T' ; :: thesis: for x being set holds
( x in T' iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus for x being set holds
( x in T' iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A2; :: thesis: verum