let V be RealLinearSpace; :: thesis:
set B = center_of_mass V;
defpred S₁[ Nat] means for k being Nat st k <= $1 holds
for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds
(center_of_mass V) .: S is affinely-independent Subset of V;
let S be c=-linear Subset-Family of V; :: thesis:
A1: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let k be Nat; :: thesis:
assume A4: k <= n + 1 ; :: thesis:

per cases by A4, NAT_1:8;

suppose k <= n ; :: thesis:

hence for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds
(center_of_mass V) .: S is affinely-independent Subset of V by A3; :: thesis:

end;

suppose A5: k = n + 1 ; :: thesis:

let S be c=-linear Subset-Family of V; :: thesis:
assume that
A6: card (union S) = k and
A7: ( union S is finite & union S is affinely-independent ) ; :: thesis:
set U = union S;
A8: S c= bool (union S) by ZFMISC_1:82;
set SU = S \ {(union S)};
A9: union (S \ {(union S)}) c= union S by XBOOLE_1:36, ZFMISC_1:77;
then reconsider Usu = union (S \ {(union S)}) as finite set by A7;
A10: S \ {(union S)} c= S by XBOOLE_1:36;
A11: union (S \ {(union S)}) <> union S

proof

assume A12: union (S \ {(union S)}) = union S ; :: thesis:
then not S \ {(union S)} is empty by A5, A6, ZFMISC_1:2;
then union (S \ {(union S)}) in S \ {(union S)} by A7, A10, A8, SIMPLEX0:9;
hence contradiction by A12, ZFMISC_1:56; :: thesis:

end;

then union (S \ {(union S)}) c< union S by A9;
then consider v being object such that
A13: v in union S and
A14: not v in union (S \ {(union S)}) by XBOOLE_0:6;
reconsider v = v as Element of V by A13;
A15: ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} is affinely-independent Subset of V by A7, A13, Th28;
not union S is empty by A5, A6;
then A16: union S in dom (center_of_mass V) by A1, ZFMISC_1:56;
(center_of_mass V) . (union S) in {((center_of_mass V) . (union S))} by TARSKI:def 1;
then (center_of_mass V) . (union S) in ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} by XBOOLE_0:def 3;
then reconsider BU = (center_of_mass V) . (union S) as Element of V by A15;
not S is empty by A5, A6, ZFMISC_1:2;
then (S \ {(union S)}) \/ {(union S)} = S by A7, A8, SIMPLEX0:9, ZFMISC_1:116;
then A17: (center_of_mass V) .: S = ((center_of_mass V) .: (S \ {(union S)})) \/ ((center_of_mass V) .: {(union S)}) by RELAT_1:120
.= ((center_of_mass V) .: (S \ {(union S)})) \/ (Im ((center_of_mass V),(union S))) by RELAT_1:def 16
.= ((center_of_mass V) .: (S \ {(union S)})) \/ {BU} by A16, FUNCT_1:59 ;
A18: {v} c= union S by A13, ZFMISC_1:31;
A19: card {v} = 1 by CARD_1:30;

per cases ;

suppose n = 0 ; :: thesis:

then A20: union S = {v} by A5, A6, A7, A18, A19, CARD_2:102;
(S \ {(union S)}) /\ (dom (center_of_mass V)) = {}

proof

assume (S \ {(union S)}) /\ (dom (center_of_mass V)) <> {} ; :: thesis:
then consider x being object such that
A21: x in (S \ {(union S)}) /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;
reconsider x = x as set by TARSKI:1;
x in S \ {(union S)} by A21, XBOOLE_0:def 4;
then A22: x c= union (S \ {(union S)}) by ZFMISC_1:74;
then x c= union S by A9;
then A23: ( x = union S or x = {} ) by A20, ZFMISC_1:33;
not v in x by A14, A22;
hence contradiction by A20, A21, A23, TARSKI:def 1, ZFMISC_1:56; :: thesis:

