now :: thesis: for o being object st o in { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } holds
o in the carrier of (VecSp (K,F))

let o be object ; :: thesis: ( o in { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } implies o in the carrier of (VecSp (K,F)) )
assume o in { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } ; :: thesis: o in the carrier of (VecSp (K,F))
then consider a, b being Element of K such that
A: ( o = a * b & a in BE & b in BK ) ;
the carrier of (VecSp (K,F)) = the carrier of K by FIELD_4:def 6;
hence o in the carrier of (VecSp (K,F)) by A; :: thesis: verum

end;

then { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } c= the carrier of (VecSp (K,F)) ;
hence { (a * b) where a, b is Element of K : ( a in BE & b in BK ) } is Subset of (VecSp (K,F)) ; :: thesis: verum