let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)
let K be F -extending FieldExtension of F; :: thesis: for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)
let BE be non empty finite linearly-independent Subset of (VecSp (E,F)); :: thesis: for BK being non empty finite linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = (card BE) * (card BK)
let BK be non empty finite linearly-independent Subset of (VecSp (K,E)); :: thesis: card (Base (BE,BK)) = (card BE) * (card BK)
thus (card BE) * (card BK) = card [:BE,BK:] by CARD_2:46
.= card (Base (BE,BK)) by BE1 ; :: thesis: verum