[:
X
,
Y
:]
c=
[:
X
,
Y
:]
;
then
reconsider
R
=
[:
X
,
Y
:]
as
Relation
of
X
,
Y
;
rng
R
=
Y
;
then
R
is
onto
by
FUNCT_2:def 3
;
hence
ex
b
_{1}
being
Relation
of
X
,
Y
st
b
_{1}
is
onto
;
:: thesis:
verum