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

proof

thus rng m c= B . i ; :: according to XBOOLE_0:def 10 :: thesis: B . i c= rng m
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B . i or a in rng m )
assume A3: a in B . i ; :: thesis: a in rng m
A4: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def 18;
A5: rng (F . i) = [|B,C|] . i by A1, A2, MSUALG_3:def 3;
A6: [|B,C|] . i <> {} by A2;
then consider z being set such that
A7: z in [|B,C|] . i by XBOOLE_0:def 1;
A8: z in [:(B . i),(C . i):] by A2, A7, PBOOLE:def 21;
set p = [a,(z `2 )];
A9: [a,(z `2 )] `1 in B . i by A3, MCART_1:7;
[a,(z `2 )] `2 = z `2 by MCART_1:7;
then [a,(z `2 )] `2 in C . i by A8, MCART_1:10;
then [a,(z `2 )] in [:(B . i),(C . i):] by A9, MCART_1:11;
then [a,(z `2 )] in [|B,C|] . i by A2, PBOOLE:def 21;
then consider b being set such that
A10: b in A . i and
A11: (F . i) . b = [a,(z `2 )] by A4, A5, FUNCT_2:17;
A12: dom (F . i) = A . i by A4, A6, FUNCT_2:def 1;
B . i <> {} by A2;
then A13: dom m = A . i by FUNCT_2:def 1;
m . b = (pr1 (F . i)) . b by A2, Def1
.= [a,(z `2 )] `1 by A10, A11, A12, MCART_1:def 12
.= a by MCART_1:7 ;
hence a in rng m by A10, A13, FUNCT_1:def 5; :: thesis: verum

end;

hence rng ((Mpr1 F) . i) = B . i ; :: thesis: verum