let K be Ring; :: thesis:
let V, U be VectSp of K; :: thesis:
let f be linear-transformation of V,U; :: thesis:
set T = CQFunctional f;
set Vq = VectQuot (V,(ker f));
Q0: the carrier of (im f) = [#] (im f)
.= f .: ([#] V) by RANKNULL:def 2
.= f .: (dom f) by FUNCT_2:def 1
.= rng f by RELAT_1:113 ;
Q1: for x being object holds
( x in rng (CQFunctional f) iff x in rng f )

let x be object ; :: thesis:

assume x in rng (CQFunctional f) ; :: thesis:
then consider z being object such that
Q12: ( z in dom (CQFunctional f) & x = (CQFunctional f) . z ) by FUNCT_1:def 3;
reconsider z = z as Vector of (VectQuot (V,(ker f))) by Q12;
consider a being Vector of V such that
A14: z = a + (ker f) by VECTSP10:22;
(CQFunctional f) . z = f . a by A14, Def12;
hence x in rng f by Q12, FUNCT_2:4; :: thesis:

end;

assume x in rng f ; :: thesis:
then consider a being object such that
Q12: ( a in dom f & x = f . a ) by FUNCT_1:def 3;
reconsider a = a as Vector of V by Q12;
reconsider z = a + (ker f) as Vector of (VectQuot (V,(ker f))) by VECTSP10:23;
(CQFunctional f) . z = f . a by Def12;
hence x in rng (CQFunctional f) by Q12, FUNCT_2:4; :: thesis:

end;

let A, B be Vector of (VectQuot (V,(ker f))); :: thesis:
thus T . (A + B) = ((CQFunctional f) . A) + ((CQFunctional f) . B) by VECTSP_1:def 20
.= (T . A) + (T . B) by VECTSP_4:13 ; :: thesis:

end;

let A be Vector of (VectQuot (V,(ker f))); :: thesis:
let r be Element of K; :: thesis:
thus T . (r * A) = r * ((CQFunctional f) . A) by MOD_2:def 2
.= r * (T . A) by VECTSP_4:14 ; :: thesis:

end;