let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let K be E -extending FieldExtension of F; :: thesis:
let BE be finite Subset of (VecSp (K,E)); :: thesis:
let BF be finite Subset of (VecSp (K,F)); :: thesis:
let l1 be Linear_Combination of BF; :: thesis:
let l2 be Linear_Combination of BE; :: thesis:
assume AS: ( l1 = l2 & BF c= BE ) ; :: thesis:
H0: the carrier of (VecSp (K,F)) = the carrier of K by FIELD_4:def 6
.= the carrier of (VecSp (K,E)) by FIELD_4:def 6 ;
H1: ( F is Subring of E & E is Subring of K ) by FIELD_4:def 1;
then H2: ( the carrier of F c= the carrier of E & the carrier of E c= the carrier of K ) by C0SP1:def 3;
defpred S₁[ Nat] means for l1 being Linear_Combination of BF
for l2 being Linear_Combination of BE st l1 = l2 & BF c= BE & card (Carrier l1) = $1 holds
Sum l1 = Sum l2;
IA: S₁[ 0 ]

proof

now :: thesis:

let l1 be Linear_Combination of BF; :: thesis:
let l2 be Linear_Combination of BE; :: thesis:
assume A: ( l1 = l2 & BF c= BE & card (Carrier l1) = 0 ) ; :: thesis:
card (Carrier l2) = 0

proof

now :: thesis:

assume B1: Carrier l2 <> {} ; :: thesis:
set o = the Element of Carrier l2;
consider v2 being Element of (VecSp (K,E)) such that
B2: ( the Element of Carrier l2 = v2 & l2 . v2 <> 0. E ) by B1, VECTSP_6:1;
reconsider v1 = v2 as Element of (VecSp (K,F)) by H0;
0. E = 0. F by H1, C0SP1:def 3;
then the Element of Carrier l2 in Carrier l1 by A, B2, VECTSP_6:1;
hence contradiction by A; :: thesis:

end;

hence card (Carrier l2) = 0 ; :: thesis:

end;

then A0: ( Carrier l1 = {} & Carrier l2 = {} ) by A;
hence Sum l1 = 0. (VecSp (K,F)) by VECTSP_6:19
.= 0. K by FIELD_4:def 6
.= 0. (VecSp (K,E)) by FIELD_4:def 6
.= Sum l2 by A0, VECTSP_6:19 ;
:: thesis:

end;

hence S₁[ 0 ] ; :: thesis:

end;

IS: now :: thesis:

let k be Nat; :: thesis:
assume IV: S₁[k] ; :: thesis:

now :: thesis:

let l1 be Linear_Combination of BF; :: thesis:
let l2 be Linear_Combination of BE; :: thesis:
assume A0: ( l1 = l2 & BF c= BE & card (Carrier l1) = k + 1 ) ; :: thesis:
then A1: Carrier l1 <> {} ;
set o = the Element of Carrier l1;
A2: the Element of Carrier l1 in Carrier l1 by A1;
then reconsider v1 = the Element of Carrier l1 as Element of (VecSp (K,F)) ;
A3: ( the carrier of (VecSp (K,F)) = the carrier of K & the carrier of (VecSp (K,E)) = the carrier of K ) by FIELD_4:def 6;
A4: ( Carrier l1 c= BF & Carrier l2 c= BE ) by VECTSP_6:def 4;
reconsider v2 = v1 as Element of (VecSp (K,E)) by A3;
defpred S₂[ Element of K, Element of F] means ( ( $1 = v1 & $2 = l1 . v1 ) or ( $1 <> v1 & $2 = 0. F ) );

G0: now :: thesis:

let x be Element of K; :: thesis:

per cases ;

suppose x = the Element of Carrier l1 ; :: thesis:

hence ex y being Element of F st S₂[x,y] ; :: thesis:

end;

suppose x <> the Element of Carrier l1 ; :: thesis:

hence ex y being Element of F st S₂[x,y] ; :: thesis:

end;

