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 (CQFunctional f) iff x in rng f )

proof

let x be object ; :: thesis: ( x in rng (CQFunctional f) iff x in rng f )

hereby :: thesis: ( x in rng f implies x in rng (CQFunctional f) )

assume x in rng (CQFunctional f) ; :: thesis: x in rng f
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: verum

end;

assume x in rng f ; :: thesis: x in rng (CQFunctional f)
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: verum

end;

then P1: rng (CQFunctional f) = the carrier of (im f) by Q0, TARSKI:2;
the carrier of (VectQuot (V,(ker f))) = dom (CQFunctional f) 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 FUNCT_2:2, P1;
A1: T is onto by Q0, Q1, TARSKI:2;
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) = ((CQFunctional f) . A) + ((CQFunctional f) . B) by VECTSP_1:def 20
.= (T . A) + (T . B) by VECTSP_4:13 ; :: thesis: verum

end;

then AD: T is additive ;

now :: thesis: for A being Vector of (VectQuot (V,(ker f)))
for r being Element of K holds T . (r * A) = r * (T . A)

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

end;

then T is homogeneous ;
then reconsider T = T as linear-transformation of (VectQuot (V,(ker f))),(im f) by AD;
take T ; :: thesis: ( T = CQFunctional f & T is bijective )
thus ( T = CQFunctional f & T is bijective ) by A1; :: thesis: verum