let I be set ; :: thesis: for A being V8() V31() ManySortedSet of ex F being ManySortedFunction of I --> NAT ,A st F is "onto"
let A be V8() V31() ManySortedSet of ; :: 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 i in I ; :: thesis: ex j being set st S₁[i,j]
then ( not A . i is empty & A . i is finite ) by FINSET_1:def 4;
then consider f being Function of NAT ,(A . i) such that
A2: rng f = A . i by CARD_3:146;
take j = f; :: thesis: S₁[i,j]
thus S₁[i,j] by A2; :: thesis: verum

end;

consider F being ManySortedSet of such that
A3: 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 A4: i in I ; :: thesis: F . i is Element of bool [:((I --> NAT ) . i),(A . i):]
then consider f being Function of NAT ,(A . i) such that
A5: F . i = f and
rng f = A . i by A3;
(I --> NAT ) . i = NAT by A4, FUNCOP_1:13;
hence F . i is Element of bool [:((I --> NAT ) . i),(A . i):] by A5; :: 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 rng (F . i) = A . i )
assume i in I ; :: thesis: rng (F . i) = A . i
then consider f being Function of NAT ,(A . i) such that
A6: ( F . i = f & rng f = A . i ) by A3;
thus rng (F . i) = A . i by A6; :: thesis: verum