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 Def4;
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 ; :: 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, Def4; :: 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, Def4;
hence x in T by A6, TARSKI:def 4; :: thesis: verum

end;

end;

now :: thesis: for x being Element of T holds x is strict LModMorphism of R

let x be Element of T; :: thesis: x is strict LModMorphism of R
ex G, H being strict Element of V st x is strict Morphism of G,H by A1;
hence x is strict LModMorphism of R ; :: thesis: verum

end;

then reconsider T9 = T as LModMorphism_DOMAIN of R by Def2;
take T9 ; :: thesis: 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; :: thesis: verum