let V be free finite-rank Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V st V is_the_direct_sum_of W1,W2 holds
rank V = (rank W1) + (rank W2)
let W1, W2 be free finite-rank Subspace of V; :: thesis: ( V is_the_direct_sum_of W1,W2 implies rank V = (rank W1) + (rank W2) )
assume A1: V is_the_direct_sum_of W1,W2 ; :: thesis: rank V = (rank W1) + (rank W2)
rank ((Omega). V) = (rank W1) + (rank W2) by ThRankDirectSum, A1;
hence rank V = (rank W1) + (rank W2) by ZMODUL05:4; :: thesis: verum