let I be set ; :: thesis: for A being non-empty ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
let A be non-empty ManySortedSet of I; :: thesis: for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
let B be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,{B} holds F is "onto"
let F be ManySortedFunction of A,{B}; :: thesis: F is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng (F . i) = {B} . i )
assume A1: i in I ; :: thesis: rng (F . i) = {B} . i
then ( {B} . i = {(B . i)} & F . i is Function of (A . i),({B} . i) ) by PBOOLE:def 15, PZFMISC1:def 1;
hence rng (F . i) = {B} . i by A1, Th2; :: thesis: verum