defpred S₁[ set ] 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 set holds
( x in S iff ( x in bool (product (Carrier A)) & S₁[x] ) ) from XBOOLE_0:sch 1();
S c= bool (product (Carrier A))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in S or a in bool (product (Carrier A)) )
assume a in S ; :: thesis: a in bool (product (Carrier A))
hence a in bool (product (Carrier A)) by A1; :: thesis: verum

end;

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 & 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 set ; :: 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
A3: ( g = a & dom g = dom B & ( for y being set st y in dom B holds
g . y in B . y ) ) by A2, CARD_3:def 5;
A4: dom g = I by A3, PARTFUN1:def 4
.= dom (Carrier A) by PARTFUN1:def 4 ;
for y being set st y in dom (Carrier A) holds
g . y in (Carrier A) . y

proof

let y be set ; :: 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 A5: y in I by PARTFUN1:def 4;
then y in dom g by A3, PARTFUN1:def 4;
then A6: g . y in B . y by A3;
B c= Carrier A by PBOOLE:def 23;
then B . y c= (Carrier A) . y by A5, PBOOLE:def 5;
hence g . y in (Carrier A) . y by A6; :: thesis: verum

end;

hence a in product (Carrier A) by A3, A4, CARD_3:def 5; :: thesis: verum

end;

hence x in S by A1, A2; :: thesis: verum