let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let T be linear-transformation of V,W; :: thesis: for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let y be Element of W; :: thesis: ( y in im T iff ex x being Element of V st y = T . x )
A1: ( y in im T implies ex x being Element of V st y = T . x )

proof

assume y in im T ; :: thesis: ex x being Element of V st y = T . x
then reconsider y = y as Element of (im T) ;
[#] (im T) = T .: ([#] V) by Def2;
then consider x being object such that
x in dom T and
A2: x in [#] V and
A3: y = T . x by FUNCT_1:def 6;
reconsider x = x as Element of V by A2;
take x ; :: thesis: y = T . x
thus y = T . x by A3; :: thesis: verum

end;

( ex x being Element of V st y = T . x implies y in im T )

proof

assume A4: ex x being Element of V st y = T . x ; :: thesis: y in im T
dom T = [#] V by Th7;
then y in T .: ([#] V) by A4, FUNCT_1:def 6;
then y in [#] (im T) by Def2;
hence y in im T ; :: thesis: verum

end;

hence ( y in im T iff ex x being Element of V st y = T . x ) by A1; :: thesis: verum