let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of {A},B holds F is "1-1"
let F be ManySortedFunction of {A},B; :: thesis: F is "1-1"

now :: thesis: for i being set st i in I holds
F . i is one-to-one

let i be set ; :: thesis: ( i in I implies F . i is one-to-one )
assume i in I ; :: thesis: F . i is one-to-one
then ( {A} . i = {(A . i)} & F . i is Function of ({A} . i),(B . i) ) by PBOOLE:def 15, PZFMISC1:def 1;
hence F . i is one-to-one by PARTFUN1:17; :: thesis: verum

end;

hence F is "1-1" by MSUALG_3:1; :: thesis: verum