let V be free finite-rank Z_Module; :: thesis: ( rank V = 2 iff ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

A14: {u,v} is linearly-independent and

A15: (Omega). V = Lin {u,v} ; :: thesis: rank V = 2

A16: {u,v} is Basis of V by A14, A15, VECTSP_7:def 3;

card {u,v} = 2 by A13, CARD_2:57;

hence rank V = 2 by A16, ZMODUL03:def 5; :: thesis: verum

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )

hereby :: thesis: ( ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies rank V = 2 )

given u, v being VECTOR of V such that A13:
u <> v
and ( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies rank V = 2 )

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

assume rank V = 2 ; :: thesis: ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )

then A2: card I = 2 by A1, ZMODUL03:def 5;

then consider u being object such that

A3: u in I by CARD_1:27, XBOOLE_0:def 1;

reconsider u = u as VECTOR of V by A3;

A4: v in I and

A5: not v in {u} ;

reconsider v = v as VECTOR of V by A4;

A6: v <> u by A5, TARSKI:def 1;

then A11: I = {u,v} by A7;

then A12: {u,v} is linearly-independent by A1, VECTSP_7:def 3;

Lin {u,v} = (Omega). V by A1, A11, VECTSP_7:def 3;

hence ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; :: thesis: verum

end;A1: I is Basis of V by ZMODUL03:def 3;

assume rank V = 2 ; :: thesis: ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )

then A2: card I = 2 by A1, ZMODUL03:def 5;

then consider u being object such that

A3: u in I by CARD_1:27, XBOOLE_0:def 1;

reconsider u = u as VECTOR of V by A3;

now :: thesis: not I c= {u}

then consider v being object such that assume
I c= {u}
; :: thesis: contradiction

then card I <= card {u} by NAT_1:43;

then 2 <= 1 by A2, CARD_1:30;

hence contradiction ; :: thesis: verum

end;then card I <= card {u} by NAT_1:43;

then 2 <= 1 by A2, CARD_1:30;

hence contradiction ; :: thesis: verum

A4: v in I and

A5: not v in {u} ;

reconsider v = v as VECTOR of V by A4;

A6: v <> u by A5, TARSKI:def 1;

A7: now :: thesis: I c= {u,v}

{u,v} c= I
by A3, A4, TARSKI:def 2;assume
not I c= {u,v}
; :: thesis: contradiction

then consider w being object such that

A8: w in I and

A9: not w in {u,v} ;

{u,v,w} c= I by A3, A4, A8, ENUMSET1:def 1;

then A10: card {u,v,w} <= card I by NAT_1:43;

( w <> u & w <> v ) by A9, TARSKI:def 2;

then 3 <= 2 by A2, A6, A10, CARD_2:58;

hence contradiction ; :: thesis: verum

end;then consider w being object such that

A8: w in I and

A9: not w in {u,v} ;

{u,v,w} c= I by A3, A4, A8, ENUMSET1:def 1;

then A10: card {u,v,w} <= card I by NAT_1:43;

( w <> u & w <> v ) by A9, TARSKI:def 2;

then 3 <= 2 by A2, A6, A10, CARD_2:58;

hence contradiction ; :: thesis: verum

then A11: I = {u,v} by A7;

then A12: {u,v} is linearly-independent by A1, VECTSP_7:def 3;

Lin {u,v} = (Omega). V by A1, A11, VECTSP_7:def 3;

hence ex u, v being VECTOR of V st

( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; :: thesis: verum

A14: {u,v} is linearly-independent and

A15: (Omega). V = Lin {u,v} ; :: thesis: rank V = 2

A16: {u,v} is Basis of V by A14, A15, VECTSP_7:def 3;

card {u,v} = 2 by A13, CARD_2:57;

hence rank V = 2 by A16, ZMODUL03:def 5; :: thesis: verum