let S1, S2 be Subset-Family of (product (Carrier A)); :: thesis: ( ( for x being set holds
( x in S1 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) ) ) ) & ( for x being set holds
( x in S2 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) ) ) ) implies S1 = S2 )
assume that
A10: for x being set holds
( x in S1 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) ) ) and
A11: for x being set holds
( x in S2 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) ) ) ; :: thesis: S1 = S2
for x being object holds
( x in S1 iff x in S2 )
proof
let x be object ; :: thesis: ( x in S1 iff x in S2 )
( x in S1 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) ) ) by A10;
hence ( x in S1 iff x in S2 ) by A11; :: thesis: verum
end;
hence S1 = S2 by TARSKI:2; :: thesis: verum