deffunc H1( set ) -> set = { NetStr(# $1,r,f #) where r is Relation of $1,$1, f is Element of Funcs ($1, the carrier of X) : NetStr(# $1,r,f #) is net of X } ;
set I = the_universe_of the carrier of X;
consider M being ManySortedSet of the_universe_of the carrier of X such that
A1:
for i being set st i in the_universe_of the carrier of X holds
M . i = H1(i)
from PBOOLE:sch 7();
take IT = Union M; for x being object holds
( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
let x be object ; ( x in IT iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) )
A2:
Union M = union (rng M)
by CARD_3:def 4;
hereby ( ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) implies x in IT )
assume
x in IT
;
ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X )then consider y being
set such that A3:
x in y
and A4:
y in rng M
by A2, TARSKI:def 4;
consider z being
object such that A5:
z in dom M
and A6:
M . z = y
by A4, FUNCT_1:def 3;
reconsider z =
z as
set by TARSKI:1;
z in the_universe_of the
carrier of
X
by A5;
then
y = { NetStr(# z,r,f #) where r is Relation of z,z, f is Element of Funcs (z, the carrier of X) : NetStr(# z,r,f #) is net of X }
by A1, A6;
then consider r being
Relation of
z,
z,
f being
Element of
Funcs (
z, the
carrier of
X)
such that A7:
x = NetStr(#
z,
r,
f #)
and A8:
NetStr(#
z,
r,
f #) is
net of
X
by A3;
reconsider N =
NetStr(#
z,
r,
f #) as
strict net of
X by A8;
take N =
N;
( N = x & the carrier of N in the_universe_of the carrier of X )thus
N = x
by A7;
the carrier of N in the_universe_of the carrier of Xthus
the
carrier of
N in the_universe_of the
carrier of
X
by A5;
verum
end;
given N being strict net of X such that A9:
N = x
and
A10:
the carrier of N in the_universe_of the carrier of X
; x in IT
set i = the carrier of N;
the carrier of N in dom M
by A10, PARTFUN1:def 2;
then A11:
M . the carrier of N in rng M
by FUNCT_1:def 3;
A12:
the mapping of N in Funcs ( the carrier of N, the carrier of X)
by FUNCT_2:8;
M . the carrier of N = { NetStr(# the carrier of N,r,f #) where r is Relation of the carrier of N, the carrier of N, f is Element of Funcs ( the carrier of N, the carrier of X) : NetStr(# the carrier of N,r,f #) is net of X }
by A1, A10;
then
N in M . the carrier of N
by A12;
hence
x in IT
by A2, A9, A11, TARSKI:def 4; verum