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 } ;
( ZERO G0,H0 is Element of Morphs G0,H0 & Morphs G0,H0 in { (Morphs G,H) where G, H is strict Element of V : verum } ) by Def27;
then reconsider T = union { (Morphs G,H) where G, H is strict Element of V : verum } as non empty set by TARSKI:def 4;
A1: 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
A2: x in Y and
A3: 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
A4: Y = Morphs G,H by A3;
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 A2, A4, 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 A5: x is strict Morphism of G,H ; :: thesis: x in T
set M = Morphs G,H;
A6: Morphs G,H in { (Morphs G,H) where G, H is strict Element of V : verum } ;
x in Morphs G,H by A5, Def27;
hence x in T by A6, 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 A1;
hence x is strict GroupMorphism ; :: thesis: verum

end;

then reconsider T9 = T as GroupMorphism_DOMAIN by Def23;
take T9 ; :: thesis: for x being set holds
( x in T9 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 T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A1; :: thesis: verum