let I be set ; for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
let A be ManySortedSet of I; for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
let B, C be V2() ManySortedSet of I; 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|]; ( F is "onto" implies Mpr1 F is "onto" )
assume A1:
F is "onto"
; Mpr1 F is "onto"
let i be set ; MSUALG_3:def 3 ( not i in I or rng ((Mpr1 F) . i) = B . i )
assume A2:
i in I
; rng ((Mpr1 F) . i) = B . i
then reconsider m = (Mpr1 F) . i as Function of (A . i),(B . i) by PBOOLE:def 15;
rng m = B . i
proof
thus
rng m c= B . i
;
XBOOLE_0:def 10 B . i c= rng m
let a be
object ;
TARSKI:def 3 ( not a in B . i or a in rng m )
assume A3:
a in B . i
;
a in rng m
consider z being
object such that A4:
z in [|B,C|] . i
by A2, XBOOLE_0:def 1;
set p =
[a,(z `2)];
z in [:(B . i),(C . i):]
by A2, A4, PBOOLE:def 16;
then A5:
[a,(z `2)] `2 in C . i
by MCART_1:10;
[a,(z `2)] `1 in B . i
by A3;
then
[a,(z `2)] in [:(B . i),(C . i):]
by A5, ZFMISC_1:def 2;
then A6:
[a,(z `2)] 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 = [a,(z `2)]
by A8, A6, FUNCT_2:11;
m . b =
(pr1 (F . i)) . b
by A2, Def1
.=
[a,(z `2)] `1
by A10, A11, A9, MCART_1:def 12
.=
a
;
hence
a in rng m
by A10, A7, FUNCT_1:def 3;
verum
end;
hence
rng ((Mpr1 F) . i) = B . i
; verum