let I be set ; :: thesis: for A being V8() ManySortedSet of
for B being ManySortedSet of
for F being ManySortedFunction of A,{B} holds F is "onto"
let A be V8() ManySortedSet of ; :: thesis: for B being ManySortedSet of
for F being ManySortedFunction of A,{B} holds F is "onto"
let B be ManySortedSet of ; :: 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 A2: A . i <> {} ;
A3: {B} . i = {(B . i)} by A1, PZFMISC1:def 1;
F . i is Function of (A . i),({B} . i) by A1, PBOOLE:def 18;
hence rng (F . i) = {B} . i by A2, A3, Th2; :: thesis: verum