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 holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
let L be Scalar of K; :: thesis: f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))
set fid = f + (L * (id V1));
set U = UnionKers (f + (L * (id V1)));
reconsider fidU = (f + (L * (id V1))) | (UnionKers (f + (L * (id V1)))) as linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1)))) by Th30;
rng (f | (UnionKers (f + (L * (id V1))))) c= the carrier of (UnionKers (f + (L * (id V1))))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (UnionKers (f + (L * (id V1))))) or y in the carrier of (UnionKers (f + (L * (id V1)))) )
assume A1: y in rng (f | (UnionKers (f + (L * (id V1))))) ; :: thesis: y in the carrier of (UnionKers (f + (L * (id V1))))
consider x being set such that
A2: ( x in dom (f | (UnionKers (f + (L * (id V1))))) & (f | (UnionKers (f + (L * (id V1))))) . x = y ) by A1, FUNCT_1:def 5;
A3: x in the carrier of (UnionKers (f + (L * (id V1)))) by A2, FUNCT_2:def 1;
then A4: x in UnionKers (f + (L * (id V1))) by STRUCT_0:def 5;
then x in V1 by VECTSP_4:17;
then reconsider v = x as Vector of V1 by STRUCT_0:def 5;
(f + (L * (id V1))) . v = (f . v) + ((L * (id V1)) . v) by MATRLIN:def 5
.= (f . v) + (L * ((id V1) . v)) by MATRLIN:def 6
.= (f . v) + (L * v) by FUNCT_1:35 ;
then A5: ((f + (L * (id V1))) . v) + ((- L) * v) = (f . v) + ((L * v) + ((- L) * v)) by RLVECT_1:def 6
.= (f . v) + ((L + (- L)) * v) by VECTSP_1:def 26
.= (f . v) + ((0. K) * v) by VECTSP_1:63
.= (f . v) + (0. V1) by VECTSP_1:59
.= f . v by RLVECT_1:def 7 ;
dom fidU = the carrier of (UnionKers (f + (L * (id V1)))) by FUNCT_2:def 1;
then ( fidU . v = (f + (L * (id V1))) . v & fidU /. v = fidU . v ) by A3, FUNCT_1:70, PARTFUN1:def 8;
then ( (f + (L * (id V1))) . v in UnionKers (f + (L * (id V1))) & (- L) * v in UnionKers (f + (L * (id V1))) ) by A4, STRUCT_0:def 5, VECTSP_4:29;
then ( f . v in UnionKers (f + (L * (id V1))) & (f | (UnionKers (f + (L * (id V1))))) . v = f . v ) by A2, A5, FUNCT_1:70, VECTSP_4:28;
hence y in the carrier of (UnionKers (f + (L * (id V1)))) by A2, STRUCT_0:def 5; :: thesis: verum

end;

hence f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1)))) by Lm1, FUNCT_2:8; :: thesis: verum