let F be Field; :: thesis: for W1, W2 being finite-dimensional VectSp of F st (Omega). W1 = (Omega). W2 holds
for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
let W1, W2 be finite-dimensional VectSp of F; :: thesis: ( (Omega). W1 = (Omega). W2 implies for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2 )
assume A1: (Omega). W1 = (Omega). W2 ; :: thesis: for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
let m be Nat; :: thesis: m Subspaces_of W1 = m Subspaces_of W2
(Omega). W1 is Subspace of (Omega). W2 by A1, VECTSP_4:24;
then W1 is Subspace of (Omega). W2 by Th5;
then W1 is Subspace of W2 by Th3;
hence m Subspaces_of W1 c= m Subspaces_of W2 by VECTSP_9:38; :: according to XBOOLE_0:def 10 :: thesis: m Subspaces_of W2 c= m Subspaces_of W1
(Omega). W2 is Subspace of (Omega). W1 by A1, VECTSP_4:24;
then W2 is Subspace of (Omega). W1 by Th5;
then W2 is Subspace of W1 by Th3;
hence m Subspaces_of W2 c= m Subspaces_of W1 by VECTSP_9:38; :: thesis: verum