let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2
let K be F -extending FieldExtension of F; :: thesis: for BE being linearly-independent Subset of (VecSp (E,F))
for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2
let BE be linearly-independent Subset of (VecSp (E,F)); :: thesis: for BK being linearly-independent Subset of (VecSp (K,E))
for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2
let BK be linearly-independent Subset of (VecSp (K,E)); :: thesis: for a1, a2, b1, b2 being Element of K st a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 holds
a1 * b1 <> a2 * b2
let a1, a2, b1, b2 be Element of K; :: thesis: ( a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 implies a1 * b1 <> a2 * b2 )
set VE = VecSp (E,F);
set VK = VecSp (K,E);
assume A0: ( a1 in BE & a2 in BE & b1 in BK & b2 in BK & b1 <> b2 ) ; :: thesis: a1 * b1 <> a2 * b2
then reconsider a1v = a1, a2v = a2 as Element of (VecSp (E,F)) ;
reconsider b1v = b1, b2v = b2 as Element of (VecSp (K,E)) by A0;
A1: a1 <> 0. (VecSp (E,F)) by A0, VECTSP_7:2;
A3: ( 0. (VecSp (E,F)) = 0. E & 0. (VecSp (K,E)) = 0. K ) by FIELD_4:def 6;
A5: ( E is Subring of K & E is Subfield of K ) by FIELD_4:7, FIELD_4:def 1;
then Z: ( 0. K = 0. E & 1. E = 1. K ) by C0SP1:def 3;
reconsider a1e = a1, a2e = a2 as Element of the carrier of E by A0, FIELD_4:def 6;
not a1 is zero by A1, A3, A5, C0SP1:def 3;
then a1e " = a1 " by A5, FIELD_6:18;
then (a1e ") * a2e = (a1 ") * a2 by A5, FIELD_6:16;
then ZZ: - ((a1e ") * a2e) = - ((a1 ") * a2) by A5, FIELD_6:17;
defpred S₁[ object , object ] means ( ( $1 = b1 & $2 = 1. E ) or ( $1 = b2 & $2 = - ((a1 ") * a2) ) or ( $1 <> b1 & $1 <> b2 & $2 = 0. E ) );
A: for x being object st x in the carrier of (VecSp (K,E)) holds
ex y being object st
( y in the carrier of E & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (VecSp (K,E)) implies ex y being object st
( y in the carrier of E & S₁[x,y] ) )
assume x in the carrier of (VecSp (K,E)) ; :: thesis: ex y being object st
( y in the carrier of E & S₁[x,y] )

per cases ( x = b1 or x = b2 or ( x <> b1 & x <> b2 ) ) ;

suppose x = b1 ; :: thesis: ex y being object st
( y in the carrier of E & S₁[x,y] )

hence ex y being object st
( y in the carrier of E & S₁[x,y] ) ; :: thesis: verum

end;

suppose x = b2 ; :: thesis: ex y being object st
( y in the carrier of E & S₁[x,y] )

hence ex y being object st
( y in the carrier of E & S₁[x,y] ) by ZZ; :: thesis: verum

end;

suppose ( x <> b1 & x <> b2 ) ; :: thesis: ex y being object st
( y in the carrier of E & S₁[x,y] )

hence ex y being object st
( y in the carrier of E & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

consider l being Function of the carrier of (VecSp (K,E)), the carrier of E such that
L: for x being object st x in the carrier of (VecSp (K,E)) holds
S₁[x,l . x] from FUNCT_2:sch 1(A);
reconsider l = l as Element of Funcs ( the carrier of (VecSp (K,E)), the carrier of E) by FUNCT_2:8;
for v being Element of (VecSp (K,E)) st not v in {b1v,b2v} holds
l . v = 0. E

proof

let v be Element of (VecSp (K,E)); :: thesis: ( not v in {b1v,b2v} implies l . v = 0. E )
assume not v in {b1v,b2v} ; :: thesis: l . v = 0. E
then ( v <> b1 & v <> b2 ) by TARSKI:def 2;
hence l . v = 0. E by L; :: thesis: verum

end;

then reconsider l = l as Linear_Combination of VecSp (K,E) by VECTSP_6:def 1;
B: l . b1v = 1. E by A0, L
.= 1. K by A5, C0SP1:def 3 ;
then A6: ( b1 in Carrier l & Carrier l <> {} ) by Z, VECTSP_6:1;
C1: [(l . b1v),b1v] in [: the carrier of E, the carrier of K:] by ZFMISC_1:def 2;
D: (l . b1v) * b1v = ( the multF of K | [: the carrier of E, the carrier of K:]) . ((l . b1v),b1v) by FIELD_4:def 6
.= (1. K) * b1 by B, C1, FUNCT_1:49 ;
C1: [(l . b2v),b2v] in [: the carrier of E, the carrier of K:] by ZFMISC_1:def 2;
E: (l . b2v) * b2v = ( the multF of K | [: the carrier of E, the carrier of K:]) . ((l . b2v),b2v) by FIELD_4:def 6
.= the multF of K . ((l . b2v),b2v) by C1, FUNCT_1:49
.= (- ((a1 ") * a2)) * b2 by A0, L ;

now :: thesis: for o being object st o in Carrier l holds
o in {b1v,b2v}

let o be object ; :: thesis: ( o in Carrier l implies o in {b1v,b2v} )
assume o in Carrier l ; :: thesis: o in {b1v,b2v}
then consider v being Element of (VecSp (K,E)) such that
A1: ( o = v & l . v <> 0. E ) by VECTSP_6:1;
( ( v = b1 & l . v = 1. E ) or ( v = b2 & l . v = - ((a1 ") * a2) ) ) by L, A1;
hence o in {b1v,b2v} by A1, TARSKI:def 2; :: thesis: verum

end;

then Carrier l c= {b1v,b2v} ;
then reconsider l = l as Linear_Combination of {b1v,b2v} by VECTSP_6:def 4;
A7: Sum l = ((l . b1v) * b1v) + ((l . b2v) * b2v) by A0, VECTSP_6:18
.= ((1. K) * b1) + ((- ((a1 ") * a2)) * b2) by D, E, FIELD_4:def 6 ;
A8: {b1v,b2v} c= BK by A0, TARSKI:def 2;
A9: a1 <> 0. K by A3, A1, A5, C0SP1:def 3;

now :: thesis: not a1 * b1 = a2 * b2

assume a1 * b1 = a2 * b2 ; :: thesis: contradiction
then 0. K = (a1 * b1) - ((1. K) * (a2 * b2)) by RLVECT_1:15
.= (a1 * b1) - (((a1 ") * a1) * (a2 * b2)) by A9, VECTSP_1:def 10
.= (a1 * b1) - ((a1 * (a1 ")) * (a2 * b2)) by GROUP_1:def 12
.= (a1 * b1) - (a1 * ((a1 ") * (a2 * b2))) by GROUP_1:def 3
.= a1 * (b1 - ((a1 ") * (a2 * b2))) by VECTSP_1:11 ;
then 0. K = ((1. K) * b1) - ((a1 ") * (a2 * b2)) by Z, A1, A3, VECTSP_2:def 1
.= ((1. K) * b1) + (- (((a1 ") * a2) * b2)) by GROUP_1:def 3
.= Sum l by A7, VECTSP_1:9 ;
hence contradiction by A3, A6, A8, VECTSP_7:1, VECTSP_7:def 1; :: thesis: verum

end;

hence a1 * b1 <> a2 * b2 ; :: thesis: verum