let R be Ring; :: thesis: for V, W being LeftMod of R
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 V, W be LeftMod of R; :: 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, MOD_3:12
.= (Lin (T .: B)) + ((0). W) by LMTh441, A1
.= Lin (T .: B) by VECTSP_5:9 ; :: thesis: verum