consider f being Function of the carrier of K, the carrier of F such that
G1: for x being Element of K holds S₂[x,f . x] from FUNCT_2:sch 3(G0);
( dom f = the carrier of (VecSp (K,F)) & rng f c= the carrier of F ) by A3, FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (K,F)), the carrier of F) by FUNCT_2:def 2;

now :: thesis:

let v be Element of (VecSp (K,F)); :: thesis:
assume not v in BF ; :: thesis:
then not v in Carrier l1 by A4;
hence f . v = 0. F by G1, A2, A3; :: thesis:

end;

then reconsider h = f as Linear_Combination of VecSp (K,F) by VECTSP_6:def 1;

Z100: now :: thesis:

let o be object ; :: thesis:
assume C1: o in Carrier h ; :: thesis:
then reconsider v = o as Element of (VecSp (K,F)) ;
reconsider x = v as Element of K by FIELD_4:def 6;
h . x <> 0. F by C1, VECTSP_6:2;
then v = v1 by G1;
hence o in {v1} by TARSKI:def 1; :: thesis:

end;

then Carrier h c= {v1} ;
then Y: h is Linear_Combination of {v1} by VECTSP_6:def 4;
{v1} c= Carrier l1 by A2, TARSKI:def 1;
then {v1} c= BF by A4;
then reconsider h1 = h as Linear_Combination of BF by Y, VECTSP_6:4;
reconsider h2 = h1 as Linear_Combination of BE by A0, sp1;
Z: h2 is Linear_Combination of {v2}

proof

now :: thesis:

let o be object ; :: thesis:
assume Z1: o in Carrier h2 ; :: thesis:
then reconsider v = o as Element of (VecSp (K,E)) ;
reconsider x = v as Element of (VecSp (K,E)) ;
h2 . v <> 0. E by Z1, VECTSP_6:2;
then ( h1 . x <> 0. F & x in the carrier of K ) by A3, H1, C0SP1:def 3;
then x = v1 by G1;
hence o in {v2} by TARSKI:def 1; :: thesis:

end;

then Carrier h2 c= {v2} ;
hence h2 is Linear_Combination of {v2} by VECTSP_6:def 4; :: thesis:

end;

