let X1, X2 be ManySortedSet of I; :: thesis: ( ( for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & X1 . i = Intersect Q ) ) & ( for i being object 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 A3: ( ( for i being object st i in I holds
ex Q1 being Subset-Family of (M . i) st
( Q1 = SF . i & X1 . i = Intersect Q1 ) ) & ( for i being object 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 :: thesis: for i being object st i in I holds
X1 . i = X2 . i
let i be object ; :: thesis: ( i in I implies X1 . i = X2 . i )
assume i in I ; :: thesis: X1 . i = X2 . i
then ( ex Q1 being Subset-Family of (M . i) st
( Q1 = SF . i & X1 . i = Intersect Q1 ) & ex Q2 being Subset-Family of (M . i) st
( Q2 = SF . i & X2 . i = Intersect Q2 ) ) by A3;
hence X1 . i = X2 . i ; :: thesis: verum
end;
hence X1 = X2 ; :: thesis: verum