let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )

let V be finite-dimensional VectSp of K; :: thesis: for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )

let W be Subspace of V; :: thesis: ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in S holds
T . v = v + W ) )

set S = the Linear_Compl of W;
set aC = addCoset (V,W);
set C = CosetSet (V,W);
set Vq = VectQuot (V,W);
defpred S1[ Vector of V, Vector of (VectQuot (V,W))] means \$2 = \$1 + W;
A2: now :: thesis: for v being Vector of V ex y being Vector of (VectQuot (V,W)) st S1[v,y]
let v be Vector of V; :: thesis: ex y being Vector of (VectQuot (V,W)) st S1[v,y]
reconsider y = v + W as Vector of (VectQuot (V,W)) by VECTSP10:23;
take y = y; :: thesis: S1[v,y]
thus S1[v,y] ; :: thesis: verum
end;
consider ff being Function of the carrier of V, the carrier of (VectQuot (V,W)) such that
A7: for v being Vector of V holds S1[v,ff . v] from set T = ff | the carrier of the Linear_Compl of W;
S1: the carrier of the Linear_Compl of W c= the carrier of V by VECTSP_4:def 2;
then reconsider T = ff | the carrier of the Linear_Compl of W as Function of the carrier of the Linear_Compl of W, the carrier of (VectQuot (V,W)) by FUNCT_2:32;
P1: for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W
proof
let v be Vector of V; :: thesis: ( v in the Linear_Compl of W implies T . v = v + W )
assume v in the Linear_Compl of W ; :: thesis: T . v = v + W
hence T . v = ff . v by FUNCT_1:49
.= v + W by A7 ;
:: thesis: verum
end;
now :: thesis: for a, b being Vector of the Linear_Compl of W holds T . (a + b) = (T . a) + (T . b)
let a, b be Vector of the Linear_Compl of W; :: thesis: T . (a + b) = (T . a) + (T . b)
reconsider a1 = a, b1 = b as Vector of V by S1;
A91: ( a1 in the Linear_Compl of W & b1 in the Linear_Compl of W ) ;
a1 + b1 = a + b by VECTSP_4:13;
then A94: a1 + b1 in the Linear_Compl of W ;
A95: T . a = a1 + W by ;
A96: T . b = b1 + W by ;
thus T . (a + b) = T . (a1 + b1) by VECTSP_4:13
.= (a1 + b1) + W by
.= (T . a) + (T . b) by ; :: thesis: verum
end;
now :: thesis: for a being Vector of the Linear_Compl of W
for r being Element of K holds T . (r * a) = r * (T . a)
let a be Vector of the Linear_Compl of W; :: 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)
reconsider a1 = a as Vector of V by S1;
A91: a1 in the Linear_Compl of W ;
r * a = r * a1 by VECTSP_4:14;
then A94: r * a1 in the Linear_Compl of W ;
A95: T . a = a1 + W by ;
thus T . (r * a) = T . (r * a1) by VECTSP_4:14
.= (r * a1) + W by
.= r * (T . a) by ; :: thesis: verum
end;
then T is homogeneous ;
then reconsider T = T as linear-transformation of the Linear_Compl of W,(VectQuot (V,W)) by AD;
A100: V is_the_direct_sum_of the Linear_Compl of W,W by VECTSP_5:def 5;
the carrier of (VectQuot (V,W)) c= rng T
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (VectQuot (V,W)) or y in rng T )
assume y in the carrier of (VectQuot (V,W)) ; :: thesis: y in rng T
then consider a being Vector of V such that
A10: y = a + W by VECTSP10:22;
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = the Linear_Compl of W + W by ;
then a in the Linear_Compl of W + W ;
then consider s, w being Element of V such that
A12: ( s in the Linear_Compl of W & w in W & a = s + w ) by VECTSP_5:1;
reconsider s0 = s as Vector of the Linear_Compl of W by A12;
reconsider B = s + W as Vector of (VectQuot (V,W)) by VECTSP10:23;
reconsider A = a + W, Z = w + W as Vector of (VectQuot (V,W)) by VECTSP10:23;
Z = zeroCoset (V,W) by
.= 0. (VectQuot (V,W)) by VECTSP10:def 6 ;
then A13: B = B + Z
.= A by ;
T . s0 = y by A10, A12, A13, P1;
hence y in rng T by FUNCT_2:4; :: thesis: verum
end;
then rng T = the carrier of (VectQuot (V,W)) ;
then A14: T is onto ;
X1: for x1, x2 being object st x1 in the carrier of the Linear_Compl of W & x2 in the carrier of the Linear_Compl of W & T . x1 = T . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in the carrier of the Linear_Compl of W & x2 in the carrier of the Linear_Compl of W & T . x1 = T . x2 implies x1 = x2 )
assume A15: ( x1 in the carrier of the Linear_Compl of W & x2 in the carrier of the Linear_Compl of W & T . x1 = T . x2 ) ; :: thesis: x1 = x2
then reconsider a1 = x1, a2 = x2 as Vector of V by S1;
A16: ( a1 in the Linear_Compl of W & a2 in the Linear_Compl of W ) by A15;
A17: T . x1 = a1 + W by ;
T . x2 = a2 + W by ;
then consider w being Element of V such that
A19: ( w in W & a2 = a1 + w ) by ;
A20: a2 - a1 = w + (a1 - a1) by
.= w + (0. V) by VECTSP_1:19
.= w ;
a2 - a1 in the Linear_Compl of W by ;
then a2 - a1 in the Linear_Compl of W /\ W by ;
then a2 - a1 in (0). V by ;
then a2 - a1 = 0. V by VECTSP_4:35;
hence x1 = x2 by RLVECT_1:21; :: thesis: verum
end;
take the Linear_Compl of W ; :: thesis: ex T being linear-transformation of the Linear_Compl of W,(VectQuot (V,W)) st
( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) )

take T ; :: thesis: ( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) )

thus ( T is bijective & ( for v being Vector of V st v in the Linear_Compl of W holds
T . v = v + W ) ) by ; :: thesis: verum