let V be RealUnitarySpace; :: thesis: for A, B being finite Subset of V st UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

defpred S_{1}[ Nat] means for n being Element of NAT

for A, B being finite Subset of V st card A = n & card B = $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( $1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) );

A1: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
_{1}[m]
from NAT_1:sch 2(A26, A1);

let A, B be finite Subset of V; :: thesis: ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent ) ; :: thesis: ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

hence ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A30; :: thesis: verum

( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

defpred S

for A, B being finite Subset of V st card A = n & card B = $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( $1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) );

A1: for m being Nat st S

S

proof

A26:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A2: S_{1}[m]
; :: thesis: S_{1}[m + 1]

let n be Element of NAT ; :: thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

let A, B be finite Subset of V; :: thesis: ( card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume that

A3: card A = n and

A4: card B = m + 1 and

A5: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and

A6: B is linearly-independent ; :: thesis: ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

consider v being object such that

A7: v in B by A4, CARD_1:27, XBOOLE_0:def 1;

reconsider v = v as VECTOR of V by A7;

set Bv = B \ {v};

A8: B \ {v} is linearly-independent by A6, RLVECT_3:5, XBOOLE_1:36;

{v} is Subset of B by A7, SUBSET_1:41;

then A9: card (B \ {v}) = (card B) - (card {v}) by CARD_2:44

.= (m + 1) - 1 by A4, CARD_1:30

.= m ;

then consider C being finite Subset of V such that

A10: C c= A and

A11: card C = n - m and

A12: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A8;

A13: not v in Lin (B \ {v}) by A6, A7, RUSUB_3:25;

then consider w being VECTOR of V such that

A17: w in C and

A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by A13, Th1;

set Cw = C \ {w};

((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by XBOOLE_1:9, XBOOLE_1:36;

then (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v}) by XBOOLE_1:9;

then A19: (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w}) by A7, Lm1;

{w} is Subset of C by A17, SUBSET_1:41;

then A20: card (C \ {w}) = (card C) - (card {w}) by CARD_2:44

.= (n - m) - 1 by A11, CARD_1:30

.= n - (m + 1) ;

C \ {w} c= C by XBOOLE_1:36;

then A21: C \ {w} c= A by A10;

((C \/ (B \ {v})) \ {w}) \/ {v} = ((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v} by XBOOLE_1:42

.= (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) by XBOOLE_1:4 ;

then Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is Subspace of Lin (B \/ (C \ {w})) by A19, RUSUB_3:7;

then A22: w in Lin (B \/ (C \ {w})) by A18, RUSUB_1:1;

A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by A17, Lm1, XBOOLE_1:36;

then Lin ((B \ {v}) \/ C) is Subspace of Lin (B \/ (C \ {w})) by RUSUB_3:27;

then A24: the carrier of (Lin ((B \ {v}) \/ C)) c= the carrier of (Lin (B \/ (C \ {w}))) by RUSUB_1:def 1;

the carrier of (Lin (B \/ (C \ {w}))) c= the carrier of V by RUSUB_1:def 1;

then the carrier of (Lin (B \/ (C \ {w}))) = the carrier of V by A12, A24;

then A25: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ (C \ {w})) by A12, RUSUB_1:24;

m <= n by A2, A3, A5, A9, A8;

then m < n by A14, XXREAL_0:1;

hence ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A21, A20, A25, NAT_1:13; :: thesis: verum

end;assume A2: S

let n be Element of NAT ; :: thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

let A, B be finite Subset of V; :: thesis: ( card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume that

A3: card A = n and

A4: card B = m + 1 and

A5: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and

A6: B is linearly-independent ; :: thesis: ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

consider v being object such that

A7: v in B by A4, CARD_1:27, XBOOLE_0:def 1;

reconsider v = v as VECTOR of V by A7;

set Bv = B \ {v};

A8: B \ {v} is linearly-independent by A6, RLVECT_3:5, XBOOLE_1:36;

{v} is Subset of B by A7, SUBSET_1:41;

then A9: card (B \ {v}) = (card B) - (card {v}) by CARD_2:44

.= (m + 1) - 1 by A4, CARD_1:30

.= m ;

then consider C being finite Subset of V such that

A10: C c= A and

A11: card C = n - m and

A12: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A8;

A13: not v in Lin (B \ {v}) by A6, A7, RUSUB_3:25;

A14: now :: thesis: not m = n

v in Lin ((B \ {v}) \/ C)
by A12;assume
m = n
; :: thesis: contradiction

then consider C being finite Subset of V such that

C c= A and

A15: card C = m - m and

A16: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A9, A8;

C = {} by A15;

then B \ {v} is Basis of V by A8, A16, RUSUB_3:def 2;

hence contradiction by A13, RUSUB_3:21; :: thesis: verum

end;then consider C being finite Subset of V such that

C c= A and

A15: card C = m - m and

A16: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A9, A8;

C = {} by A15;

then B \ {v} is Basis of V by A8, A16, RUSUB_3:def 2;

hence contradiction by A13, RUSUB_3:21; :: thesis: verum

then consider w being VECTOR of V such that

A17: w in C and

A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by A13, Th1;

set Cw = C \ {w};

((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by XBOOLE_1:9, XBOOLE_1:36;

then (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v}) by XBOOLE_1:9;

then A19: (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w}) by A7, Lm1;

{w} is Subset of C by A17, SUBSET_1:41;

then A20: card (C \ {w}) = (card C) - (card {w}) by CARD_2:44

.= (n - m) - 1 by A11, CARD_1:30

.= n - (m + 1) ;

C \ {w} c= C by XBOOLE_1:36;

then A21: C \ {w} c= A by A10;

((C \/ (B \ {v})) \ {w}) \/ {v} = ((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v} by XBOOLE_1:42

.= (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) by XBOOLE_1:4 ;

then Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is Subspace of Lin (B \/ (C \ {w})) by A19, RUSUB_3:7;

then A22: w in Lin (B \/ (C \ {w})) by A18, RUSUB_1:1;

A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by A17, Lm1, XBOOLE_1:36;

now :: thesis: for x being object st x in (B \ {v}) \/ C holds

x in the carrier of (Lin (B \/ (C \ {w})))

then
(B \ {v}) \/ C c= the carrier of (Lin (B \/ (C \ {w})))
;x in the carrier of (Lin (B \/ (C \ {w})))

let x be object ; :: thesis: ( x in (B \ {v}) \/ C implies x in the carrier of (Lin (B \/ (C \ {w}))) )

assume x in (B \ {v}) \/ C ; :: thesis: x in the carrier of (Lin (B \/ (C \ {w})))

then ( x in B \ {v} or x in C ) by XBOOLE_0:def 3;

then ( x in B or x in C \ {w} or x in {w} ) by A23, XBOOLE_0:def 3;

then ( x in B \/ (C \ {w}) or x in {w} ) by XBOOLE_0:def 3;

then ( x in Lin (B \/ (C \ {w})) or x = w ) by RUSUB_3:2, TARSKI:def 1;

hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22; :: thesis: verum

end;assume x in (B \ {v}) \/ C ; :: thesis: x in the carrier of (Lin (B \/ (C \ {w})))

then ( x in B \ {v} or x in C ) by XBOOLE_0:def 3;

then ( x in B or x in C \ {w} or x in {w} ) by A23, XBOOLE_0:def 3;

then ( x in B \/ (C \ {w}) or x in {w} ) by XBOOLE_0:def 3;

then ( x in Lin (B \/ (C \ {w})) or x = w ) by RUSUB_3:2, TARSKI:def 1;

hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22; :: thesis: verum

then Lin ((B \ {v}) \/ C) is Subspace of Lin (B \/ (C \ {w})) by RUSUB_3:27;

then A24: the carrier of (Lin ((B \ {v}) \/ C)) c= the carrier of (Lin (B \/ (C \ {w}))) by RUSUB_1:def 1;

the carrier of (Lin (B \/ (C \ {w}))) c= the carrier of V by RUSUB_1:def 1;

then the carrier of (Lin (B \/ (C \ {w}))) = the carrier of V by A12, A24;

then A25: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ (C \ {w})) by A12, RUSUB_1:24;

m <= n by A2, A3, A5, A9, A8;

then m < n by A14, XXREAL_0:1;

hence ( m + 1 <= n & ex C being finite Subset of V st

( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A21, A20, A25, NAT_1:13; :: thesis: verum

proof

A30:
for m being Nat holds S
let n be Element of NAT ; :: thesis: for A, B being finite Subset of V st card A = n & card B = 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds

( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

let A, B be finite Subset of V; :: thesis: ( card A = n & card B = 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume that

A27: card A = n and

A28: card B = 0 and

A29: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and

B is linearly-independent ; :: thesis: ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

B = {} by A28;

then A = B \/ A ;

hence ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A27, A29; :: thesis: verum

end;( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

let A, B be finite Subset of V; :: thesis: ( card A = n & card B = 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume that

A27: card A = n and

A28: card B = 0 and

A29: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and

B is linearly-independent ; :: thesis: ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

B = {} by A28;

then A = B \/ A ;

hence ( 0 <= n & ex C being finite Subset of V st

( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A27, A29; :: thesis: verum

let A, B be finite Subset of V; :: thesis: ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )

assume ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent ) ; :: thesis: ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )

hence ( card B <= card A & ex C being finite Subset of V st

( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A30; :: thesis: verum