let V, W be Z_Module; :: thesis: for T being linear-transformation of V,W
for A, B, X being Subset of V st A c= the carrier of (ker T) & X = B \/ A holds
Lin (T .: X) = Lin (T .: B)
let T be linear-transformation of V,W; :: thesis: for A, B, X being Subset of V st A c= the carrier of (ker T) & X = B \/ A holds
Lin (T .: X) = Lin (T .: B)
let A, B, X be Subset of V; :: thesis: ( A c= the carrier of (ker T) & X = B \/ A implies Lin (T .: X) = Lin (T .: B) )
assume that
A1: A c= the carrier of (ker T) and
A2: X = B \/ A ; :: thesis: Lin (T .: X) = Lin (T .: B)
P1: T .: X = (T .: B) \/ (T .: A) by A2, RELAT_1:120;
thus Lin (T .: X) = (Lin (T .: B)) + (Lin (T .: A)) by P1, ZMODUL02:72
.= (Lin (T .: B)) + ((0). W) by LMTh441, A1
.= Lin (T .: B) by ZMODUL01:99 ; :: thesis: verum