set G0 = the strict Element of V;
set M = Morphs ( the strict Element of V, the strict Element of V);
set S = { (Morphs (G,H)) where G, H is strict Element of V : verum } ;
( ZERO ( the strict Element of V, the strict Element of V) is Element of Morphs ( the strict Element of V, the strict Element of V) & Morphs ( the strict Element of V, the strict Element of V) in { (Morphs (G,H)) where G, H is strict Element of V : verum } )
by Def20;
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 object 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
object ;
( 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 )
( 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
;
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
;
ex H being strict Element of V st x is strict Morphism of G,H
take
H
;
x is strict Morphism of G,H
thus
x is
strict Morphism of
G,
H
by A2, A4, Def20;
verum
end;
thus
( ex
G,
H being
strict Element of
V st
x is
strict Morphism of
G,
H implies
x in T )
verum
end;
then reconsider T9 = T as GroupMorphism_DOMAIN by Def16;
take
T9
; for x being object 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 object holds
( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
by A1; verum