let F1, F2 be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds
F1 . i = Funcs (X . i),(Y . i) ) & ( for i being set st i in I holds
F2 . i = Funcs (X . i),(Y . i) ) implies F1 = F2 )
assume that
A1: for i being set st i in I holds
F1 . i = Funcs (X . i),(Y . i) and
A2: for i being set st i in I holds
F2 . i = Funcs (X . i),(Y . i) ; :: thesis: F1 = F2

now

let i be set ; :: thesis: ( i in I implies F1 . i = F2 . i )
assume A3: i in I ; :: thesis: F1 . i = F2 . i
hence F1 . i = Funcs (X . i),(Y . i) by A1
.= F2 . i by A2, A3 ;
:: thesis: verum

end;

hence F1 = F2 by Th3; :: thesis: verum