Z1: h2 . v2 = h1 . v1 ;
Z3: [(h1 . v1),v2] in [: the carrier of F, the carrier of K:] by A3, ZFMISC_1:def 2;
Z4: [(h2 . v1),v2] in [: the carrier of E, the carrier of K:] by A3, Z1, ZFMISC_1:def 2;
Z5: Sum h1 = (h1 . v1) * v1 by Y, VECTSP_6:17
.= ( the multF of K | [: the carrier of F, the carrier of K:]) . ((h1 . v1),v2) by FIELD_4:def 6
.= the multF of K . ((h1 . v1),v2) by Z3, FUNCT_1:49
.= ( the multF of K | [: the carrier of E, the carrier of K:]) . ((h2 . v2),v2) by Z4, FUNCT_1:49
.= (h2 . v2) * v2 by FIELD_4:def 6
.= Sum h2 by Z, VECTSP_6:17 ;
reconsider li1 = l1 - h1 as Linear_Combination of BF by VECTSP_6:42;
li1 - (l1 - h1) = ZeroLC (VecSp (K,F)) by VECTSP_6:43;
then B: l1 = (li1 - (l1 - h1)) + l1 by VECTSP_6:27
.= (li1 + (- (l1 - h1))) + l1 by VECTSP_6:def 11
.= (li1 + (- (l1 + (- h1)))) + l1 by VECTSP_6:def 11
.= li1 + ((- (l1 + (- h1))) + l1) by VECTSP_6:26
.= li1 + (((- (1. F)) * (l1 + (- h1))) + l1) by VECTSP_6:def 10
.= li1 + ((((- (1. F)) * l1) + ((- (1. F)) * (- h1))) + l1) by VECTSP_6:33
.= li1 + ((((- (1. F)) * l1) + ((- (1. F)) * ((- (1. F)) * h1))) + l1) by VECTSP_6:def 10
.= li1 + ((((- (1. F)) * l1) + (((- (1. F)) * (- (1. F))) * h1)) + l1) by VECTSP_6:34
.= li1 + ((((- (1. F)) * l1) + (((1. F) * (1. F)) * h1)) + l1) by VECTSP_1:10
.= li1 + ((((- (1. F)) * l1) + h1) + l1) by VECTSP_6:35
.= li1 + (((- l1) + h1) + l1) by VECTSP_6:def 10
.= li1 + ((h1 + (- l1)) + l1) by VECTSP_6:25
.= li1 + (h1 + ((- l1) + l1)) by VECTSP_6:26
.= li1 + (h1 + (l1 + (- l1))) by VECTSP_6:25
.= li1 + (h1 + (l1 - l1)) by VECTSP_6:def 11
.= li1 + (h1 + (ZeroLC (VecSp (K,F)))) by VECTSP_6:43
.= li1 + h1 by VECTSP_6:27 ;
reconsider li2 = l2 - h2 as Linear_Combination of BE by VECTSP_6:42;
li2 - (l2 - h2) = ZeroLC (VecSp (K,E)) by VECTSP_6:43;
then C: l2 = (li2 - (l2 - h2)) + l2 by VECTSP_6:27
.= (li2 + (- (l2 - h2))) + l2 by VECTSP_6:def 11
.= (li2 + (- (l2 + (- h2)))) + l2 by VECTSP_6:def 11
.= li2 + ((- (l2 + (- h2))) + l2) by VECTSP_6:26
.= li2 + (((- (1. E)) * (l2 + (- h2))) + l2) by VECTSP_6:def 10
.= li2 + ((((- (1. E)) * l2) + ((- (1. E)) * (- h2))) + l2) by VECTSP_6:33
.= li2 + ((((- (1. E)) * l2) + ((- (1. E)) * ((- (1. E)) * h2))) + l2) by VECTSP_6:def 10
.= li2 + ((((- (1. E)) * l2) + (((- (1. E)) * (- (1. E))) * h2)) + l2) by VECTSP_6:34
.= li2 + ((((- (1. E)) * l2) + (((1. E) * (1. E)) * h2)) + l2) by VECTSP_1:10
.= li2 + ((((- (1. E)) * l2) + h2) + l2) by VECTSP_6:35
.= li2 + (((- l2) + h2) + l2) by VECTSP_6:def 10
.= li2 + ((h2 + (- l2)) + l2) by VECTSP_6:25
.= li2 + (h2 + ((- l2) + l2)) by VECTSP_6:26
.= li2 + (h2 + (l2 + (- l2))) by VECTSP_6:25
.= li2 + (h2 + (l2 - l2)) by VECTSP_6:def 11
.= li2 + (h2 + (ZeroLC (VecSp (K,E)))) by VECTSP_6:43
.= li2 + h2 by VECTSP_6:27 ;
Z6: li1 = li2

proof

D1: dom li1 = the carrier of (VecSp (K,F)) by FUNCT_2:def 1
.= dom li2 by A3, FUNCT_2:def 1 ;

now :: thesis:

let o be object ; :: thesis:
assume D2: o in dom li1 ; :: thesis:
then reconsider vF = o as Element of (VecSp (K,F)) ;
reconsider vE = o as Element of (VecSp (K,E)) by D1, D2;
reconsider lF = li1 . vF, aF = h1 . vF as Element of K by H2;
reconsider lE = li2 . vE, aE = h2 . vE as Element of K by H2;
D4: [lF,aF] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
D5: [: the carrier of F, the carrier of F:] c= [: the carrier of E, the carrier of E:] by H2, ZFMISC_1:96;
D6: l1 . vF = (li1 . vF) + (h1 . vF) by B, VECTSP_6:22
.= ( the addF of E || the carrier of F) . (lF,aF) by H1, C0SP1:def 3
.= the addF of E . (lF,aF) by D4, FUNCT_1:49
.= ( the addF of K || the carrier of E) . (lF,aF) by H1, C0SP1:def 3
.= lF + aF by D4, D5, FUNCT_1:49 ;
D7: [lE,aE] in [: the carrier of E, the carrier of E:] by ZFMISC_1:def 2;
D8: l2 . vF = (li2 . vE) + (h2 . vE) by C, VECTSP_6:22
.= ( the addF of K || the carrier of E) . (lE,aE) by H1, C0SP1:def 3
.= lE + aE by D7, FUNCT_1:49 ;
lF = lF + (0. K)
.= lF + (aF + (- aF)) by RLVECT_1:5
.= (lF + aF) + (- aF) by RLVECT_1:def 3
.= lE + (aE + (- aE)) by A0, D6, D8, RLVECT_1:def 3
.= lE + (0. K) by RLVECT_1:5 ;
hence li1 . o = li2 . o ; :: thesis:

