let R be Ring; :: thesis: for V, W being LeftMod of R
for T being linear-transformation of V,W
for A being Subset of V st A c= the carrier of (ker T) holds
Lin (T .: A) = (0). W
let V, W be LeftMod of R; :: thesis: for T being linear-transformation of V,W
for A being Subset of V st A c= the carrier of (ker T) holds
Lin (T .: A) = (0). W
let T be linear-transformation of V,W; :: thesis: for A being Subset of V st A c= the carrier of (ker T) holds
Lin (T .: A) = (0). W
let A be Subset of V; :: thesis: ( A c= the carrier of (ker T) implies Lin (T .: A) = (0). W )
assume A1: A c= the carrier of (ker T) ; :: thesis: Lin (T .: A) = (0). W

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: Lin (T .: A) = (0). W

then T .: A = {} the carrier of W ;
hence Lin (T .: A) = (0). W by MOD_3:6; :: thesis: verum

end;

suppose A <> {} ; :: thesis: Lin (T .: A) = (0). W

then consider a being object such that
A6: a in A by XBOOLE_0:def 1;
A8: a in ker T by A1, A6;
reconsider a = a as Vector of V by A6;
A9: T . a = 0. W by A8, RANKNULL:10;
for x being object holds
( x in T .: A iff x in {(0. W)} )

proof

let x be object ; :: thesis: ( x in T .: A iff x in {(0. W)} )

hereby :: thesis: ( x in {(0. W)} implies x in T .: A )

assume x in T .: A ; :: thesis: x in {(0. W)}
then consider z being Element of V such that
A4: ( z in A & x = T . z ) by FUNCT_2:65;
z in ker T by A1, A4;
then T . z = 0. W by RANKNULL:10;
hence x in {(0. W)} by TARSKI:def 1, A4; :: thesis: verum

end;

assume x in {(0. W)} ; :: thesis: x in T .: A
then x = T . a by A9, TARSKI:def 1;
hence x in T .: A by FUNCT_2:35, A6; :: thesis: verum

end;

then T .: A = {(0. W)} by TARSKI:2;
hence Lin (T .: A) = (0). W by ZMODUL06:22; :: thesis: verum

end;

end;