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 S1[ 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 S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; :: thesis: S1[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 ;
reconsider v = v as VECTOR of V by A7;
set Bv = B \ {v};
A8: B \ {v} is linearly-independent by ;
{v} is Subset of B by ;
then A9: card (B \ {v}) = (card B) - () by CARD_2:44
.= (m + 1) - 1 by
.= 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 ;
A14: now :: thesis: not m = n
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 ;
hence contradiction by A13, RUSUB_3:21; :: thesis: verum
end;
v in Lin ((B \ {v}) \/ C) by A12;
then consider w being VECTOR of V such that
A17: w in C and
A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by ;
set Cw = C \ {w};
((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by ;
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 ;
{w} is Subset of C by ;
then A20: card (C \ {w}) = (card C) - () by CARD_2:44
.= (n - m) - 1 by
.= 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 ;
then A22: w in Lin (B \/ (C \ {w})) by ;
A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by ;
now :: thesis: for x being object st x in (B \ {v}) \/ C holds
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 ;
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 ;
hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22; :: thesis: verum
end;
then (B \ {v}) \/ C c= the carrier of (Lin (B \/ (C \ {w}))) ;
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 ;
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 ;
m <= n by A2, A3, A5, A9, A8;
then m < n by ;
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 ; :: thesis: verum
end;
A26: S1[ 0 ]
proof
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 ; :: thesis: verum
end;
A30: for m being Nat holds S1[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