let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )
let A, B be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )
let F be ManySortedFunction of A,B; :: thesis: ( F is "onto" iff rngs F = B )
A1: dom F = I by PARTFUN1:def 2;
thus ( F is "onto" implies rngs F = B ) :: thesis: ( rngs F = B implies F is "onto" )

proof

assume A2: F is "onto" ; :: thesis: rngs F = B

now :: thesis: for i being object st i in I holds
(rngs F) . i = B . i

let i be object ; :: thesis: ( i in I implies (rngs F) . i = B . i )
assume A3: i in I ; :: thesis: (rngs F) . i = B . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
rng f = B . i by A2, A3;
hence (rngs F) . i = B . i by A1, A3, FUNCT_6:22; :: thesis: verum

end;

hence rngs F = B ; :: thesis: verum

end;

assume A4: rngs F = 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 i in I ; :: thesis: rng (F . i) = B . i
hence rng (F . i) = B . i by A1, A4, FUNCT_6:22; :: thesis: verum