let V be Z_Module; :: thesis: for I being finite Subset of V
for W being Submodule of V
for a being Element of INT.Ring st a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W
let I be finite Subset of V; :: thesis: for W being Submodule of V
for a being Element of INT.Ring st a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W
let W be Submodule of V; :: thesis: for a being Element of INT.Ring st a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W
let a be Element of INT.Ring; :: thesis: ( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) implies for v being VECTOR of V st v in Lin I holds
a * v in W )
assume that
a <> 0. INT.Ring and
AS2: for v being VECTOR of V st v in I holds
a * v in W ; :: thesis: for v being VECTOR of V st v in Lin I holds
a * v in W
defpred S₁[ Nat] means for I being finite Subset of V st card I = $1 & ( for v being VECTOR of V st v in I holds
a * v in W ) holds
for v being VECTOR of V st v in Lin I holds
a * v in W;
P1: S₁[ 0 ]

proof

let I be finite Subset of V; :: thesis: ( card I = 0 & ( for v being VECTOR of V st v in I holds
a * v in W ) implies for v being VECTOR of V st v in Lin I holds
a * v in W )
assume that
A0: card I = 0 and
for v being VECTOR of V st v in I holds
a * v in W ; :: thesis: for v being VECTOR of V st v in Lin I holds
a * v in W
I = {} the carrier of V by A0;
then P1: Lin I = (0). V by ZMODUL02:67;
thus for v being VECTOR of V st v in Lin I holds
a * v in W :: thesis: verum

proof

let v be VECTOR of V; :: thesis: ( v in Lin I implies a * v in W )
assume v in Lin I ; :: thesis: a * v in W
then v in {(0. V)} by P1, VECTSP_4:def 3;
then v = 0. V by TARSKI:def 1;
then a * v = 0. V by ZMODUL01:1
.= 0. W by ZMODUL01:26 ;
hence a * v in W ; :: thesis: verum

end;

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
let I be finite Subset of V; :: thesis: ( card I = n + 1 & ( for v being VECTOR of V st v in I holds
a * v in W ) implies for v being VECTOR of V st v in Lin I holds
a * v in W )
assume that
A0: card I = n + 1 and
A1: for v being VECTOR of V st v in I holds
a * v in W ; :: thesis: for v being VECTOR of V st v in Lin I holds
a * v in W
not I is empty by A0;
then consider u being object such that
B3: u in I by XBOOLE_0:def 1;
reconsider u = u as VECTOR of V by B3;
set Iu = I \ {u};
{u} is Subset of I by B3, SUBSET_1:41;
then B6: card (I \ {u}) = (n + 1) - (card {u}) by A0, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Iu = I \ {u} as finite Subset of V ;
set Ku = {u};
E1: I = Iu \/ {u} by B3, XBOOLE_1:45, ZFMISC_1:31;
E3: Lin I = (Lin Iu) + (Lin {u}) by E1, ZMODUL02:72;
A4: for v being VECTOR of V st v in Iu holds
a * v in W

proof

let v be VECTOR of V; :: thesis: ( v in Iu implies a * v in W )
assume v in Iu ; :: thesis: a * v in W
then ( v in I & not v in {u} ) by XBOOLE_0:def 5;
hence a * v in W by A1; :: thesis: verum

end;

thus for v being VECTOR of V st v in Lin I holds
a * v in W :: thesis: verum

proof

let v be VECTOR of V; :: thesis: ( v in Lin I implies a * v in W )
assume v in Lin I ; :: thesis: a * v in W
then consider v1, v2 being VECTOR of V such that
F1: v1 in Lin Iu and
F2: v2 in Lin {u} and
F3: v = v1 + v2 by E3, ZMODUL01:92;
F4: a * v1 in W by F1, A4, B1, B6;
consider i being Element of INT.Ring such that
F5: v2 = i * u by F2, ZMODUL06:19;
F6: a * v2 = (a * i) * u by F5, VECTSP_1:def 16
.= (i * a) * u
.= i * (a * u) by VECTSP_1:def 16 ;
F7: a * v2 in W by A1, B3, F6, ZMODUL01:37;
( a * v = a * (v1 + v2) & a * (v1 + v2) = (a * v1) + (a * v2) ) by F3, VECTSP_1:def 14;
hence a * v in W by ZMODUL01:36, F7, F4; :: thesis: verum

end;

end;

X1: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
card I is Nat ;
hence for v being VECTOR of V st v in Lin I holds
a * v in W by X1, AS2; :: thesis: verum