for y being object st y in the carrier of (VectQuot (V,W)) holds
ex x being object st
( x in the carrier of V & y = (ZQMorph (V,W)) . x )
proof
let y be
object ;
( y in the carrier of (VectQuot (V,W)) implies ex x being object st
( x in the carrier of V & y = (ZQMorph (V,W)) . x ) )
assume
y in the
carrier of
(VectQuot (V,W))
;
ex x being object st
( x in the carrier of V & y = (ZQMorph (V,W)) . x )
then reconsider A =
y as
Element of
CosetSet (
V,
W)
by VECTSP10:def 6;
A in CosetSet (
V,
W)
;
then consider A0 being
Coset of
W such that P0:
A = A0
;
consider v being
VECTOR of
V such that P1:
A0 = v + W
by VECTSP_4:def 6;
(ZQMorph (V,W)) . v = y
by P0, P1, defMophVW;
hence
ex
x being
object st
(
x in the
carrier of
V &
y = (ZQMorph (V,W)) . x )
;
verum
end;
then
rng (ZQMorph (V,W)) = the carrier of (VectQuot (V,W))
by FUNCT_2:10;
hence
ZQMorph (V,W) is onto
by FUNCT_2:def 3; verum