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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = 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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = 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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = 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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = 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 & a1 * b1 = a2 * b2 holds
( a1 = a2 & b1 = b2 )
let a1, a2, b1, b2 be Element of K; :: thesis: ( a1 in BE & a2 in BE & b1 in BK & b2 in BK & a1 * b1 = a2 * b2 implies ( a1 = a2 & b1 = b2 ) )
assume A1: ( a1 in BE & a2 in BE & b1 in BK & b2 in BK ) ; :: thesis: ( not a1 * b1 = a2 * b2 or ( a1 = a2 & b1 = b2 ) )
then reconsider b1v = b1 as Element of (VecSp (K,E)) ;
assume A2: a1 * b1 = a2 * b2 ; :: thesis: ( a1 = a2 & b1 = b2 )
{b1v} c= BK by A1, TARSKI:def 1;
then b1v <> 0. (VecSp (K,E)) by VECTSP_7:1, VECTSP_7:3;
then A3: b1 <> 0. K by FIELD_4:def 6;
A4: b1 = b2 by A1, A2, BE0;
a1 * b1 = b2 * a2 by A2, GROUP_1:def 12;
then b1 * a1 = b2 * a2 by GROUP_1:def 12;
hence ( a1 = a2 & b1 = b2 ) by A3, A4, VECTSP_2:8; :: thesis: verum