defpred S1[ object ] means ex B being Segre-like ManySortedSubset of Carrier A st
( $1 = product B & ex i being Element of I st B . i is Block of (A . i) );
consider S being set such that
A1: for x being object holds
( x in S iff ( x in bool (product (Carrier A)) & S1[x] ) ) from XBOOLE_0:sch 1();
 S c= bool (product (Carrier A)) by A1;
then reconsider S = S as Subset-Family of (product (Carrier A)) ;
take S ; :: thesis: for x being set holds
( x in S iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )
let x be set ; :: thesis: ( x in S iff ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )
thus ( x in S implies ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) by A1; :: thesis: ( ex B being Segre-like ManySortedSubset of Carrier A st
( x = product B & ex i being Element of I st B . i is Block of (A . i) ) implies x in S )
given B being Segre-like ManySortedSubset of Carrier A such that A2: x = product B and
A3: ex i being Element of I st B . i is Block of (A . i) ; :: thesis: x in S
x c= product (Carrier A)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in product (Carrier A) )
assume a in x ; :: thesis: a in product (Carrier A)
then consider g being Function such that
A4: g = a and
A5: dom g = dom B and
A6: for y being object st y in dom B holds
g . y in B . y by A2, CARD_3:def 5;
A7: for y being object st y in dom (Carrier A) holds
g . y in (Carrier A) . y
proof
let y be object ; :: thesis: ( y in dom (Carrier A) implies g . y in (Carrier A) . y )
assume y in dom (Carrier A) ; :: thesis: g . y in (Carrier A) . y
then A8: y in I by PARTFUN1:def 2;
then y in dom g by A5, PARTFUN1:def 2;
then A9: g . y in B . y by A5, A6;
B c= Carrier A by PBOOLE:def 18;
then B . y c= (Carrier A) . y by A8;
hence g . y in (Carrier A) . y by A9; :: thesis: verum
end;
dom g = I by A5, PARTFUN1:def 2
.= dom (Carrier A) by PARTFUN1:def 2 ;
hence a in product (Carrier A) by A4, A7, CARD_3:def 5; :: thesis: verum
end;
hence x in S by A1, A2, A3; :: thesis: verum