let B, B1 be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds
B . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds
B1 . i = (F . i) .: (A . i) ) implies B = B1 )
assume that
A3: for i being set st i in I holds
B . i = (F . i) .: (A . i) and
A4: for i being set st i in I holds
B1 . i = (F . i) .: (A . i) ; :: thesis: B = B1

now :: thesis: for i being set st i in I holds
B . i = B1 . i

let i be set ; :: thesis: ( i in I implies B . i = B1 . i )
reconsider f = F . i as Function ;
assume A5: i in I ; :: thesis: B . i = B1 . i
then B . i = f .: (A . i) by A3;
hence B . i = B1 . i by A4, A5; :: thesis: verum

end;

hence B = B1 by Th3; :: thesis: verum