defpred S1[ object ] means ex g being Function st
( $1 = product g & g in product ((Seg n) --> X) );
consider Y being set such that
A1:
for x being object holds
( x in Y iff ( x in bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X))))) & S1[x] ) )
from XBOOLE_0:sch 1();
take
Y
; for f being object holds
( f in Y iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) )
now ( ( for x being object st x in Y holds
ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) ) & ( for x being object st ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) holds
x in Y ) )thus
for
x being
object st
x in Y holds
ex
g being
Function st
(
x = product g &
g in product ((Seg n) --> X) )
by A1;
for x being object st ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) holds
x in Ylet x be
object ;
( ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) implies x in Y )assume A2:
ex
g being
Function st
(
x = product g &
g in product ((Seg n) --> X) )
;
( ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) implies x in Y )given g being
Function such that A3:
x = product g
and A4:
g in product ((Seg n) --> X)
;
x in YA5:
dom g = dom ((Seg n) --> X)
by A4, CARD_3:9;
rng g c= Union ((Seg n) --> X)
then
Union g c= union (Union ((Seg n) --> X))
by ZFMISC_1:77;
then
Funcs (
(dom g),
(Union g))
c= Funcs (
(dom ((Seg n) --> X)),
(union (Union ((Seg n) --> X))))
by A5, FUNCT_5:56;
then A11:
bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X)))))
by ZFMISC_1:67;
product g c= Funcs (
(dom g),
(Union g))
by FUNCT_6:1;
hence
x in Y
by A2, A1, A3, A11;
verum end;
hence
for f being object holds
( f in Y iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) )
; verum