let K be Ring; :: thesis: for V, U being VectSp of K
for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st
( T = CQFunctional f & T is bijective )

let V, U be VectSp of K; :: thesis: for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st
( T = CQFunctional f & T is bijective )

let f be linear-transformation of V,U; :: thesis: ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st
( T = CQFunctional f & T is bijective )

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 () iff x in rng f )
proof
let x be object ; :: thesis: ( x in rng () iff x in rng f )
hereby :: thesis: ( x in rng f implies x in rng () )
assume x in rng () ; :: thesis: x in rng f
then consider z being object such that
Q12: ( z in dom () & x = () . 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 ;
hence x in rng f by ; :: thesis: verum
end;
assume x in rng f ; :: thesis: x in rng ()
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 () by ; :: thesis: verum
end;
then P1: rng () = the carrier of (im f) by ;
the carrier of (VectQuot (V,(ker f))) = dom () by FUNCT_2:def 1;
then reconsider T = CQFunctional f as Function of the carrier of (VectQuot (V,(ker f))), the carrier of (im f) by ;
A1: T is onto by ;
set Tq = CQFunctional f;
now :: thesis: for A, B being Vector of (VectQuot (V,(ker f))) holds T . (A + B) = (T . A) + (T . B)
let A, B be Vector of (VectQuot (V,(ker f))); :: thesis: T . (A + B) = (T . A) + (T . B)
thus T . (A + B) = (() . A) + (() . B) by VECTSP_1:def 20
.= (T . A) + (T . B) by VECTSP_4:13 ; :: thesis: verum
end;