let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let L be Scalar of K; :: thesis: for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
set V = V1;
set fi = f + ((- L) * (id V1));
let I be Linear_Compl of UnionKers (f + ((- L) * (id V1))); :: thesis: for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1
let fI be linear-transformation of I,I; :: thesis: ( fI = f | I implies for v being Vector of I st fI . v = L * v holds
v = 0. V1 )
assume A1: fI = f | I ; :: thesis: for v being Vector of I st fI . v = L * v holds
v = 0. V1
A2: (f + ((- L) * (id V1))) | I is one-to-one by Th36;
let v be Vector of I; :: thesis: ( fI . v = L * v implies v = 0. V1 )
assume A3: fI . v = L * v ; :: thesis: v = 0. V1
reconsider v1 = v as Vector of V1 by VECTSP_4:18;
A4: f . v = fI . v by A1, FUNCT_1:72
.= L * v1 by A3, VECTSP_4:22 ;
((f + ((- L) * (id V1))) | I) . v1 = (f + ((- L) * (id V1))) . v1 by FUNCT_1:72
.= (f . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 5
.= (f . v1) + ((- L) * ((id V1) . v1)) by MATRLIN:def 6
.= (L * v1) + ((- L) * v1) by A4, FUNCT_1:35
.= (L + (- L)) * v1 by VECTSP_1:def 26
.= (0. K) * v1 by VECTSP_1:66
.= 0. V1 by VECTSP_1:59 ;
then ( v1 in ker ((f + ((- L) * (id V1))) | I) & ker ((f + ((- L) * (id V1))) | I) = (0). I ) by A2, MATRLIN2:43, RANKNULL:10;
hence v = 0. I by VECTSP_4:46
.= 0. V1 by VECTSP_4:19 ;
:: thesis: verum