end;

then (center_of_mass V) .: (S \ {(union S)}) = (center_of_mass V) .: {} by RELAT_1:112
.= {} ;
hence (center_of_mass V) .: S is affinely-independent Subset of V by A17; :: thesis:

end;

suppose A24: n > 0 ; :: thesis:

reconsider u = union S as finite set by A7;
A25: Usu c= u by XBOOLE_1:36, ZFMISC_1:77;
then card Usu <= n + 1 by A5, A6, NAT_1:43;
then card Usu < n + 1 by A5, A6, A11, A25, CARD_2:102, XXREAL_0:1;
then A26: card Usu <= n by NAT_1:13;
( union (S \ {(union S)}) c= (union S) \ {v} & (union S) \ {v} c= ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} ) by A9, A14, XBOOLE_1:7, ZFMISC_1:34;
then union (S \ {(union S)}) is affinely-independent by A15, RLAFFIN1:43, XBOOLE_1:1;
then reconsider BSU = (center_of_mass V) .: (S \ {(union S)}) as affinely-independent Subset of V by A3, A10, A26;
BSU c= Affin ((union S) \ {v})

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in BSU ; :: thesis:
then consider x being object such that
A27: x in dom (center_of_mass V) and
A28: x in S \ {(union S)} and
A29: (center_of_mass V) . x = y by FUNCT_1:def 6;
reconsider x = x as non empty Subset of V by A27, ZFMISC_1:56;
x in S by A28, XBOOLE_0:def 5;
then A30: x c= union S by ZFMISC_1:74;
x c= union (S \ {(union S)}) by A28, ZFMISC_1:74;
then not v in x by A14;
then x c= (union S) \ {v} by A30, ZFMISC_1:34;
then A31: conv x c= conv ((union S) \ {v}) by RLTOPSP1:20;
y in conv x by A7, A29, A30, Th16;
then A32: y in conv ((union S) \ {v}) by A31;
conv ((union S) \ {v}) c= Affin ((union S) \ {v}) by RLAFFIN1:65;
hence y in Affin ((union S) \ {v}) by A32; :: thesis:

end;

then A33: Affin BSU c= Affin ((union S) \ {v}) by RLAFFIN1:51;
card (union S) <> 1 by A5, A6, A24;
then not BU in union S by A7, Th19;
then not BU in (union S) \ {v} by XBOOLE_0:def 5;
then not BU in Affin BSU by A15, A33, Th27;
hence (center_of_mass V) .: S is affinely-independent Subset of V by A17, Th27; :: thesis:

end;

end;

end;

end;

end;

A34: S₁[ 0 ]

proof

let k be Nat; :: thesis:
assume A35: k <= 0 ; :: thesis:
let S be c=-linear Subset-Family of V; :: thesis:
assume that
A36: card (union S) = k and
( union S is finite & union S is affinely-independent ) ; :: thesis:
A37: union S = {} by A35, A36;
S /\ (dom (center_of_mass V)) = {}

proof

assume S /\ (dom (center_of_mass V)) <> {} ; :: thesis:
then consider x being object such that
A38: x in S /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;
reconsider x = x as set by TARSKI:1;
x in S by A38, XBOOLE_0:def 4;
then A39: x c= {} by A37, ZFMISC_1:74;
x <> {} by A38, ZFMISC_1:56;
hence contradiction by A39; :: thesis:

end;

then (center_of_mass V) .: S = (center_of_mass V) .: {} by RELAT_1:112
.= {} ;
hence (center_of_mass V) .: S is affinely-independent Subset of V ; :: thesis:

end;

A40: for n being Nat holds S₁[n] from NAT_1:sch 2(A34, A2);
assume A41: ( union S is finite & union S is affinely-independent ) ; :: thesis:
then card (union S) is Nat ;
hence (center_of_mass V) .: S is affinely-independent Subset of V by A40, A41; :: thesis: