let X1, X2 be ManySortedSet of ; :: thesis: ( ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & X1 . i = Intersect Q ) ) & ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & X2 . i = Intersect Q ) ) implies X1 = X2 )
assume that
A4: for i being set st i in I holds
ex Q1 being Subset-Family of (M . i) st
( Q1 = SF . i & X1 . i = Intersect Q1 ) and
A5: for i being set st i in I holds
ex Q2 being Subset-Family of (M . i) st
( Q2 = SF . i & X2 . i = Intersect Q2 ) ; :: thesis: X1 = X2

now

let i be set ; :: thesis: ( i in I implies X1 . i = X2 . i )
assume A6: i in I ; :: thesis: X1 . i = X2 . i
then consider Q1 being Subset-Family of (M . i) such that
A7: ( Q1 = SF . i & X1 . i = Intersect Q1 ) by A4;
consider Q2 being Subset-Family of (M . i) such that
A8: ( Q2 = SF . i & X2 . i = Intersect Q2 ) by A5, A6;
thus X1 . i = X2 . i by A7, A8; :: thesis: verum

end;

hence X1 = X2 by PBOOLE:3; :: thesis: verum