end;

hence li1 = li2 by D1; :: thesis:

end;

ZZ: v1 is Element of K by FIELD_4:def 6;
Z7: li1 . v1 = (l1 . v1) - (h1 . v1) by VECTSP_6:40
.= (l1 . v1) - (l1 . v1) by ZZ, G1
.= 0. F by RLVECT_1:5 ;
Carrier l1 = (Carrier li1) \/ {v1}

proof

B9: li1 . v1 = (l1 . v1) - (h1 . v1) by VECTSP_6:40
.= (l1 . v1) + (- (l1 . v1)) by ZZ, G1
.= 0. F by RLVECT_1:5 ;
B0: for x being Element of K st x <> v1 holds
li1 . x = l1 . x

proof

let x be Element of K; :: thesis:
reconsider v = x as Element of (VecSp (K,F)) by FIELD_4:def 6;
assume x <> v1 ; :: thesis:
then not v in {v1} by TARSKI:def 1;
then h1 . v = 0. F by Z100, VECTSP_6:1;
then li1 . v = (l1 . v) - (0. F) by VECTSP_6:40;
hence li1 . x = l1 . x ; :: thesis:

end;

B7: now :: thesis:

let o be object ; :: thesis:
assume B8: o in Carrier li1 ; :: thesis:
then reconsider v = o as Element of (VecSp (K,F)) ;
reconsider vK = v as Element of K by FIELD_4:def 6;
B1: li1 . v <> 0. F by B8, VECTSP_6:2;
then li1 . vK = l1 . vK by B0, B9;
hence o in Carrier l1 by B1, VECTSP_6:2; :: thesis:

end;

B1: now :: thesis:

let o be object ; :: thesis:
assume B2: o in Carrier l1 ; :: thesis:
then reconsider v = o as Element of (VecSp (K,F)) ;
ZZ: v is Element of K by FIELD_4:def 6;

per cases ;

suppose o = v1 ; :: thesis:

then o in {v1} by TARSKI:def 1;
hence o in (Carrier li1) \/ {v1} by XBOOLE_0:def 3; :: thesis:

end;

suppose o <> v1 ; :: thesis:

then l1 . v = li1 . v by ZZ, B0;
then li1 . v <> 0. F by B2, VECTSP_6:2;
then v in Carrier li1 by VECTSP_6:2;
hence o in (Carrier li1) \/ {v1} by XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in (Carrier li1) \/ {v1} ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose o in Carrier li1 ; :: thesis:

hence o in Carrier l1 by B7; :: thesis:

end;

suppose o in {v1} ; :: thesis:

hence o in Carrier l1 by A2, TARSKI:def 1; :: thesis:

end;

hence Carrier l1 = (Carrier li1) \/ {v1} by B1, TARSKI:2; :: thesis:

end;

then Z8: (card (Carrier li1)) + 1 = k + 1 by Z7, A0, VECTSP_6:2, CARD_2:41;
thus Sum l1 = (Sum li1) + (Sum h1) by B, VECTSP_6:44
.= the addF of (VecSp (K,F)) . ((Sum li2),(Sum h2)) by Z8, Z6, Z5, A0, IV
.= the addF of K . ((Sum li2),(Sum h2)) by FIELD_4:def 6
.= (Sum li2) + (Sum h2) by FIELD_4:def 6
.= Sum l2 by C, VECTSP_6:44 ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: card (Carrier l1) = n ;
thus Sum l1 = Sum l2 by AS, I, H; :: thesis: