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