let V be Z_Module; :: thesis: for W being free finite-rank Subspace of V
for a being Element of INT.Ring st a <> 0. INT.Ring holds
rank (a (*) W) = rank W
let W be free finite-rank Subspace of V; :: thesis: for a being Element of INT.Ring st a <> 0. INT.Ring holds
rank (a (*) W) = rank W
let a be Element of INT.Ring; :: thesis: ( a <> 0. INT.Ring implies rank (a (*) W) = rank W )
assume A1: a <> 0. INT.Ring ; :: thesis: rank (a (*) W) = rank W
defpred S₁[ Element of W, object ] means $2 = a * $1;
P0: for x being Element of W ex y being Element of (a (*) W) st S₁[x,y]

proof

let x be Element of W; :: thesis: ex y being Element of (a (*) W) st S₁[x,y]
a * x in the carrier of (a (*) W) ;
hence ex y being Element of (a (*) W) st S₁[x,y] ; :: thesis: verum

end;

consider F being Function of W,(a (*) W) such that
A2: for x being Element of W holds S₁[x,F . x] from FUNCT_2:sch 3(P0);
X1X: for x1, x2 being object st x1 in the carrier of W & x2 in the carrier of W & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in the carrier of W & x2 in the carrier of W & F . x1 = F . x2 implies x1 = x2 )
assume D1: ( x1 in the carrier of W & x2 in the carrier of W & F . x1 = F . x2 ) ; :: thesis: x1 = x2
reconsider xx1 = x1, xx2 = x2 as Element of W by D1;
( F . x1 = a * xx1 & F . x2 = a * xx2 ) by A2;
hence x1 = x2 by A1, ZMODUL01:10, D1; :: thesis: verum

end;

for y being object st y in the carrier of (a (*) W) holds
y in rng F

proof

let y be object ; :: thesis: ( y in the carrier of (a (*) W) implies y in rng F )
assume D1: y in the carrier of (a (*) W) ; :: thesis: y in rng F
consider v being Element of W such that
D2: y = a * v by D1;
F . v = a * v by A2;
hence y in rng F by D2, FUNCT_2:4; :: thesis: verum

end;

then X2X: the carrier of (a (*) W) c= rng F ;
B0: F is additive

proof

let x, y be Element of W; :: according to VECTSP_1:def 19 :: thesis: F . (x + y) = (F . x) + (F . y)
B03: F . x = a * x by A2;
B04: F . y = a * y by A2;
thus F . (x + y) = a * (x + y) by A2
.= (a * x) + (a * y) by VECTSP_1:def 14
.= (F . x) + (F . y) by ZMODUL01:28, B03, B04 ; :: thesis: verum

end;

for r being Element of INT.Ring
for x being Element of W holds F . (r * x) = r * (F . x)

proof

let r be Element of INT.Ring; :: thesis: for x being Element of W holds F . (r * x) = r * (F . x)
let x be Element of W; :: thesis: F . (r * x) = r * (F . x)
thus F . (r * x) = a * (r * x) by A2
.= (a * r) * x by VECTSP_1:def 16
.= r * (a * x) by VECTSP_1:def 16
.= r * (F . x) by ZMODUL01:29, A2 ; :: thesis: verum

end;

then reconsider F = F as linear-transformation of W,(a (*) W) by B0, MOD_2:def 2;
reconsider aW = a (*) W as free finite-rank Z_Module ;
reconsider W0 = W as free finite-rank Z_Module ;
reconsider F = F as linear-transformation of W0,aW ;
( F is one-to-one & F is onto ) by X1X, FUNCT_2:19, X2X, FUNCT_2:def 3, XBOOLE_0:def 10;
hence rank (a (*) W) = rank W by HM15; :: thesis: verum