let I be set ; :: thesis: for A being V8() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT ,A st F is "onto"
let A be V8() V32() ManySortedSet of I; :: thesis: ex F being ManySortedFunction of I --> NAT ,A st F is "onto"
defpred S₁[ set , set ] means ex f being Function of NAT ,(A . $1) st
( $2 = f & rng f = A . $1 );
A1: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume A2: i in I ; :: thesis: ex j being set st S₁[i,j]
then A . i is finite by FINSET_1:def 4;
then consider f being Function of NAT ,(A . i) such that
A3: rng f = A . i by A2, CARD_3:146;
take j = f; :: thesis: S₁[i,j]
thus S₁[i,j] by A3; :: thesis: verum

end;

consider F being ManySortedSet of I such that
A4: for i being set st i in I holds
S₁[i,F . i] from PBOOLE:sch 3(A1);
F is ManySortedFunction of I --> NAT ,A

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I or F . i is Element of bool [:((I --> NAT ) . i),(A . i):] )
assume i in I ; :: thesis: F . i is Element of bool [:((I --> NAT ) . i),(A . i):]
then ( ex f being Function of NAT ,(A . i) st
( F . i = f & rng f = A . i ) & (I --> NAT ) . i = NAT ) by A4, FUNCOP_1:13;
hence F . i is Element of bool [:((I --> NAT ) . i),(A . i):] ; :: thesis: verum

end;

then reconsider F = F as ManySortedFunction of I --> NAT ,A ;
take F ; :: thesis: F is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or proj2 (F . i) = A . i )
assume i in I ; :: thesis: proj2 (F . i) = A . i
then ex f being Function of NAT ,(A . i) st
( F . i = f & rng f = A . i ) by A4;
hence proj2 (F . i) = A . i ; :: thesis: verum