let I be set ; :: thesis: for A being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let A be ManySortedSet of I; :: thesis: for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let B, C be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
let F be ManySortedFunction of A,[|B,C|]; :: thesis: ( F is "onto" implies Mpr2 F is "onto" )
assume A1: F is "onto" ; :: thesis: Mpr2 F is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng ((Mpr2 F) . i) = C . i )
assume A2: i in I ; :: thesis: rng ((Mpr2 F) . i) = C . i
then reconsider m = (Mpr2 F) . i as Function of (A . i),(C . i) by PBOOLE:def 15;
rng m = C . i

proof

thus rng m c= C . i ; :: according to XBOOLE_0:def 10 :: thesis: C . i c= rng m
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in C . i or a in rng m )
assume A3: a in C . i ; :: thesis: a in rng m
consider z being object such that
A4: z in [|B,C|] . i by A2, XBOOLE_0:def 1;
set p = [(z `1),a];
z in [:(B . i),(C . i):] by A2, A4, PBOOLE:def 16;
then A5: [(z `1),a] `1 in B . i by MCART_1:10;
[(z `1),a] `2 in C . i by A3;
then [(z `1),a] in [:(B . i),(C . i):] by A5, ZFMISC_1:def 2;
then A6: [(z `1),a] in [|B,C|] . i by A2, PBOOLE:def 16;
A7: dom m = A . i by A2, FUNCT_2:def 1;
A8: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def 15;
then A9: dom (F . i) = A . i by A2, FUNCT_2:def 1;
rng (F . i) = [|B,C|] . i by A1, A2;
then consider b being object such that
A10: b in A . i and
A11: (F . i) . b = [(z `1),a] by A8, A6, FUNCT_2:11;
m . b = (pr2 (F . i)) . b by A2, Def2
.= [(z `1),a] `2 by A10, A11, A9, MCART_1:def 13
.= a ;
hence a in rng m by A10, A7, FUNCT_1:def 3; :: thesis: verum

end;

hence rng ((Mpr2 F) . i) = C . i ; :: thesis: verum