let I be set ; :: thesis: for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"
let A be V2() 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]
consider f being Function of NAT,(A . i) such that
A3: rng f = A . i by A2, CARD_3:96;
take f ; :: thesis: S₁[i,f]
thus S₁[i,f] 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 15 :: 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:7;
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 rng (F . i) = A . i )
assume i in I ; :: thesis: rng (F . i) = A . i
then ex f being Function of NAT,(A . i) st
( F . i = f & rng f = A . i ) by A4;
hence rng (F . i) = A . i ; :: thesis: verum